TVLA: A system for implementing static analyses

DOI10.1007/978-3-540-45099-3_15MaRDI QIDQ2722067zbMATH OpenFDO

Authors Tal Lev-Ami, Mooly Sagiv

Publication date 11 July 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-45099-3_15

Mathematics Subject Classification ID

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

Recommendations

• Computer Aided Verification
• scientific article; zbMATH DE number 1948397
• Tools and Algorithms for the Construction and Analysis of Systems
• Rewriting Approximations for Fast Prototyping of Static Analyzers
• scientific article; zbMATH DE number 2087567

Cited in

(28)

• Verify heaps via unified model checking
• Local higher-order fixpoint iteration
• TVLA
• Multilevel static analysis for improving program quality
• Loop summarization using state and transition invariants
• A logic of reachable patterns in linked data-structures
• A generic framework for heap and value analyses of object-oriented programming languages
• On the key dependent message security of the Fujisaki-Okamoto constructions
• Automatic inference of access permissions
• Sawja: static analysis workshop for Java
• Static analysis of PostScript code
• Bounded quantifier instantiation for checking inductive invariants
• Verifying Heap-Manipulating Programs in an SMT Framework
• On the Almighty Wand
• Beyond Shapes: Lists with Ordered Data
• On the almighty wand
• scientific article; zbMATH DE number 1948397 (Why is no real title available?)
• Interprocedural shape analysis for effectively cutpoint-free programs
• scientific article; zbMATH DE number 7455743 (Why is no real title available?)
• Computer Aided Verification
• An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures
• The Spotlight Principle
• Static analysis for syntax objects
• A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs
• Parameterized recursive refinement types for automated program verification
• Reasoning about sequences of memory states
• Bit-vector typestate analysis
• Translating Java for multiple model checkers: The Bandera back-end

This page was built for publication: TVLA: A system for implementing static analyses

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2722067)