Combining Model Checking and Data-Flow Analysis
From MaRDI portal
Publication:3176374
DOI10.1007/978-3-319-10575-8_16zbMath1392.68231MaRDI QIDQ3176374
Sumit Gulwani, Dirk Beyer, David A. Schmidt
Publication date: 20 July 2018
Published in: Handbook of Model Checking (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-10575-8_16
68Q60: Specification and verification (program logics, model checking, etc.)
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Related Items
Software Model Checking for Mobile Security – Collusion Detection in $$\mathbb {K}$$K, Upper bound computation of information leakages for unbounded recursion, Verification by gambling on program slices, Predicate Abstraction for Program Verification
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Generating data flow analysis algorithms from modal specifications
- Program verification as probabilistic inference
- Lifting abstract interpreters to quantified logical domains
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Abstractions from proofs
- Non-linear loop invariant generation using Gröbner bases
- Precise interprocedural analysis through linear algebra
- Counterexample-guided abstraction refinement for symbolic model checking
- Constraint-Based Approach for Analysis of Hybrid Systems
- Orion: High-Precision Methods for Static Error Analysis of C and C++ Programs
- Constraint-Based Invariant Inference over Predicate Abstraction
- Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction
- Graph-Based Algorithms for Boolean Function Manipulation
- Global Data Flow Analysis and Iterative Algorithms
- Global optimization by suppression of partial redundancies
- Property-oriented expansion
- Linear Ranking for Linear Lasso Programs
- Lazy abstraction
- Systematic design of program transformation frameworks by abstract interpretation
- Continuity analysis of programs
- From program verification to program synthesis
- A combination framework for tracking partition sizes
- Compositional shape analysis by means of bi-abduction
- Information Reuse for Multi-goal Reachability Analyses
- Intertwined Forward-Backward Reachability Analysis Using Interpolants
- An Abstract Domain to Infer Ordinal-Valued Ranking Functions
- Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
- Assertion Checking Unified
- Invariant Synthesis for Combined Theories
- Static Analysis
- Static Analysis
- Semantics of context-free languages
- Programming Languages and Systems
- Verification, Model Checking, and Abstract Interpretation
