On Local Reasoning in Verification

DOI10.1007/978-3-540-78800-3_19zbMath1134.68410OpenAlexW1573267491MaRDI 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

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

Related Items

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

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