iic

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

• type Options
  • func NewOptions() *Options
• type T
  • func New(trans *logic.S, bad z.Lit) *T
  • func (t *T) FillOutput(o *reach.Output)
  • func (t *T) Options() *Options
  • func (t *T) Try() int

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

func New(trans *logic.S, bad z.Lit) *T

New creates a new incremental inductive model checker from a transition system and bad state literal.

func (*T) FillOutput

func (t *T) FillOutput(o *reach.Output)

FillOutput fills `o` with information about the last call to Try.

func (*T) Options

func (t *T) Options() *Options

func (*T) Try

func (t *T) Try() int

Try tries to solve the reachability problem specified in New.

Try returns

1 if there is a trace to the bad state
0 if timed out
-1 if there cannot be a trace to the bad state