Horn Clause Solvers for Program Verification

DOI10.1007/978-3-319-23534-9_2zbMath1465.68044OpenAlexW2293809538MaRDI QIDQ2947164

Nikolaj Bjørner, Arie Gurfinkel, K. L. McMillan, Andrey Rybalchenko

Publication date: 22 September 2015

Published in: Fields of Logic and Computation II (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-23534-9_2

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Verifying Catamorphism-Based Contracts using Constrained Horn Clauses, Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays, A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic, Symbol elimination and applications to parametric entailment problems, On the copy complexity of width 3 Horn constraint systems, Constraint-based relational verification, Decision tree learning in CEGIS-based termination analysis, Progress in certifying hardware model checking results, A tree-based approach to data flow proofs, Toward neural-network-guided program synthesis and verification, Symbolic automatic relations and their applications to SMT and CHC solving, Exact and parameterized algorithms for read-once refutations in Horn constraint systems, Loop verification with invariants and contracts, Solving Horn Clauses on Inductive Data Types Without Induction, Automatic synthesis of logical models for order-sorted first-order theories, Leveraging Horn clause solving for compositional verification of PLC software, Analyzing read-once cutting plane proofs in Horn systems, Computing Abstract Distances in Logic Programs, Analysis and Transformation of Constrained Horn Clauses for Program Verification, Parameterized recursive refinement types for automated program verification, Towards a dereversibilizer: fewer asserts, statically, Efficient modular SMT-based model checking of pointer programs, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories, Introduction to the special issue on computational logic for verification, Predicate Pairing for program verification, Tree dimension in verification of constrained Horn clauses, Fold/Unfold Transformations for Fixpoint Logic, Proof Relevant Corecursive Resolution, Incremental and Modular Context-sensitive Analysis, Counterexample-guided prophecy for model checking modulo the theory of arrays, ICE-based refinement type discovery for higher-order functional programs, Abstraction refinement and antichains for trace inclusion of infinite state systems, Efficient Reasoning for Inconsistent Horn Formulae, On the lengths of tree-like and dag-like cutting plane refutations of Horn constraint systems. Horn constraint systems and cutting plane refutations, Removing algebraic data types from constrained Horn clauses using difference predicates, Subsumption demodulation in first-order theorem proving, Reasoning in the theory of heap: satisfiability and interpolation

Uses Software

• SMT-LIB
• ESC/Java
• Boogie
• HMC
• SeaHorn
• Spacer
• Datalog
• VeriMAP
• Refal
• Booster

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Reasoning about procedures as parameters in the language L4
• Efficient weakest preconditions
• Complexity, convexity and combinations of theories
• Property-directed inference of universal invariants or proving their absence
• Superposition as a decision procedure for timed automata
• Generalized Property Directed Reachability
• Resourceful Reachability as HORN-LA
• An overview of Ciao and its design philosophy
• Separation Logic Modulo Theories
• SAT-Based Model Checking without Unrolling
• Some characterization theorems for infinitary universal Horn logic without equality
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Booster: An Acceleration-Based Verification Framework for Array Programs
• Model Checking Recursive Programs with Exact Predicate Abstraction
• Temporal Verification of Reactive Systems: Response
• The concept of a supercompiler
• The Semantics of Predicate Logic as a Programming Language
• A Transformation System for Developing Recursive Programs
• Soundness and Completeness of an Axiom System for Program Verification
• Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Accelerating Interpolants
• Synthesis and transformation of logic programs using unfold/fold proofs
• Precise interprocedural dataflow analysis with applications to constant propagation
• Property Directed Polyhedral Abstraction
• Low-level liquid types
• A type-directed abstraction refinement approach to higher-order model checking
• A constraint-based approach to solving games on infinite graphs
• An axiomatic basis for computer programming
• Inadequacy of computable loop invariants
• On sentences which are true of direct unions of algebras