×

TVLA: A system for implementing static analyses. (English) Zbl 0966.68580

Palsberg, Jens (ed.), Static analysis. 7th internationales symposium, SAS 2000, Santa Barbara, CA, USA, June 29 - July 6, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1824, 280-301 (2000).
Summary: 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 auccessfully 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.
For the entire collection see [Zbl 0941.00028].

MSC:

68U99 Computing methodologies and applications
68T35 Theory of languages and software systems (knowledge-based systems, expert systems, etc.) for artificial intelligence
68P10 Searching and sorting

Software:

TVLA
PDFBibTeX XMLCite