A Cooperative Parallelization Approach for Property-Directed k-Induction
| Autor: | Matteo Marescotti, Antti E. J. Hyvärinen, Martin Blicha, Natasha Sharygina |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
Model checking
050101 languages & linguistics Lemma (mathematics) Class (computer programming) Computer science 05 social sciences Craig interpolation 02 engineering and technology Parallel computing Solver Margin (machine learning) Reachability Bounded function 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing 0501 psychology and cognitive sciences |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783030393212 VMCAI |
| Popis: | Recently presented, IC3-inspired symbolic model checking algorithms strengthen the procedure for showing inductiveness of lemmas expressing reachability of states. These approaches show an impressive performance gain in comparison to previous state-of-the-art, but also present new challenges to portfolio-based, lemma sharing parallelization as the solvers now store lemmas that serve different purposes. In this work we formalize this recent algorithm class for lemma sharing parallel portfolios using two central engines, one for checking inductiveness and the other for checking bounded reachability, and show when the respective engines can share their information. In our implementation based on the PD-KIND algorithm, the approach provides a consistent speed-up already in a multi-core environment, and surpasses in performance the winners of a recent solver competition by a comfortable margin. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|