Abstract
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. © Springer-Verlag Berlin Heidelberg 2000.
Cite
CITATION STYLE
Lev-Ami, T., & Sagiv, M. (2000). TVLA: A system for implementing static analyses. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1824 LNCS, pp. 280–302). Springer Verlag. https://doi.org/10.1007/978-3-540-45099-3_15
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
