Previous  Up  

Module Bwd.Selected (.ml)

module Selected: Strategy

Strategy selected by the options of the command line

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.