« April 2017 »
April
MoTuWeThFrSaSu
12
3456789
10111213141516
17181920212223
24252627282930
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