Transformation-Enabled Precondition Inference
From MaRDI portal
Publication:6063861
DOI10.1017/s1471068421000272zbMath1530.68065arXiv2108.03178MaRDI QIDQ6063861
Peter J. Stuckey, Harald Søndergaard, Bishoksan Kafle, Peter Schachte, Graeme Gange
Publication date: 12 December 2023
Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2108.03178
03B70: Logic in computer science
68Q60: Specification and verification (program logics, model checking, etc.)
68N17: Logic programming
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Cites Work
- Unnamed Item
- Unnamed Item
- Horn clause verification with convex polyhedral abstraction and tree automata-based refinement
- The octagon abstract domain
- Affine relationships among variables of a program
- Refinement of trace abstraction for real-time programs
- Dual analysis for proving safety and finding bugs
- Necessary and Sufficient Preconditions via Eager Abstraction
- An overview of Ciao and its design philosophy
- TRACER: A Symbolic Execution Tool for Verification
- Non-linear loop invariant generation using Gröbner bases
- Abstract interpretation and application to logic programs
- An iterative approach to precondition inference using constrained Horn clauses
- Abstract multiple specialization and its application to program parallelization
- Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis
- Inferring Sufficient Conditions with Backward Polyhedral Under-Approximations
- Combining Forward and Backward Abstract Interpretation of Horn Clauses
- Synthesis of Circular Compositional Program Proofs via Abduction
- Sufficient Preconditions for Modular Assertion Checking
- Automatically Refining Abstract Interpretations
- Program Development in Computational Logic
