Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Journal articles
  4. On recursion-free Horn clauses and Craig interpolation
 
research article

On recursion-free Horn clauses and Craig interpolation

Rummer, Philipp
•
Hojjat, Hossein  
•
Kuncak, Viktor  orcid-logo
2015
Formal Methods In System Design

One of the main challenges in software verification is efficient and precise analysis of programs with procedures and loops. Interpolation methods remain among the most promising techniques for such verification. To accommodate the demands of various programming language features, over the past years several extended forms of interpolation have been introduced. We give a precise ontology of such extended interpolation methods, and investigate the relationship between interpolation and fragments of constrained recursion-free Horn clauses. We also introduce a new notion of interpolation, disjunctive interpolation, which solves a more general class of problems in one step compared to previous notions of interpolants, such as tree interpolants or inductive sequences of interpolants. We present algorithms and complexity for construction of interpolants, as well as the corresponding decision problems for recursion-free Horn fragments. Finally, we give an extensive empirical evaluation using a solver for (recursive) Horn problems, in particular comparing the performance of tree interpolation and disjunctive interpolation for constraints modelling software verification tasks.

  • Details
  • Metrics
Type
research article
DOI
10.1007/s10703-014-0219-7
Web of Science ID

WOS:000361484000001

Author(s)
Rummer, Philipp
Hojjat, Hossein  
Kuncak, Viktor  orcid-logo
Date Issued

2015

Publisher

Springer

Published in
Formal Methods In System Design
Volume

47

Issue

1

Start page

1

End page

25

Subjects

Horn clause verification

•

Interpolation

•

Software verification

•

SMT solver

•

Software model checking

•

Predicate abstraction

Editorial or Peer reviewed

REVIEWED

Written at

EPFL

EPFL units
LARA  
Available on Infoscience
December 2, 2015
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/120948
Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés