« February 2018 »
February
MoTuWeThFrSaSu
1234
567891011
12131415161718
19202122232425
262728
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