JetBrains Research unites scientists working in challenging new disciplines

Seminar: Property-Directed Reachability

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.

Venue: room 3248, Faculty of Mathematics and Mechanics, Saint Petersburg

State University, Stary Peterhof, Universitetski pr., 28