Jasmin Verifier

Description:

Tool to verify safety and security properties of the Jasmin pre-assembly language.

Requirements:

• Haskell Platform (with GHC version >= 8.x)
• Dafny (only for verification)
• Boogie (only for verification)
• Z3 (only for verification)

Installation:

cabal sandbox init
cabal sandbox add-source packages/boogaman/*
cabal install boogaman
cabal install

Usage:

For usage instructions, see

cabal exec -- jasminv --help

Examples:

By default, the tool will typecheck and verify an input Jasmin program:

> jasminv examples/test.mil --verify=bothv

Tests:

For running tests, you can simply run:

cabal test

For nice test output, you can run instead:

cabal exec -- runhaskell tests/Tests.hs