On recursion-free Horn clauses and Craig interpolation

DOI10.1007/S10703-014-0219-7zbMATH Open1322.68134OpenAlexW1979348329MaRDI QIDQ746767FDOQ746767

Authors: Philipp Rümmer, Hossein Hojjat, Viktor Kuncak 

Publication date: 20 October 2015

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-014-0219-7

Recommendations

• Generalised interpolation by solving recursion-free Horn clauses
• Constraint Solving for Interpolation
• Constraint solving for interpolation
• Propositional Interpolation and Abstract Interpretation
• Complete instantiation-based interpolation

zbMATH Keywords

interpolationsoftware verificationpredicate abstractionSMT solverHorn clause verificationsoftware model checking

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Interpolation, preservation, definability (03C40)

Cites Work

• Nested interpolants
• Interpolation and SAT-based model checking.
• Efficient generation of Craig interpolants in satisfiability modulo theories
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Abstractions from proofs
• An interpolating sequent calculus for quantifier-free Presburger arithmetic
• Generalised interpolation by solving recursion-free Horn clauses
• Lazy Abstraction with Interpolants
• On recursion-free Horn clauses and Craig interpolation
• Generalized property directed reachability
• Accelerating interpolants
• Synthesis of circular compositional program proofs via abduction
• Computer aided verification. 25th international conference, CAV 2013, Saint Petersburg, Russia, July 13--19, 2013. Proceedings
• Title not available (Why is that?)
• Whale: an interpolation-based algorithm for inter-procedural verification
• SMT-based model checking for recursive programs
• Predicate abstraction and refinement for verifying multi-threaded programs
• Logic-based program synthesis and transformation. 18th international symposium, LOPSTR 2008, Valencia, Spain, July 17--18, 2008. Revised selected papers
• Automating relatively complete verification of higher-order functional programs
• Analysis of Linear Hybrid Systems in CLP
• Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification
• Efficient CTL verification via Horn constraints solving
• Dependent types from counterexamples
• Generalization strategies for the verification of infinite state systems
• Analysis of Boolean Programs
• A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs

Cited In (10)

• Inferring simple solutions to recursion-free Horn clauses via sampling
• Title not available (Why is that?)
• Case-free programs: An abstraction of definite horn programs
• Whale: an interpolation-based algorithm for inter-procedural verification
• Exploiting partial variable assignment in interpolation-based model checking
• Proof tree preserving tree interpolation
• Guiding Craig interpolation with domain-specific abstractions
• On recursion-free Horn clauses and Craig interpolation
• Generalised interpolation by solving recursion-free Horn clauses
• Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT

Uses Software

• Princess
• HMC
• Spacer

This page was built for publication: On recursion-free Horn clauses and Craig interpolation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q746767)