Skip to main content

2000 | OriginalPaper | Buchkapitel

TVLA: A System for Implementing Static Analyses

verfasst von : Tal Lev-Ami, Mooly Sagiv

Erschienen in: Static Analysis

Verlag: Springer Berlin Heidelberg

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Metadaten
Titel
TVLA: A System for Implementing Static Analyses
verfasst von
Tal Lev-Ami
Mooly Sagiv
Copyright-Jahr
2000
Verlag
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/978-3-540-45099-3_15

Premium Partner