Info

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/gsoc2018.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.

Ideas

• 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.

Ideas

• 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.

Ideas

• Make use of the Intel Cache Allocation Technology
• Modern architecture and tests for HTML tables