Presenter
Milán Mondok
BME, Budapest
Authors
Milán Mondok, Vince Molnár
Abstract
Saturation is a symbolic reachability algorithm for asynchronous systems. It works well because transitions in such systems are mostly local: each event reads and writes only a few variables, and saturation iterates along that structure instead of applying the whole transition relation at every step. Until now, this has been limited to models with explicit or limited next-state relations, mainly Petri nets. Software models, where transitions are given as logical formulas, are usually checked with SMT-based methods (BMC, CEGAR, ...) that do not use locality.
This talk is about bringing saturation to a much wider set of domains: any transition system that can be described using SMT formulas. Substitution diagrams (presented in an earlier AVM talk) let saturation take SMT predicates as its next-state relation. Substitution diagrams lazily enumerate a decision-diagram-like structure using SMT queries during exploration. One problem comes up that does not exist for Petri nets: successor values at one level can depend on variables at lower levels, and the recursion may not terminate. We handle this with look-ahead, which uses the state set explored so far to bound the iteration.
The approach is implemented in Theta. We evaluated it on Petri nets, DVE models, and concurrent C programs. For concurrent C, we are competitive with partial-order CEGAR. On Petri nets and DVE, a constant-factor overhead separates us from dedicated saturation engines.
Slides
TBA