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
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
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
This page was built for publication: Transformation-Enabled Precondition Inference
