• GHC

  • Referenced in 43 articles [sw23765]
  • Guarded Horn clauses. The thesis introduces the programming language Guarded Horn Clauses which is abbreviated ... Guarded Horn Clauses was born from the examination of existing logic programming languages and logic ... resolution-based theorem prover for Horn-clause sentences. The restriction has two aspects ... additional syntactic construct, guard. Although Guarded Horn Clauses can be classified into the family...
  • ProVerif

  • Referenced in 43 articles [sw06558]
  • representation of the protocol by Horn clauses. Its main features are: It can handle many...
  • SeaHorn

  • Referenced in 19 articles [sw18274]
  • interpretation for verification, and (d) uses Horn-clauses as an intermediate language to represent verification ... with multiple verification tools based on Horn-clauses. SeaHorn provides users with a powerful verification...
  • Teyjus

  • Referenced in 17 articles [sw21364]
  • that significantly extends the theory of Horn clauses. A systematic exploitation of features...
  • Akiss

  • Referenced in 15 articles [sw20605]
  • using a saturation procedure that performs Horn clause resolution with selection...
  • HSF

  • Referenced in 12 articles [sw09937]
  • Software Verifier based on Horn Clauses. SF is a framework that automates verification of programs...
  • Hornlog

  • Referenced in 6 articles [sw21362]
  • graph-based interpreter for general Horn clauses. In this very interesting paper a new method ... showing the unsatisfiability of ground Horn clauses. The method (called Hornlog) applies to a class ... consists of what are normally called Horn clauses, but is still strictly included ... first-order formulas. In particular, negative Horn clauses can be used as assertions and also...
  • RAHFT

  • Referenced in 6 articles [sw24485]
  • RAHFT: A tool for verifying Horn clauses using abstract interpretation and finite tree automata ... present Rahft (Refinement of Abstraction in Horn clauses using Finite Tree automata), an abstraction refinement ... safety properties of programs expressed as Horn clauses. The paper describes the architecture, strength ... verification techniques and tools developed for Horn clauses...
  • VeriMAP

  • Referenced in 11 articles [sw22866]
  • VeriMAP: Transformation-aided Horn Clause Verification. VeriMAP is a tool for supporting CHC software verifiers...
  • PARTHENON

  • Referenced in 8 articles [sw25434]
  • parallel theorem prover for non-horn clauses. The paper describes a parallel resolution theorem prover...
  • EXPANDER

  • Referenced in 6 articles [sw22715]
  • Gentzen clauses or sets of guarded Horn clauses (cf. Chapter 2). The system provides...
  • I-SATCHMO

  • Referenced in 6 articles [sw06622]
  • consequence of a non-Horn clause is unnecessary if one of its consequent atoms...
  • TreeAutomizer

  • Referenced in 3 articles [sw40819]
  • satisfiability of sets of constrained Horn clauses. Constrained Horn clauses (CHC) are a fragment...
  • Code2Inv

  • Referenced in 1 article [sw41066]
  • programs, and a Constrained Horn Clause (CHC) solver...
  • Nuprl-Light

  • Referenced in 1 article [sw31982]
  • theorem prover, Nuprl-Light uses generalized Horn clauses for logical specification. Indeed, specifications in Nuprl...
  • eThor

  • Referenced in 1 article [sw41978]
  • bytecode semantics based on Horn clauses. In particular, our static analysis supports reachability properties, which...
  • CLIN

  • Referenced in 6 articles [sw19618]
  • CLIN-S is an instance-based, clause-form first-order theorem prover. CLIN-S employs ... proof search and performs well on non-Horn parts of the proofs involving small literals ... Horn parts of the proofs. A semantic structure for the input clauses is given...
  • MGTP

  • Referenced in 7 articles [sw09701]
  • Horn magic set to suppress the generation of useless model candidates caused by irrelevant clauses...
  • Propositional Resolution

  • Referenced in 1 article [sw28841]
  • refinement is complete only for clause sets that are Horn- renamable). We also define ... establish its soundness and completeness. The clause sets are not assumed to be finite...
  • Coq

  • Referenced in 1890 articles [sw00161]
  • Coq is a formal proof management system. It...