Synthesizing realistic verification tasks
| dc.contributor.advisor | Steffen, Bernhard | |
| dc.contributor.author | Jasper, Marc | |
| dc.contributor.referee | Siegel, Stephen F. | |
| dc.date.accepted | 2021-07-15 | |
| dc.date.accessioned | 2021-08-18T06:24:46Z | |
| dc.date.available | 2021-08-18T06:24:46Z | |
| dc.date.issued | 2021 | |
| dc.description.abstract | This thesis by publications focuses on realistic benchmarks for software verification approaches. Such benchmarks are crucial to an evaluation of verification tools which helps to assess their capabilities and inform potential users. This work provides an overview of the current landscape of verification tool evaluation and compares manual and automatic approaches to benchmark generation. The main contribution of this thesis is a new framework to synthesize realistic verification tasks. This framework allows to generate verification tasks that target sequential or parallel programs. Starting from a realistic formal specification, a Büchi automaton is synthesized while ensuring realistic hardness characteristics such as the number of computation steps after which errors occur. The resulting automaton is then transformed to a Mealy machine to produce a sequential program in C or Java or to a parallel composition of modal transition systems. A refinement of the latter is encoded in Promela or as a Petri net. A task that targets such a parallel system requires checking whether or not a given interruptible temporal property is satisfied or whether parallel systems are weakly bisimilar. Temporal properties may include branching-time and linear-time formulas. For the latter, it can be ensured that every parallel component matters during verification. This thesis contains additional contributions that build on top of attached publications. These are (i) a generalization of interruptibility that covers branching-time properties, (ii) an improved generation of parallel contexts, and (iii) a definition of alphabet extension on a semantic level. Alphabet extensions are a key part for ensuring hardness of generated tasks that target parallel systems. Benchmarks that were synthesized using the presented framework have been employed in the international Rigorous Examination of Reactive Systems (RERS) Challenge during the last five years. Several international teams attempted to solve the corresponding verification tasks and used ten different tools to verify the newly added parallel programs. Apart from the evaluation of these tools, this endeavor motivated participants of RERS to conceive new formal techniques to verify parallel systems. The result of this thesis thus helps to improve the state of the art of software verification. | en |
| dc.identifier.uri | http://hdl.handle.net/2003/40473 | |
| dc.identifier.uri | http://dx.doi.org/10.17877/DE290R-22348 | |
| dc.language.iso | en | de |
| dc.subject | Benchmark generation | en |
| dc.subject | Program verification | en |
| dc.subject | Model checking | en |
| dc.subject | Bisimulation checking | en |
| dc.subject | Temporal logics | en |
| dc.subject | LTL | en |
| dc.subject | HML | en |
| dc.subject | CTL | en |
| dc.subject | Hard benchmarks | en |
| dc.subject | Error witnesses | en |
| dc.subject | Synthesis | en |
| dc.subject | Parallel decomposition | en |
| dc.subject | Property preservation | en |
| dc.subject | Modal transition systems | en |
| dc.subject | Modal contracts | en |
| dc.subject | Alphabet extension | en |
| dc.subject.ddc | 004 | |
| dc.subject.rswk | Benchmark | de |
| dc.subject.rswk | Programmverifikation | de |
| dc.subject.rswk | Model Checking | de |
| dc.subject.rswk | Bisimulation | de |
| dc.subject.rswk | Temporale Logik | de |
| dc.subject.rswk | Synthese | de |
| dc.title | Synthesizing realistic verification tasks | en |
| dc.type | Text | de |
| dc.type.publicationtype | doctoralThesis | de |
| dcterms.accessRights | open access | |
| eldorado.secondarypublication | false | de |