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

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Data.SBV.Tools.BMC

Description

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

Synopsis

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

# Documentation

bmc Source #

Arguments

:: (EqSymbolic st, Queriable IO st, res ~ QueryResult st) |
=> 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 ~ QueryResult st) => SMTConfig -> Maybe Int -> Bool -> Symbolic () -> (st -> SBool) -> (st -> [st]) -> (st -> SBool) -> IO (Either String (Int, [res])) Source #

Bounded model checking, configurable with the solver