In the talk we will consider an approach to symbolic
model checking of labeled transition systems. Instead of unrolling the
transition relation, it incrementally generates lemmas that are
inductive relative to stepwise approximate reachability information. In
this way, the algorithm gradually refines the property, eventually
producing either an inductive strengthening of the property or a
counterexample trace.

21.10.2019, 17:15.

State University, Stary Peterhof, Universitetski pr., 28