sbv-8.1: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright(c) Levent Erkok
Safe HaskellNone



Bounded model checking interface. See Documentation.SBV.Examples.ProofTools.BMC for an example use case.



bmc Source #


:: (EqSymbolic st, Queriable IO st res) 
=> Maybe Int

Optional bound

-> Bool

Verbose: prints iteration count

-> Symbolic ()

Setup code, if necessary. (Typically used for setOption calls. Pass return () if not needed.)

-> (st -> SBool)

Initial condition

-> (st -> [st])

Transition relation

-> (st -> SBool)

Goal to cover, i.e., we find a set of transitions that satisfy this predicate.

-> IO (Either String (Int, [res]))

Either a result, or a satisfying path of given length and intermediate observations.

Bounded model checking, using the default solver. See Documentation.SBV.Examples.ProofTools.BMC for an example use case.

Note that the BMC engine does *not* guarantee that the solution is unique. However, if it does find a solution at depth i, it is guaranteed that there are no shorter solutions.

bmcWith :: (EqSymbolic st, Queriable IO st res) => SMTConfig -> Maybe Int -> Bool -> Symbolic () -> (st -> SBool) -> (st -> [st]) -> (st -> SBool) -> IO (Either String (Int, [res])) Source #

Bounded model checking, configurable with the solver