« March 2017 »
March
MoTuWeThFrSaSu
12345
6789101112
13141516171819
20212223242526
2728293031
Uni-Logo
You are here: Home Tools AMTV
Document Actions

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.

Personal tools