Go Model Checker for MiGo types
Godel Checker is a model checker for MiGo types.
Run via Docker
There are many external dependencies in this tool, the easiest way to get started is to run via a Docker container.
The docker container contains all dependencies build with the latest version of
Godel, where the container is built from latest commits. Given an example cgo
file, for example:
Run the example with:
docker run -ti --rm -v /tmp:/root nickng/godel:latest Godel example.cgo # Model check docker run -ti --rm -v /tmp:/root nickng/godel:latest Godel -T example.cgo # Term check
-v /tmp:/root puts the
/tmp directory into the container as
/root, so the
example.cgo file is found in the container as
Alternatively, use the
docker-run script to run the examples:
cd /path/to/example; docker-run example.cgo
/path/to/example into docker and run the example inside the container,
all arguments are passed to the
Godel binary inside the container, e.g.
docker-run -T example.cgo # Term check
Development Environment via Docker
This is similar to above, except the
Godel binary in the current directory
will be used instead, so small modifications can be tested immediately. The
termination checker and its dependencies are in the container.
Build from scratch
Instructions to build from scratch can be found below.
There are three components:
Godel frontend, the model checker backend,
and the termination analyser backend.
Godel frontend is written in Haskell.
- Glasgow Haskell Compiler (
For Ubuntu Linux,
ghc can be installed via
apt-get as part of Haskell
Platform, and the packages can be installed via
$ sudo apt-get install haskell-platform
Then run cabal update and install:
$ cabal update && cabal install --bindir=.
Godel binary should be created after a successful build.
The model checker we use is mCRL2 (2017 release), and can be downloaded from their official website (recommended).
To build them from source, we need the following dependencies
- clang/LLVM 2.9+ (development packages)
- Obtainable from http://releases.llvm.org/download.html
- GNU Multiprecision library (GMP) version >= 5.0.0
- Needed for Yices and LLVM translation, obtainable from https://gmplib.org/
- Yices SMT solver
- We require specifically version 1 (not Yices2)
First download Yices (version 1), visit
http://yices.csl.sri.com/old/download-yices1.shtml to obtain the package,
extract and make the
yices binary available in
On Ubuntu, the other dependencies can be installed via
$ apt-get install clang llvm-dev \ ocaml-nox camlp4 libocamlgraph-ocaml-dev camlidl \ libapron-ocaml-dev libedit-dev zlib1g-dev \ libgmp-dev
kittelkoat from scratch, and make the binary
/usr/local/bin is in
$ git clone https://github.com/s-falke/kittel-koat; \ cd kittel-koat; make; cd .. ; \ cp kittel-koat/_build/kittel.native /usr/local/bin/ # Move to /usr/local/bin $ mkdir build; \ git clone https://github.com/s-falke/llvm2kittel; \ cd build; cmake ../llvm2kittel && make; cd ..; \ cp build/llvm2kittel /usr/local/bin/ # Move to /usr/local/bin
Godel frontend will call the appropriate installed binaries.