Dynamic Reductions for Model Checking Concurrent Software.
Symbolic model checking of parallel programs stands and falls with effective methods of dealing with the explosion of interleavings. We propose a dynamic reduction technique to avoid unnecessary interleavings. By extending Lipton’s original work with a notion of bisimilarity, we accommodate dynamic transactions, and thereby reduce dependence on the accuracy of static analysis, which is a severe bottleneck in other reduction techniques.
The combination of symbolic model checking and dynamic reduction techniques has proven to be challenging in the past. Our generic reduction theorem nonetheless enables us to derive an efficient symbolic encoding, which we implemented for IC3 and BMC. The experiments demonstrate the power of dynamic reduction on several case studies and a large set of SVCOMP benchmarks.
slides (larman00_main.pdf) | 1.0MiB |
Mon 16 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 15:30: Model-checking and bug findingVMCAI at Amphitheater 44 Chair(s): Andreas PodelskiUniversity of Freiburg, Germany | |||
14:00 - 14:30 Talk | Effective Bug Finding in C Programs with Shape and Effect Abstraction VMCAI Iago AbalIT University of Copenhagen, Claus BrabrandIT University of Copenhagen, Denmark, Andrzej WąsowskiIT University of Copenhagen, Denmark | ||
14:30 - 15:00 Talk | Reduction of Workflow Nets for Generalised Soundness Verification VMCAI Hadrien BrideFemto-ST / Université de Franche-Comté, Olga KouchnarenkoFemto-ST / Université de Franche-Comté, Fabien PeureuxFemto-ST / Université de Franche-Comté + Smartesting S&S Media Attached | ||
15:00 - 15:30 Talk | Dynamic Reductions for Model Checking Concurrent Software. VMCAI Henning GüntherTechnische Universität Wien, Alfons LaarmanVienna University of Technology, Ana SokolovaUniversity of Salzburg, Georg WeissenbacherTechnische Universität Wien File Attached |