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-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

• check failing example against proof of DPOR paper

• correctness: think of procedure contracts & invariants

• Dominik: read pseudocode with "seen" set

• improve input requirements (define formally), pseudocode

• look into Petri nets

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