Invariants Synthesis over a Combined Domain for Automated Program Verification
From MaRDI portal
Publication:2842643
DOI10.1007/978-3-642-39698-4_19zbMath1390.68190OpenAlexW2162164173MaRDI QIDQ2842643
Shengchao Qin, Hongli Yang, Guanhua He, Wei-Ngan Chin
Publication date: 16 August 2013
Published in: Theories of Programming and Formal Methods (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-39698-4_19
Uses Software
Cites Work
- Unnamed Item
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- Loop invariant synthesis in a combined abstract domain
- Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data
- Back to the future
- Relational inductive shape analysis
- Verifying Heap-Manipulating Programs in an SMT Framework
- Scalable Shape Analysis for Systems Code
- Separating Shape Graphs
- Grammar Analysis and Parsing by Abstract Interpretation
- Interprocedural Shape Analysis with Separated Heap Abstractions
- BI as an assertion language for mutable data structures
- Role analysis
- Low-level liquid types
- Automatic numeric abstractions for heap-manipulating programs
- A combination framework for tracking partition sizes
- Compositional shape analysis by means of bi-abduction
- Region-based shape analysis with tracked locations
- Why3 — Where Programs Meet Provers
- Compositional Shape Analysis by Means of Bi-Abduction
- Calling context abstraction with shapes
- Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
- Automated Verification of Shape and Size Properties Via Separation Logic
- Tools and Algorithms for the Construction and Analysis of Systems
This page was built for publication: Invariants Synthesis over a Combined Domain for Automated Program Verification
