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
  • read & understand section 6 of Azadeh's paper
• begin writing corresponding chapters (definitions)
  • POR background
• implementation:
  • see which code can be shared between the classes and factor out
  • run some tests to find common problems; then organize running of benchmarks
  • new-state variant of reduction: implement search-and-construct variant

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)