Tool to verify safety and security properties of the Jasmin pre-assembly language.
- Haskell Platform (with GHC version >= 8.x)
- Dafny (only for verification)
- Boogie (only for verification)
- Z3 (only for verification)
cabal sandbox init
cabal sandbox add-source packages/boogaman/*
cabal install boogaman
cabal install
For usage instructions, see
cabal exec -- jasminv --help
By default, the tool will typecheck and verify an input Jasmin program:
> jasminv examples/test.mil --verify=bothv
For running tests, you can simply run:
cabal test
For nice test output, you can run instead:
cabal exec -- runhaskell tests/Tests.hs