On Local Reasoning in Verification

DOI10.1007/978-3-540-78800-3_19zbMath1134.68410MaRDI QIDQ5458332

Viorica Sofronie-Stokkermans, Carsten Ihlemann, Swen Jacobs

Publication date: 11 April 2008

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-78800-3_19

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

Related Items

Constraint solving for finite model finding in SMT solvers, Locality Results for Certain Extensions of Theories with Bridging Functions, An Efficient Decision Procedure for Imperative Tree Data Structures, On Local Reasoning in Verification, Complete instantiation-based interpolation, On Hierarchical Reasoning in Combinations of Theories, Hierarchical Reasoning for the Verification of Parametric Systems, Decision procedures for flat array properties, On deciding satisfiability by theorem proving with speculative inferences, Symbol elimination and applications to parametric entailment problems, Superposition decides the first-order logic fragment over ground theories, Set of support, demodulation, paramodulation: a historical perspective, On invariant synthesis for parametric systems, On Interpolation and Symbol Elimination in Theory Extensions, On First-Order Model-Based Reasoning, Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata, Towards Complete Reasoning about Axiomatic Specifications, Decision Procedures for Automating Termination Proofs, Bounded Quantifier Instantiation for Checking Inductive Invariants, Towards SMT Model Checking of Array-Based Systems

Cites Work

• Unnamed Item
• Unnamed Item
• Modular proof systems for partial functions with Evans equality
• Applications of Hierarchical Reasoning in the Verification of Complex Systems
• Hierarchical and Modular Reasoning in Complex Theories: The Case of Local Theory Extensions
• Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies
• Verifying CSP-OZ-DC Specifications with Complex Data Types and Timing Parameters
• Interpolation in Local Theory Extensions
• Polynomial Time Uniform Word Problems
• Automatic recognition of tractability in inference relations
• Automated Deduction – CADE-20
• On Local Reasoning in Verification
• Computer Aided Verification
• Polynomial-time computation via local inference relations
• Verification, Model Checking, and Abstract Interpretation