Model Checking of Navigation Logics (MoNaLog)

• Applicant: Professor Dr. Markus Müller-Olm
• Subject Area: Theoretical Computer Science ; Security and Dependability, Operating-, Communication- and Distributed Systems
• Term: from 2020 to 2024
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 436811065

Software is a crucial component of systems whose failure can cause severe consequences like massive financial damages or even threats to life or limb. Software reliability is therefore a core problem of computer science. Classical validation techniques like testing or simulation are fundamentally unable to provide strong correctness guarantees since they only consider a selection of possible program executions. This problem is exacerbated by the presence of concurrency (parallelism) in modern systems which commonly implies non-deterministic behavior. Therefore, formal methods of program verification were invented which rely on techniques from mathematics and mathematical logic and are in principle able to provide strong correctness guarantees. However, classical program verification, e.g. à la Hoare-Floyd, is only partially automatable. This makes their integration into traditional software development difficult. Therefore, since the 1980s, fully automatic verification methods have been developed, in particular so called model checking, in which it is algorithmically decided whether a program abstraction satisfies a formal specification given by a formula of temporal logic.The purpose of the proposed project is the development and analysis of novel temporal logics which allow, in addition to the consideration of temporal, merely sequential succession of actions, for the consideration of characteristic aspects of the system behavior's description when formulating properties. In this context, the focus is on the navigation over complex control structures, in particular those that describe recursion and multithreading. Our aim is to define logics which enrich existing logics by corresponding concepts and for which the model checking problem remains effective. For the new logics and the corresponding classes of system models, we want to study the complexity of the model checking problem and develop model checking algorithms. These algorithms should be implemented prototypically and evaluated on characteristic benchmarks. Furthermore, we also want to study related aspects like the decidability of the satisfiability problem.

• DFG Programme: Research Grants