Distributed, Multi-Threaded Verification of Java Programs

Extended Static Checking (ESC) is a fully automated formal verification technique and is generally quite efficient, as far as verification tools go, but it is still orders of magnitude slower than simple compilation. Verification in ESC is achieved by translating programs and their specifications into Verification Conditions (VCs). Proof of a VC establishes the correctness of the program. As can be imagined, proving VCs is computationally expensive: While small classes can be verified in seconds, verifying larger programs of 50 KLOC can take hours. To help address this lack of scalability, this paper presents the multi-threaded version of ESC4 and its distributed prover back-end.