swMATH9878MaRDI QIDQ21857FDOQ21857
Author name not available (Why is that?)
Official website: http://www.cs.tau.ac.il/~tvla/
Cited In (39)
- Loop summarization using state and transition invariants
- Heap Decomposition for Concurrent Shape Analysis
- Scalable Shape Analysis for Systems Code
- Verifying Heap-Manipulating Programs in an SMT Framework
- Verify heaps via unified model checking
- Title not available (Why is that?)
- Title not available (Why is that?)
- Local higher-order fixpoint iteration
- Programming Languages and Systems
- On the almighty wand
- A generic framework for heap and value analyses of object-oriented programming languages
- Reasoning about sequences of memory states
- A Shape Analysis for Non-linear Data Structures
- Bounded quantifier instantiation for checking inductive invariants
- Semantic-directed clumping of disjunctive abstract states
- Thread Quantification for Concurrent Shape Analysis
- A Reachability Predicate for Analyzing Low-Level Software
- A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs
- Consit
- SPEED
- GENA
- FixBag
- CSSV
- VeriCon
- Title not available (Why is that?)
- MemCAD
- Cibai
- Title not available (Why is that?)
- Back to the future, revisiting precise program verification using SMT solvers
- Shape Analysis for Composite Data Structures
- Title not available (Why is that?)
- Automatic inference of access permissions
- Beyond Shapes: Lists with Ordered Data
- A logic of reachable patterns in linked data-structures
- Computer Aided Verification
- Finding Concurrency-Related Bugs Using Random Isolation
- Translating Java for multiple model checkers: The Bandera back-end
- Static Analysis
- Specialized 3-Valued Logic Shape Analysis Using Structure-Based Refinement and Loose Embedding
This page was built for software: TVLA
