Lev-Ami, Tal; Sagiv, Mooly 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]. Cited in 20 Documents 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 \textit{T. Lev-Ami} and \textit{M. Sagiv}, Lect. Notes Comput. Sci. 1824, 280--301 (2000; Zbl 0966.68580)