swMATH ID: 9878
Software Authors: Tal Lev-Ami; Mooly Sagiv
Description: TVLA: A System for Implementing Static Analyses. We present TVLA (Three-Valued-Logic Analyzer). TVLA is a “YACC”-like framework for automatically constructing static-analysis algorithms from an operational semantics, where the operational semantics is specified using logical formulae. TVLA has been implemented in Java and was successfully used to perform shape analysis on programs manipulating linked data structures (singly and doubly linked lists), to prove safety properties of Mobile Ambients, and to verify the partial correctness of several sorting programs.
Homepage: http://www.cs.tau.ac.il/~tvla/
Related Software: ESC/Java; SIMPLIFY; SPIN; SLAM; ASTREE; z3; BLAST; Spec#; CSSV; MONA; Dafny; DART; Houdini; SatAbs; VeriFast; Smallfoot; BoogiePL; Bandera; Java PathFinder; veriSoft
Cited in: 31 Publications

Standard Articles

1 Publication describing the Software, including 1 Publication in zbMATH Year
TVLA: A system for implementing static analyses. Zbl 0966.68580
Lev-Ami, Tal; Sagiv, Mooly

Citations by Year