3-Valued Logic Analysis Engine

Introduction

• A powerful language for expressing concrete semantics;
• Automatic generation of abstract interpreters from concrete semantics;
• Tunable abstractions and tunable transformers; and
  

Mailing list

Have a TVLA related question? Want to share your experience with other TVLA users?
You can do so by sending mail to the TVLA mailing list (address appears at top of page).
You can also view the TVLA mailing list archive (requires registration to LISTSERV)

Downloads

TVLA is available for academic use only, with no support.

TVLA 3 + HeDec

An experimental version of TVLA with Heap Decomposition
[HeDec Tech. Report] [tvla-3.tar.gz] [tvla-3.jar]

TVLA 3

An experimental version presented at CAV 2007 (July, 2007)
tvla-3.0alpha.zip

TVLA 2

An alpha version is now available (August 23, 2004).
tvla-2-alpha.jar
tvla-2-alpha.tar.gz

TVLA 0.91

Java distribution (August 19, 2002)
Native Win32 distribution (February 4, 2002)
Known bugs and limitations

TVLA 0.9

Java distribution

TVLA extensions

3VMC : A 3-Valued Model Checker

3VMC is a tool developed by Eran Yahav for analysis and verification of concurrent systems.
More information, including a user-manual and TVM examples is available from the link above.
3VMC has been integrated into TVLA since version 0.91.

Alexsa : Algorithm Explanation by Shape Analysis

Alexa is an extension developed by Ronald Bieber for visualization for TVLA outputs.
Alexsa is distributed separately.
More information is available from the link above.

Related projects, tools and theories

Local Reasoning and Separation Logic [Smallfoot] [Slayer]
``The main ingredients of the work so far are the logic of bunched implications (BI), a general logic of resource composition, and separation logic, an extension of Hoare's logic which addresses difficulties in reasoning about pointer data structures.''

CANVAS
The CANVAS project uses TVLA as a test bed for abstract interpretation. The goal is to check conformance of Java programs to EASL specifications.

Composite Symbolic Library
Combines different abstract domains, including shape graphs to verify concurrent systems.

Pointer Assertion Logic Engine
``Pointer Assertion Logic is a notation for expressing assertions about the heap structure of imperative languages. It allows programmers to specify pre- and post-conditions of procedures, loop invariants, and other assertions in Weak Monadic Second-order Logic of Graph Types ...
PALE - the Pointer Assertion Logic Engine - is a complete implementation of the technique.''

Related publications

"Revamping TVLA: Making Parametric Shape Analysis Competitive"
Igor Bogudlov, Tal Lev-Ami, Thomas Reps, and Mooly Sagiv in CAV 2007

"Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists"
Roman Manevich, Eran Yahav, G. Ramalingam and Mooly Sagiv in VMCAI 2005

"Partially Disjunctive Heap Abstraction"
Roman Manevich, Mooly Sagiv, Ganesan Ramalingam, and John Field in SAS 2004

"A Relational Approach to Interprocedural Shape Analysis"
Bertrand Jeannet, Alexey Loginov, Thomas Reps, Mooly Sagiv in SAS 2004

"Verifying Safety Properties Using Separation and Heterogeneous Abstractions"
Yahav E. and Ramalingam G. in PLDI 2004

"Verification via structure simulation"
Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., and Yorsh, G. in CAV 2004

"Symbolically computing most-precise abstract operations for shape analysis"
Yorsh, G., Reps, T., and Sagiv, M. in TACAS 2004

"Symbolic implementation of the best transformer"
Reps, T., Sagiv, M., and Yorsh, G. in VMCAI 2004

"TVLA: A System for Generating Abstract Interpreters"
Tal Lev-Ami, Roman Manevich, and Mooly Sagiv in IFIP 2004

"Generating Concrete Counterexamples for Sound Abstract Interpretation"
Erez G., Yahav E., and Sagiv M. 2004

"Numeric domains with summarized dimensions"
Gopan, D., DiMaio, F., Dor, N., Reps, T., and Sagiv, M. in TACAS 2003

"Establishing Local Temporal Heap Safety Properties with Application to Compile-Time Memory Management"
Shaham R., Yahav E., Kolodner E.K., and Sagiv M. in SAS 2003

"Automatically Verifying Concurrent Queue Algorithms"
Yahav E. and Sagiv M. in SoftMC 2003

"Finite Differencing of Logical Formulas for Static Analysis"
Thomas W. Reps, Shmuel Sagiv, and Alexey Loginov in ESOP 2003

"Verifying Temporal Heap Properties Specified via Evolution Logic"
Yahav, E., Reps, T., Sagiv, M., and Wilhelm R. in ESOP 2003

"Logical characterizations of heap abstractions"
Greta Yorsh, Master's thesis 2003

"Data Structures and Algorithms for Efficient Shape Analysis"
Roman Manevich, Master's thesis 2003

"Solving The Apprentice Challenge with 3VMC"
Eran Yahav in 2003 (unpublished)

"Deriving Specialized Program Analyses for Certifying Component-Client Conformance"
Ramalingam, G., Warshavsky, A., Field, J., Goyal, D., Sagiv in PLDI 2002

"Compactly Representing First-Order Structures for Static Analysis"
R. Manevich, G. Ramalingam, J. Field, D.Goyal, and M. Sagiv in SAS 2002

"Parametric shape analysis via 3-valued logic"
Shmuel Sagiv, Thomas W. Reps, Reinhard Wilhelm in TOPLAS 2002

"Kleene's Logic with Equality"
Nielson, F., Nielson, H.R. and Sagiv, M, in IPL 2001

"InterProcedural Shape Analysis"
Noam Rinetsky, Master's Thesis 2001

"Interprocedural Shape Analysis for Recursive Programs"
N. Rinetskey N., and Sagiv M. in CC 2001

"Verifying Safety Properties of Concurrent Java Programs using 3-Valued Logic"
Yahav E. in POPL 2001

"Putting Static Analysis to Work for Verification: A Case Study"
Lev-Ami T., Reps T., Sagiv. M. and Wilhelm R. in ISSTA 2000

"A Kleene analysis of mobile ambients"
Nielson F. Ries Nielson, H., and Sagiv M. in ESOP 2000

"TVLA: A System for Implementing Static Analyses"
Lev-Ami T. and Sagiv M. in SAS 2000

"Parametric Shape Analysis via 3-Valued Logic"
Sagiv, M., Reps, T., and Wilhelm, R. in POPL 1999

"Parametric shape analysis via 3-valued logic"
Sagiv, M., Reps, T., and Wilhelm, R. TR-1383 1998