Software and Computational Systems Lab at LMU Munich
Software Analysis, Software Verification, and Benchmarking
The following list contains our projects with the ideas that are (in our opinion) suitable for Google Summer of Code. Feel free to suggest your own ideas. A more detailed list of ideas (with descriptions) can be found at https://www.sosy-lab.org/gsoc/gsoc2019.php#ideas .
CPAchecker ( website )
CPAchecker is an award-winning open-source framework for the verification of software. It is written in Java and based on a highly modular architecture that allows to develop and combine a wide range of different analyses. CPAchecker is used for verification of the Linux kernel and has helped to find more than 50 bugs in the kernel.
- Eclipse plugin
- Angular and automated tests for verification report
- Integrating SymPy into CPAchecker for Invariant Generation
- DART-like Test-case Generation in CPAchecker
- Checking Equivalence of Program Semantics Automatically
JavaSMT ( website )
JavaSMT is a common API layer for accessing various SMT solvers. It was created out of our experience integrating and using different SMT solvers in the CPAchecker project. JavaSMT can express formulas in the theory of integers, rationals, bitvectors, floating-points, and uninterpreted-functions, and supports model generation, interpolation, formula inspection and transformation.
- Integrate more SMT solvers
- SMT in the Cloud
BenchExec ( website )
BenchExec is a benchmarking framework for Linux (written in Python) that is aimed at a high reliability of the results. It can measure the CPU-time and peak memory usage of whole groups of processes. To do so, it makes use of modern Linux features such as cgroups and namespaces, effectively creating a benchmarking container whose resource usage is measured.
- Make use of the Intel Cache Allocation Technology
- Modern architecture and tests for HTML tables
Software and Computational Systems Lab at LMU Munich 2019 Projects
Design and Create CLion plugin for CPAchecker executionCPAChecker 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 BenchExecIn this project we aim to incorporate Intel cache allocation software package (intel-cmt-cat) in BenchExec for cache allocation on a per core basis...