On recursion-free Horn clauses and Craig interpolation
type: Item
instance of: scholarly article
title: On recursion-free Horn clauses and Craig interpolation
zbMATH Open document ID: 1322.68134
author: Philipp Rümmer
author: Hossein Hojjat
author: Viktor Kuncak
published in: Formal Methods in System Design
publication date: 2015-10-20T00:00:00Z
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03C40
zbMATH DE Number: 6496662
zbMATH Keywords: Horn clause verification
zbMATH Keywords: interpolation
zbMATH Keywords: software verification
zbMATH Keywords: SMT solver
zbMATH Keywords: software model checking
zbMATH Keywords: predicate abstraction
describes a project that uses: Spacer
describes a project that uses: Princess
describes a project that uses: HMC
MaRDI profile type: Publication
full work available at URL: s10703-014-0219-7
OpenAlex ID: W1979348329
cites work: Whale: An Interpolation-Based Algorithm for Inter-procedural Verification
cites work: Q4472235
cites work: Analysis of Linear Hybrid Systems in CLP
cites work: Q5015366
cites work: An interpolating sequent calculus for quantifier-free Presburger arithmetic
cites work: Efficient generation of craig interpolants in satisfiability modulo theories
cites work: Linear reasoning. A new form of the Herbrand-Gentzen theorem
cites work: Synthesis of Circular Compositional Program Proofs via Abduction
cites work: Generalization strategies for the verification of infinite state systems
cites work: Analysis of Boolean Programs
cites work: Predicate abstraction and refinement for verifying multi-threaded programs
cites work: Q4997234
cites work: Logic-based program synthesis and transformation. 18th international symposium, LOPSTR 2008, Valencia, Spain, July 17--18, 2008. Revised selected papers
cites work: Nested interpolants
cites work: Abstractions from proofs
cites work: Generalized Property Directed Reachability
cites work: Accelerating Interpolants
cites work: Q4997236
cites work: SMT-based model checking for recursive programs
cites work: Computer Aided Verification
cites work: Lazy Abstraction with Interpolants
cites work: A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs
cites work: Computer aided verification. 25th international conference, CAV 2013, Saint Petersburg, Russia, July 13--19, 2013. Proceedings
cites work: Dependent types from counterexamples
cites work: Automating relatively complete verification of higher-order functional programs
DOI: 10.1007/S10703-014-0219-7
description: scientific article; zbMATH DE number 6496662