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

• read background and related work, get a better understanding of underlying theory
• begin writing corresponding chapters (definitions)
• familiarize with Ultimate, prepare implementation

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?