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.
New December 2014: some recent work on describing proof certificates for model checking.
Bedwyr is an open source project. We welcome contributions from others of example applications and new features. The developers behind the current distribution are:
The development is currently centered in the Parsifal team. David, Andrew and Quentin did most of the coding. Theoretical and design topics were contributed also by Alwen and Dale, and Gopalan contributed to the initial version of ndcore.
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 was initially supported within the context of the Slimmer project, which was funded by INRIA and NSF (Grant CCR-0429572), and by the NSF Grant OISE-0553462 (IRES-REUSSI). It is now supported by the BATT ADT effort, another INRIA grant. 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.
The latest stablish release is version 1.4-beta1 (January 2015).
The SVN repository hosted on INRIAGforge offers a read-only access to the complete development sources. You can browse the repository, especially the example files.
The sources are currently known to not work on OSX or BSD.
Some tarballs are available for some past releases. They contain the files needed to build the programs and the documentation, but lack the files needed by maintainers. Precompiled binaries are also provided for those releases.
Some packages, containing both versions of the program (native and bytecode), the complete documentation, all examples and some language files for Emacs and Vim, are available for GNU/Linux (Debian testing and Gentoo) and Windows 8. The Linux packages also include the standalone core library ndcore for development purposes.
/etc/apt/sources.list.d/slimmer.listcontaining the line
deb http://slimmer.gforge.inria.fr/releases/debian/ jessie main
apt-key add heath.asc
apt-get update, then
apt-get install bedwyr bedwyr-doc
layman -a dawan
/var/lib/layman/make.confis sourced by
C:\Program Files (x86)\Slimmer\Bedwyr, along with examples and an uninstaller.
Includes a user guide, a system description and examples.
Last modifed: October 2014.