Documentation ¶
Overview ¶
Package iic provides an incremental inductive reachability checker.
Background references:
[1] Efficient Implementation of Property Directed Reachability Niklas Een, Alan Mishchenko, Robert Brayton. 2011 FMCAD
[2] IC3 and beyond: Incremental, Inductive Verification Aaron R. Bradley. 2012 in CAV
[3] Checking Safety by Inductive Generalization of Counterexamples to Induction. Aaron R. Bradley and Zohar Manna
Index ¶
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
This section is empty.
Types ¶
type Options ¶
type Options struct { Verbose bool Preprocess bool MaxDepth int Duration time.Duration GenTrace bool VerifyInvariant bool FilterObs bool ConsecuSift bool ConsecuSiftPull bool Justify bool DeepObs bool GnrlRemoveLits bool }
Options for the IIC checker
func NewOptions ¶
func NewOptions() *Options
NewOptions gives a new Options object with default values. The zero value is not default.
type T ¶
type T struct {
// contains filtered or unexported fields
}
T contains state for an ic3/pdr model checker.
func New ¶
New creates a new incremental inductive model checker from a transition system and bad state literal.
func (*T) FillOutput ¶
FillOutput fills `o` with information about the last call to Try.
Source Files ¶
Directories ¶
Path | Synopsis |
---|---|
internal
|
|
cnf
Package cnf provides a levelled cnf for iic.
|
Package cnf provides a levelled cnf for iic. |
lits
Package lits supports storage of and miscellaneous operations on literals for iic.
|
Package lits supports storage of and miscellaneous operations on literals for iic. |
obs
Package obs provides support for proof obligations.
|
Package obs provides support for proof obligations. |
queue
Packaage queue contains a basic queue of ints.
|
Packaage queue contains a basic queue of ints. |