Project: Cloud-Based Software Verification

Team: Prof. Dr. Dirk Beyer, Peter Häring

Research institution: Universität Passau

Abstract: Formal software verification proves if a given program satisfies a given specification. Even though this is an undecidable problem in theory, improvements in the last decade have brought verification of software systems to the matureness where it becomes interesting for industrial applications. Still, current state-of-the-art approaches still require a considerable amount of time and memory resources for a single verification problem. This project focusses on large-scale verification with our verification tool CPAchecker.

One example for industrial-scale software verification is proving safety specifications of the Linux Kernel. The Linux Kernel itself is huge, and poses (among others) two verification challenges: (1) it is a software product line, which means that it describes millions of slightly different configurations (specified by over 8000 configuration options) and (2) the high development pace results in many versions (commits). Similar to software regression testing, timely feedback after each commit is desirable. Given the high demand of resources for verification runs, we investigate distributed verification in cloud environments.

This Figure shows a cloud consisting of possibly heterogeneous computing resources with the capability to solve verification problems. We combine the computing power of many resources for software verification, and investigate the possibilities of software verification in large projects.

Last modified 8 years ago Last modified on Dec 2, 2013 11:48:42 AM

Attachments (1)

Download all attachments as: .zip