Previous  Up  Next

Module Bwd.BFSH (.ml)

module BFSH: Strategy 
val search : ?invariants:Node.t list ->
       ?candidates:Node.t list -> Ast.t_system -> Bwd.result

Backward reachability search on a system. The user can also provide invariants that are true of the system to help the search. Candidate invariants can also be provided, they will be proven as real invariants if necessary.