Florian Schrögendorfer,
"Bounded Model Checking of Lockless Programs"
, in Institut für Formale Modelle und Verifikation, Johannes Kepler Universität Linz, 2021
Original Titel:
Bounded Model Checking of Lockless Programs
Sprache des Titels:
Englisch
Original Kurzfassung:
In this thesis we explore the potential of bounded model checking for verifying concurrent programs including the target architecture's memory ordering habits. Due to the complexity of actual processors, we devise a highly simplified virtual machine model and show that the addition of store buffers is sufficient to imitate the behaviour of current x86 implementations. After designing a formal framework for the execution of arbitrary programs on this virtual machine, encodings of the corresponding model checking problems in two different SMT formats are developed. We then present ConcuBinE, a tool for automating the encoding and evaluation of generated SMT formulas using state-of-the-art solvers and show the feasibility of our approach through a variety of experiments.
Forschungs-