A Dynamic Logic for deductive verification of multi-threaded programs

摘要

We present MODL, a Dynamic Logic and a deductive verification calculus for a core Java-like language that includes multi-threading. The calculus is based on symbolic execution. Even though we currently do not handle non-atomic loops, employing the technique of symmetry reduction allows us to verify systems without limits on state space or thread number. We have instantiated our logic for (restricted) multi-threaded Java programs and implemented the verification calculus within the KeY system. We demonstrate our approach by verifying a central method of the StringBuf f er class from the Java standard library in the presence of unbounded concurrency.