Software and Computational Systems Lab at LMU Munich
Software and Computational Systems Lab at LMU Munich is participating in GSoC 2024. View the ideas list and the contribution guide for this organization.
Implementing backward bounded model checking in CPAchecker
Bas Laarakker
Backward bounded model checking is a technique for program analysis that aims to solve the error location reachability problem by searching for...
Scaling Formal Verification: Parallel Analysis of Functions
George Granberry
Formal methods have been known to be useful for verifying critical software. However, one of the main factors keeping tools such as CPA-Checker from...
Reverse Program Synthesis for Backward Reachability Analysis in CPAchecker
Jia Sun
CPAchecker now supports reachability analysis, which can search for a path from the initial program location to the error location. This project is a...
Integrating the SMT solver dReal to the framework JavaSMT
Julius Brehme
SMT solvers are widely utilized in computer-guided verification of computer programs and artificial intelligence. With a multitude of theories...