Verifier Selection using LLMs
Contributor: Patrik Felbinger
This project developed a machine-learning framework to predict the most effective software verifier for a given C program – trained on the Software...
Programming languages
Software and Computational Systems Lab at LMU Munich
Algorithms and Tooling for Software Verification
Technologies
grpcJavaJavaScriptPythonQuarkus
Topics
benchmarkingcloudformal methodsprogram analysisSAT & SMT solvingsoftware verification
- Total projects
- 12
- Years participating
- 5
- Most recent
- 2025
Participation history
Historical projects
CPA-Daemon: Behavior Driven Tests
Contributor: Wenyi Shi
CPA-Daemon is a microservice (currently gRPC service) for continuous verification of C programs with CPAchecker. Clients could craft gRPC requests...
Extending PJBDD with CESRBDDs: BDDs with Complemented Edges and Edge-Specified Reductions
Contributor: Ahmed Tarek
PJBDD is a Java-based, multi-threaded Binary Decision Diagram (BDD) library that facilitates concurrent computation and parallel operations. It is...
Adaptive Algorithm Selection for Btor2 Verification Tasks
Contributor: Zhengyang Lu
We developed the first algorithm selector, Btor2-Select, for the word-level hardware model-checking problem described in the Btor2 language. Given a...
Overlay Handling with fuse-overlayfs
Contributor: Haoran Yang
For benchmarking purposes, BenchExec typically creates a container with a file-system overlay atop the system's file system. However, due to a kernel...
Implementing backward bounded model checking in CPAchecker
Contributor: 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
Contributor: 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
Contributor: 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
Contributor: Julius Brehme
SMT solvers are widely utilized in computer-guided verification of computer programs and artificial intelligence. With a multitude of theories...
Design and Create CLion plugin for CPAchecker execution
Contributor: Tharsanan Kurukulasingam
CPAChecker is a framework which can be used as a software verification tool for C programs. We can use CPAchecker locally by command line interface...
Implement Cache Allocation Technology in BenchExec
Contributor: Aditya Arora
In this project we aim to incorporate Intel cache allocation software package (intel-cmt-cat) in BenchExec for cache allocation on a per core basis...
Upgrade of AngularJS, Refactoring UI and automated testing for CPAchecker.
Contributor: Lokesh Kishor Nandanwar
CPAchecker Project - Upgrade of AngularJS and other third-party libraries used. Refactoring of User Interface Writing automated tests for unit...