On Local Reasoning in Verification
From MaRDI portal
Recommendations
Cites work
- Applications of hierarchical reasoning in the verification of complex systems
- Automated Deduction – CADE-20
- Automated reasoning in some local exensions of ordered structures
- Automatic recognition of tractability in inference relations
- Computer Aided Verification
- Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies
- Hierarchical and Modular Reasoning in Complex Theories: The Case of Local Theory Extensions
- scientific article; zbMATH DE number 3963900 (Why is no real title available?)
- Interpolation in Local Theory Extensions
- Modular proof systems for partial functions with Evans equality
- On Local Reasoning in Verification
- Polynomial Time Uniform Word Problems
- Polynomial-time computation via local inference relations
- Verification, Model Checking, and Abstract Interpretation
- Verifying CSP-OZ-DC Specifications with Complex Data Types and Timing Parameters
Cited in
(25)- Local soundness for QBF calculi
- Superposition decides the first-order logic fragment over ground theories
- Set of support, demodulation, paramodulation: a historical perspective
- Local reasoning about the presence of bugs: incorrectness separation logic
- On invariant synthesis for parametric systems
- Decision procedures for flat array properties
- 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
- scientific article; zbMATH DE number 1341465 (Why is no real title available?)
- On deciding satisfiability by theorem proving with speculative inferences
- 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
- Footprints in Local Reasoning
- On Hierarchical Reasoning in Combinations of Theories
- Hierarchical reasoning for the verification of parametric systems
- Complete instantiation-based interpolation
- On P-Interpolation in Local Theory Extensions and Applications to the Study of Interpolation in the Description Logics $$\mathcal{E}\mathcal{L}, \mathcal{E}\mathcal{L}^+$$
- On symbol elimination and uniform interpolation in theory extensions
- Symbol elimination and applications to parametric entailment problems
This page was built for publication: On Local Reasoning in Verification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5458332)