Module proof

Module proof 

Source
Expand description

Algorithms for proving the safety of a finite state transition system.

Re-exports§

pub use ic3_stateful_solver::IC3Stateful;
pub use ic3_stateless_solver::IC3Stateless;
pub use pdr::PDR;
pub use proof_result::ProofResult;

Modules§

ic3_stateful_solver
This algorithm is an almost exact implementation of what is described in “SAT-Based Model Checking without Unrolling”.
ic3_stateless_solver
This algorithm is an exact implementation of what is described in “SAT-Based Model Checking without Unrolling”.
pdr
proof_result

Traits§

FiniteStateTransitionSystemProver