Sleep Set POR in Trace Abstraction Refinement

Project Goal

Integrate Trace Abstraction Refinement (TAR) with a form of Partial Order Reduction (POR), namely Sleep Sets. Thereby we aim to improve the verification time for concurrent programs. We formulate the integration, prove soundness and completeness, and implement it in Ultimate Automizer's automata-based analysis of concurrent programs.

Resources

• Paper by Cassez & Ziegler: https://link.springer.com/chapter/10.1007/978-3-662-48899-7_17
• POR book by Godefroid: https://www.semanticscholar.org/paper/Partial-order-Methods-for-the-Veriication-of-an-to-Godefroid-Devillers/acaf9c18e5711d4fd63144953292d43fb3fdac92?p2df

Work Packages

• Related Work & Background
• Implementation & Evaluation of Godefroid's sleep set algorithm (with delay sets)
• Definition, Proof, Implementation & Evaluation of a modified sleep set construction (no delay sets)
• Basic integration of POR and TAR: devise, prove, implement
• Implement lazy construction of program automaton
• Store interpolants & use for improved reduction (conditional POR)
• Optimized integration: devise, implement, prove
• Finalize thesis

Current Tasks

• thesis presentation
• code cleanup & documentation; merge into dev
• overall evaluation of different concurrency approaches

Ultimate

Sleep Set Reduction

Project Library-Automata, package de.uni_freiburg.informatik.ultimate.automata.partialorder

• IIndependenceRelation (given as parameter)
• INwaOutgoingLetterAndTransitionProvider<LETTER, STATE> represents an automaton
• NestedWordAutomataUtils.isFiniteAutomaton to test if automaton does not contain call or return edges
• consider form of implementation: lazy automata construction, eager automata construction, emptiness check?

Usage

• settings: ultimate/trunk/examples/settings/automizer/concurrent/svcomp-Reach-32bit-Automizer_Default-noMmResRef-FA-NoLbe-Delay.epf
• toolchain AutomizerCInline or AutomizerBplInline
• examples in trunk/examples/concurrent; or SV-COMP (see here)