Software and Computational Systems Lab at LMU Munich

This project developed a machine-learning framework to predict the most effective software verifier for a given C program – trained on the Software...

CPA-Daemon is a microservice (currently gRPC service) for continuous verification of C programs with CPAchecker. Clients could craft gRPC requests...

PJBDD is a Java-based, multi-threaded Binary Decision Diagram (BDD) library that facilitates concurrent computation and parallel operations. It is...

We developed the first algorithm selector, Btor2-Select, for the word-level hardware model-checking problem described in the Btor2 language. Given a...

For benchmarking purposes, BenchExec typically creates a container with a file-system overlay atop the system's file system. However, due to a kernel...