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

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

• look into Petri nets
• first draft of input requirements
• first draft of pseudocode for DPOR algorithm (next(p) / same process still as blackbox; consider: "membrane" property, preference order)

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