[Haskell-cafe] ANN improve-0.0.4

[Tom Hawkins]

Hi,

ImProve [1] is a little imperative DSL that compiles to C code.
Intended for high assurance embedded applications, ImProve is also an
infinite state, unbounded model checker.  Meaning ImProve can verify
assertions in a program will always be true.  Here's an example:

  module Main where
  import Language.ImProve

  launchControl :: Stmt ()
  launchControl = do
    presidentialAuthority <- input bool "presidentialAuthority"
    buttonPressed         <- input bool "buttonPressed"
    launchMissiles        <- bool' "launchMissiles" $
(presidentialAuthority ||. buttonPressed)
    assert "conditionsToLaunch" $ launchMissiles ==.
(presidentialAuthority &&. buttonPressed)

  main :: IO ()
  main = verify "yices" 20 launchControl


Running this program yields:

  verifying conditionsToLaunch    FAILED: disproved basis in k = 1 (see trace)


On verification failures, ImProve will emit a counter example showing
the violation, which is essentially a program trace showing how things
could go wrong.  In this case, the trace looks like this:

  initialize launchMissiles := false
  cycle 0
  input presidentialAuthority <== true
  input buttonPressed <== false
  launchMissiles <== true
  assertion FAILED: conditionsToLaunch

This basically means Barack was somehow able to launch on his own.
(Man!  I even voted for the guy!)

Under the hood, ImProve uses Yices [2] for SMT solving, and a method
of unbounded model checking known as k-induction.

Don't expect too much from ImProve; it's a very restrictive language.
It's basically three data types (bool, int, float), variables
assignments, and 'if' statements.  No procedures, no loops, no arrays,
no pointers, etc.  However, it can still do interesting things --
especially with Haskell combinators in play.

Hope you find it useful.  And as always, questions, comments, and
feedback welcome.

-Tom

[1] http://hackage.haskell.org/package/improve
[2] http://yices.csl.sri.com/