Large Block Encoding for Concurrent Programs

Large Block Encoding for Concurrent Programs

Tasks

11. Use the developer GUI to analyze a program.

Examples in trunk/examples/concurrent/ Toolchain trunk/examples/toolchains/PetriAutomizerBplInline.xml or trunk/examples/toolchains/PetriAutomizerCInline.xml

12. Write example programs

Write two new concurrent program (one safe/one unsafe) that are related to your thesis.

13. Get familiar with AutomataScript and Petri nets

https://ultimate.informatik.uni-freiburg.de/?ui=int&tool=automata_library&task=automataScript&sample=151597609 Write two Peti nets that are related to your thesis. Demonstate somehow that large block encoding is speeding up automata operations

14. Get the pthread benchmarks from the SV-COMP https://sv-comp.sosy-lab.org/2019/

and verify one of these.

Literature

Petri nets

Petri nets on Wikipedia

Petri net unfoldings

1996TACAS - Esparza,Römer,Vogler - An Improvement of McMillan's Unfolding Algorithm

Textbook Unfoldings-Esparza-Heljanko

Semiar slides of Claus Schätzle

Program Verification (in general) via Trace Abstraction

Software Model Checking for People Who Love Automata

Poster zu Ultimate Automizer

Program Verification for Concurrent Programs via Trace Abstraction

Bachelorarbeit of Julian Jarecki