An iterative approach to precondition inference using constrained Horn clauses

DOI10.1017/S1471068418000091zbMath1451.68075arXiv1804.05989OpenAlexW2962816164WikidataQ57664976 ScholiaQ57664976MaRDI QIDQ4559813

Harald Søndergaard, Peter J. Stuckey, Peter Schachte, Graeme Gange, Bishoksan Kafle, John P. Gallagher

Publication date: 4 December 2018

Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1804.05989

zbMATH Keywords

program transformationrefinementabstract interpretationbackwards analysisprecondition inferenceprogram specialisation

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (6)

Transformation-Enabled Precondition Inference ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ Resource Analysis driven by (Conditional) Termination Proofs ⋮ Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis ⋮ Unnamed Item ⋮ Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction*

Uses Software

• Yices
• Dagger
• PPL
• TRACER
• InvGen
• SeaHorn
• RAHFT

Cites Work

• Unnamed Item
• Computer aided verification. 24th international conference, CAV 2012, Berkeley, CA, USA, July 7--13, 2012. Proceedings
• Verification, model checking, and abstract interpretation. 12th international conference, VMCAI 2011, Austin, TX, USA, January 23--25, 2011. Proceedings
• Horn clause verification with convex polyhedral abstraction and tree automata-based refinement
• The octagon abstract domain
• Computer aided verification. 21st international conference, CAV 2009, Grenoble, France, June 26--July 2, 2009. Proceedings
• Static analysis. 5th international symposium, SAS '98, Pisa, Italy, September 14--16, 1998. Proceedings
• Tools and algorithms for the construction and analysis of systems. 19th international conference, TACAS 2013, held as part of the European joint conferences on theory and practice of software, ETAPS 2013, Rome, Italy, March 16--24, 2013. Proceedings
• Static analysis. 24th international symposium, SAS 2017, New York, NY, USA, August 30 -- September 1, 2017. Proceedings
• Reachability problems. 11th international workshop, RP 2017, London, UK, September 7--9, 2017. Proceedings
• Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Proceedings
• Verification, model checking, and abstract interpretation. 9th international conference, VMCAI 2008, San Francisco, USA, January 7--9, 2008. Proceedings
• An overview of Ciao and its design philosophy
• Counterexample-guided abstraction refinement for symbolic model checking
• Abstract interpretation and application to logic programs
• The semantics of constraint logic programs1Note that reviewing of this paper was handled by the Editor-in-Chief.1
• Inferring Sufficient Conditions with Backward Polyhedral Under-Approximations
• Program Development in Computational Logic
• Tools and Algorithms for the Construction and Analysis of Systems
• Integrated Formal Methods
• Computer aided verification. 9th international conference, CAV'97, Haifa, Israel, June 22--25, 1997. Proceedings

This page was built for publication: An iterative approach to precondition inference using constrained Horn clauses