Invariant Synthesis for Combined Theories

DOI10.1007/978-3-540-69738-1_27zbMath1132.68333OpenAlexW1711276981MaRDI QIDQ5452621

Andrey Rybalchenko, Rupak Majumdar, Dirk Beyer, Thomas A. Henzinger

Publication date: 4 April 2008

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

Full work available at URL: http://edoc.mpg.de/356708

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Verifying Array Manipulating Programs with Full-Program Induction, Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data, \textsc{Diffy}: inductive reasoning of array programs using difference invariants, Guiding Craig interpolation with domain-specific abstractions, SAT-Based Model Checking, Combining Model Checking and Data-Flow Analysis, What else is undecidable about loops?, A unifying view on SMT-based software verification, An extension of lazy abstraction with interpolation for programs with arrays, An array content static analysis based on non-contiguous partitions, From invariant checking to invariant inference using randomized search, Verification and falsification of programs with loops using predicate abstraction, Loop invariants, Inferring Loop Invariants Using Postconditions, Hierarchical Reasoning for the Verification of Parametric Systems, An Assume Guarantee Approach for Checking Quantified Array Assertions, Speeding up the Constraint-Based Method in Difference Logic, On invariant synthesis for parametric systems, Abstraction Refinement for Quantified Array Assertions

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Model theory.
• Non-linear loop invariant generation using Gröbner bases
• Lazy abstraction
• Automated Deduction – CADE-20
• Static Analysis
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Computer Aided Verification