The Bedwyr System for Model Checking over Syntactic Expressions. Bedwyr is a generalization of logic programming that allows model checking directly on syntactic expressions possibly containing bindings. This system, written in OCaml, is a direct implementation of two recent advances in the theory of proof search. The first is centered on the fact that both finite success and finite failure can be captured in the sequent calculus by incorporating inference rules for definitions that allow fixed points to be explored. As a result, proof search in such a sequent calculus can capture simple model checking problems as well as may and must behavior in operational semantics. The second is that higher-order abstract syntax is directly supported using term-level λ-binders and the ∇ quantifier. These features allow reasoning directly on expressions containing bound variables.

References in zbMATH (referenced in 23 articles )

Showing results 1 to 20 of 23.
Sorted by year (citations)

1 2 next

  1. Miller, Dale; Viel, Alexandre: The undecidability of proof search when equality is a logical connective (2022)
  2. Heath, Quentin; Miller, Dale: A proof theory for model checking (2019)
  3. Miller, Dale: Mechanized metatheory revisited (2019)
  4. Momigliano, Alberto; Pientka, Brigitte; Thibodeau, David: A case study in programming coinductive proofs: Howe’s method (2019)
  5. Ahn, Ki Yung; Horne, Ross; Tiu, Alwen: A characterisation of open bisimilarity using an intuitionistic modal logic (2017)
  6. Cheney, James; Momigliano, Alberto: (\alpha\mathrmCheck): a mechanized metatheory model checker (2017)
  7. Heath, Quentin; Miller, Dale: A proof theory for model checking: an extended abstract (2017)
  8. Miller, Dale: Proof checking and logic programming (2017)
  9. Tiu, Alwen; Nguyen, Nam; Horne, Ross: SPEC: an equivalence checker for security protocols (2016)
  10. Miller, Dale; Tiu, Alwen: Extracting proofs from tabled proof search (2013)
  11. Felty, Amy; Momigliano, Alberto: Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (2012)
  12. Gacek, Andrew; Miller, Dale; Nadathur, Gopalan: A two-level logic approach to reasoning about computations (2012)
  13. Tiu, Alwen; Momigliano, Alberto: Cut elimination for a logic with induction and co-induction (2012)
  14. Gacek, Andrew; Miller, Dale; Nadathur, Gopalan: Nominal abstraction (2011)
  15. Delzanno, Giorgio; Giacobazzi, Roberto; Ranzato, Francesco: Static analysis, abstract interpretation and verification in (constraint logic) programming (2010)
  16. Schack-Nielsen, Anders; Schürmann, Carsten: Curry-style explicit substitutions for the linear and affine lambda calculus (2010)
  17. Baelde, David: On the expressivity of minimal generic quantification (2009)
  18. Dunfield, Joshua; Pientka, Brigitte: Case analysis of higher-order data (2009)
  19. Gacek, Andrew; Miller, Dale; Nadathur, Gopalan: Reasoning in Abella about structural operational semantics specifications (2009)
  20. Miller, Dale: Formalizing operational semantic specifications in logic (2009)

1 2 next