Combining model checking and data-flow analysis
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 1701764 (Why is no real title available?)
- scientific article; zbMATH DE number 1701765 (Why is no real title available?)
- scientific article; zbMATH DE number 3874579 (Why is no real title available?)
- scientific article; zbMATH DE number 5542185 (Why is no real title available?)
- scientific article; zbMATH DE number 50149 (Why is no real title available?)
- scientific article; zbMATH DE number 3548373 (Why is no real title available?)
- scientific article; zbMATH DE number 1324833 (Why is no real title available?)
- scientific article; zbMATH DE number 1953274 (Why is no real title available?)
- scientific article; zbMATH DE number 944097 (Why is no real title available?)
- scientific article; zbMATH DE number 2087560 (Why is no real title available?)
- scientific article; zbMATH DE number 1903378 (Why is no real title available?)
- scientific article; zbMATH DE number 5254145 (Why is no real title available?)
- A combination framework for tracking partition sizes
- Abstractions from proofs
- An abstract domain to infer ordinal-valued ranking functions
- Assertion Checking Unified
- Compositional shape analysis by means of bi-abduction
- Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
- Constraint-Based Approach for Analysis of Hybrid Systems
- Constraint-Based Invariant Inference over Predicate Abstraction
- Continuity analysis of programs
- Counterexample-guided abstraction refinement for symbolic model checking
- Deriving invariants by algorithmic learning, decision procedures, and predicate abstraction
- From program verification to program synthesis
- Generating data flow analysis algorithms from modal specifications
- Global Data Flow Analysis and Iterative Algorithms
- Global optimization by suppression of partial redundancies
- Graph-Based Algorithms for Boolean Function Manipulation
- Information reuse for multi-goal reachability analyses
- Intertwined forward-backward reachability analysis using interpolants
- Invariant Synthesis for Combined Theories
- Lazy abstraction
- Lifting abstract interpreters to quantified logical domains
- Linear ranking for linear lasso programs
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Non-linear loop invariant generation using Gröbner bases
- Orion: High-Precision Methods for Static Error Analysis of C and C++ Programs
- Precise interprocedural analysis through linear algebra
- Program verification as probabilistic inference
- Programming Languages and Systems
- Property-oriented expansion
- Semantics of context-free languages
- Static Analysis
- Static Analysis
- Systematic design of program transformation frameworks by abstract interpretation
- Types and programing languages
- Verification, Model Checking, and Abstract Interpretation
Cited in
(14)- Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
- Predicate abstraction for program verification
- Interpolation and SAT-based model checking revisited: adoption to software verification
- A framework for combining analysis and verification
- Verification by gambling on program slices
- Software Model Checking for Mobile Security – Collusion Detection in $$\mathbb {K}$$K
- Extending Model Checking with Dynamic Analysis
- Generating data flow analysis algorithms from modal specifications
- Combining Model Checking and Deduction
- Verifying data- and control-oriented properties combining static and runtime verification: theory and tools
- Upper bound computation of information leakages for unbounded recursion
- From under-approximations to over-approximations and back
- Towards efficient data-flow test data generation
- Syntactic and semantic soundness of structural dataflow analysis
Describes a project that uses
Uses Software
This page was built for publication: Combining model checking and data-flow analysis
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3176374)
