Dual Approximated Reachability Model Checking in CPAchecker
Hardware verification algorithms were previously modified to suit software verification and implemented in CPAchecker. These algorithms iteratively compute interpolants to overapproximate reachable state space and eventually converge to invariant. They use interpolation in a so-called forward fashion to overapproximate reachable states from initial states. Dual Approximated Reachability algorithm also uses interpolants to overapproximate states that can reach assertion-violating states. It combines information from both forward and backward interpolation sequences to converge faster. In the talk, we briefly explain the main idea of the algorithm, show practical obstacles in the CPAchecker implementation that we overcame and present the final results of the algorithm’s performance.
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 |