Bedwyr
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.
Keywords for this software
References in zbMATH (referenced in 15 articles )
Showing results 1 to 15 of 15.
Sorted by year (- Felty, Amy; Momigliano, Alberto: Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (2012)
- Gacek, Andrew; Miller, Dale; Nadathur, Gopalan: A two-level logic approach to reasoning about computations (2012)
- Tiu, Alwen; Momigliano, Alberto: Cut elimination for a logic with induction and co-induction (2012)
- Gacek, Andrew; Miller, Dale; Nadathur, Gopalan: Nominal abstraction (2011)
- Delzanno, Giorgio; Giacobazzi, Roberto; Ranzato, Francesco: Static analysis, abstract interpretation and verification in (constraint logic) programming (2010)
- Schack-Nielsen, Anders; Schürmann, Carsten: Curry-style explicit substitutions for the linear and affine lambda calculus (2010)
- Baelde, David: On the expressivity of minimal generic quantification. (2009)
- Baelde, David: On the expressivity of minimal generic quantification (2009)
- Dunfield, Joshua; Pientka, Brigitte: Case analysis of higher-order data. (2009)
- Dunfield, Joshua; Pientka, Brigitte: Case analysis of higher-order data (2009)
- Gacek, Andrew; Miller, Dale; Nadathur, Gopalan: Reasoning in Abella about structural operational semantics specifications (2009)
- Gacek, Andrew; Miller, Dale; Nadathur, Gopalan: Reasoning in abella about structural operational semantics specifications. (2009)
- Miller, Dale: Formalizing operational semantic specifications in logic (2009)
- Miller, Dale: Formalizing operational semantic specifications in logic (2009)
- Baelde, David; Miller, Dale: Least and greatest fixed points in linear logic (2007)