Program Verification with Constrained Horn Clauses (Invited Paper)
Arie Gurfinkel
Abstract
Abstract Many problems in program verification, Model Checking, and type inference are naturally expressed as satisfiability of a verification condition expressed in a fragment of First-Order Logic called Constrained Horn Clauses (CHC). This transforms program analysis and verification tasks to the realm of first order satisfiability and into the realm of SMT solvers. In this paper, we give a brief overview of how CHCs capture verification problems for sequential imperative programs, and discuss CHC solving algorithm underlying the Spacer engine of SMT-solver Z3.
Topics & Concepts
Horn clauseComputer scienceSatisfiabilityProgramming languageBoolean satisfiability problemSatisfiability modulo theoriesFragment (logic)Formal verificationSolverType inferenceModel checkingAutomated theorem provingTheoretical computer scienceSoftware verificationInferenceAlgorithmPrologArtificial intelligenceSoftwareSoftware systemSoftware constructionFormal Methods in VerificationSoftware Testing and Debugging TechniquesLogic, programming, and type systems