Bedwyr is a generalization of logic programming that allows model checking directly on syntactic expression possibly containing bindings. This system, written in OCaml, is a direct implementation of two recent advances in the theory of proof search.
The distributed system comes with several example applications, including the finite pi-calculus (operational semantics, bisimulation, trace analyses, and modal logics), the spi-calculus (operational semantics), value-passing CCS, the lambda-calculus, winning strategies for games, and various other model checking problems.
While the system has been written to validate certain theoretic results and to help suggest new theoretical directions, we believe that the system can be of use to others interested more in reasoning about computer systems than about proof theory foundations.
Bedwyr is an open source project. Two major versions have been released (v1.0 on 1 Nov 2006 and v1.1 on 12 Feb 2007). We welcome contributions from others of example applications and new features. The developers behind the current distribution are:
The team thanks Brigitte Pientka, for her advices regarding tabling, and Axelle Ziegler, for her help in translating an early implementation from SML to OCaml. Much of the effort for this work is supported within the context of the Slimmer project, which is supported by funds from INRIA and NSF. Support has also been provided by the NSF Grant OISE-0553462 (IRES-REUSSI). Of course, the opinions, findings, and conclusions or recommendations expressed in this material are those of the project participants and do not necessarily reflect the views of INRIA or the National Science Foundation.
Documentation: The Bedwyr User's Guide is available in pdf, ps or html.
Download: Get the latest version of Bedwyr's source code.
Open source repository: Active development versions are available from the Bedwyr subversion repository hosted by INRIA's Gforge. You can browse the repository, especially the examples.
Some relevant publications: