Bedwyr:
A proof search approach to model checking

Overview

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.

1. It is possible to capture both finite success and finite failure in a sequent calculus. Proof search in such a proof system can capture both may and must behavior in operational semantics.
2. Higher-order abstract syntax is directly supported using term-level lambda-binders, the nabla-quantifier, higher-order pattern unification, and explicit substitutions. These features allow reasoning directly on expressions containing bound variables.

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.

Current developers

Bedwyr is an open source project. We welcome contributions from others of example applications and new features. The developers behind the current distribution are:

• David Baelde (LSV, ENS Cachan)
• Andrew Gacek (Rockwell Collins)
• Dale Miller & Quentin Heath (Parsifal, INRIA & LIX/Ecole Polytechnique)
• Gopalan Nadathur (University of Minnesota)
• Alwen Tiu (Australian National University).

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.

Download

The latest stablish release is version 1.4-alpha9 (April 2013).

SCM
The SVN repository hosted on INRIAGforge offers a read-only access to the complete development sources. You can browse the repository, especially the examples.

Binaries & Tarballs
Some tarballs are available for all 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.

Packages
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.

• The Debian packages exist for i386 and amd64 and are designed for the current testing (Wheezy), but might just work for other versions or even derivatives such as Ubuntu:
  • create (as root) the file /etc/apt/sources.list.d/slimmer.list containing deb http://slimmer.gforge.inria.fr/releases/debian/ wheezy main
  • download this public PGP key (note: the old 9678A222 has been revoked, this one should be 40565E01) and add it to your APT keyring by running (as root) apt-key add heath.asc
  • run apt-get update, then apt-get install bedwyr bedwyr-doc
  • brose /usr/share/bedwyr/examples
• The Gentoo package, for ~x86 and ~amd64, is in the overlay dawan:
  • emerge layman and run layman -a dawan
  • make sure that /var/lib/layman/make.conf is sourced by /etc/portage/make.conf
  • emerge sci-mathematics/bedwyr (dev-lang/ocaml will be part of the dependencies)
• The Windows package is a full-featured (although simple) installer that should work on Windows Vista, 7 and 8, 32 or 64 bits. It installs the program in C:\Program Files (x86)\Slimmer\Bedwyr, along with examples and an uninstaller.

Documentation

A User Guide to Bedwyr v1.3 [html]

Links

Publications: the Bedwyr system and underlying theory

1. The Bedwyr system for model checking over syntactic expressions by David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and Alwen Tiu. CADE 2007: 21th Conference on Automated Deduction, Frank Pfenning, editor, LNAI 4603, pages 391-397. Springer, 2007. (pdf)
2. A proof theory for generic judgments by Dale Miller and Alwen Tiu. ACM Trans. on Computational Logic, 6(4):749-783, October 2005. (pdf).
3. Mixing Finite Success and Finite Failure in an Automated Prover, by Alwen Tiu and Gopalan Nadathur and Dale Miller (pdf). Appears in ESHOL'05: Empirically Successful Automated Reasoning in Higher-Order Logics, 2 December (conference proceedings).

Publications: Applications of Bedwyr

1. Model checking for pi-calculus using proof search by Alwen Tiu. In Proceedings of CONCUR 2005, LNCS Vol. 3653, pages 36 - 50, Springer-Verlag, 2005. (pdf).
2. Proof Search Specifications of Bisimulation and Modal Logics for the π-calculus, by Alwen Tiu and Dale Miller. ACM Transactions on Computational Logic, 11(2), 2010. (pdf, arXiv)

Last modifed: 06 April 2013.