AMTV
AMTV(Automated Modular Thread Verifier) proves safety of multithreaded programs. AMTV takes a finite-state multithreaded program and a specification; it outputs either an inductive invariant that proves the property or all shortest error traces. AMTV always terminates with a definite answer. AMTV is polynomial-time on all programs with thread-modular proofs and on a class of binary mutex programs without thread-modular proofs. AMTV practically fights the state explosion problem in the number of threads, scaling, for example, up to 100 threads on the binary mutex programs. For more information, please contact Alexander Malkis.