Dynamic POR for Verification of Concurrent Programs with Loops

Project Goal

...

Resources

• Sound sequentialization for concurrent program verification (https://dl.acm.org/doi/10.1145/3519939.3523727)
• Dynamic partial-order reduction for model checking software (https://dl.acm.org/doi/10.1145/1047659.1040315)
• Verification of Concurrent Programs Using Petri Net Unfoldings (https://link.springer.com/chapter/10.1007/978-3-030-67067-2_9)
• ...

Meetings

2023-02-09

• Eclipse, again
• contract for SetBacktrackingPoints; try the proof
• for now: backtrack all conflicts, not only the latest (simplifies the proofs, may be necessary because we don't have processes)
• variations on definition of L-persistent: prefixes of accepted words, perhaps minimal i
• alternative definition of L-persistent: restrict M to letters in L

2023-02-06

• necessary spec for disabling relation
• break down correctness proofs into smaller lemmas, using weakly L-persistent sets
• project-specific Java version setting cause of Ultimate compilation failure?

2023-01-24

• actions f_a(q) that need to be executed to enable another action a (replacement for next(p)) -- formal definition (similar to membranes)
• membranes instead of a_1...a_n \in L(A) -> a_1...a_n t \in L(A)

2023-01-19

2023-01-13

• definition of "thread-equivalence" -- is it an equivalence, is it well-defined?
• problems with disabling actions "of other processes"
• one example where the algorithm seems to miss an equivalence class
• possible procedure contracts

2022-12-29

• discussion of input requirements; formal definition of requirements on "threads" assignment (seems like simply an equivalence relation)
• pseudocode, in particular processes and preference order
• Ultimate setup

2022-12-19

• why do equivalent words not always lead to the same states
• ICFGs: interprocedural control flow graphs, i.e., control flow graphs with special edges for fork and join
• replacement for "process" notion in DPOR: definition based solely on language (which can be checked on Petri net), or definition directly on Petri net structure
• Petri nets & Petri programs
• Ultimate setup

Current Tasks

• continue proof of SetBacktrackPoints
• Dominik: sanity check for variations of L-persistent definition
• try to come up with monotonic definition of persistent (any superset of a "persistent" set is also "persistent")
• Eclipse setup

Work Packages

• Theoretic Foundation of DPOR
  • Input requirements
  • Happens-before relation
  • Translation of DPOR algorithm
  • Correctness theorem
• Implementation
  • Architecture Planning
  • Clock Vectors
  • DPOR algorithm
• Unit Tests & Debugging
• Integration Tests & Debugging
• Evaluation
• Thesis