Scaling Formal Verification: Parallel Analysis of Functions
We give an overview of the development of software model checking, a general approach to algorithmic program verification that integrates static analysis, model checking, and deduction. We start with a look backwards and briefly cover some of the important steps in the past decades. The general approach has become a research topic on its own, with a wide range of tools that are based on the approach. Therefore, we discuss the maturity of the research area of software model checking in terms of looking at competitions, at citations, and most importantly, at the tools that were build in this area: we count 76 verification systems for software written in C or Java. We conclude that software model checking has quickly grown to a significant field of research with a high impact on current research directions and tools in software verification. This talk is based on the following joint work with Andreas Podelski: https://doi.org/10.1007/978-3-031-22337-2_27
Mon 11 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:30 - 15:00 | |||
14:30 5mTalk | Enhancing CPAchecker: A Framework for Distributed Analyses [Workshop] CPAchecker Matthias Kettl LMU Munich | ||
14:35 5mTalk | Scaling Formal Verification: Parallel Analysis of Functions [Workshop] CPAchecker George Granberry Chalmers University of Technology | ||
14:40 5mTalk | Dual Approximated Reachability Model Checking in CPAchecker [Workshop] CPAchecker Marek Jankola LMU Munich | ||
14:45 5mTalk | Current State of Memory-Safety Analysis in CPAchecker [Workshop] CPAchecker Daniel Baier Ludwig Maximilian University of Munich | ||
14:50 5mTalk | CPAdaemon: Progress and Demo [Workshop] CPAchecker Henrik Wachowitz LMU Munich |