Software development is facing a paradigm shift towards ubiquitous concurrent programming, giving rise to software that is among the most complex technical artifacts ever created by humans. Concurrent programming presents several risks and dangers for programmers who are overwhelmed by puzzling and irreproducible concurrent program behavior, and by new types of bugs that elude traditional quality assurance techniques. If this situation is not addressed, we are drifting into an era of widespread unreliable software, with consequences ranging from collapsed programmer productivity, to catastrophic failures in mission-critical systems.
This project will take steps against a concurrent software crisis, by producing verification technology that assists non-specialist programmers in detecting concurrency errors, or demonstrating their absence. The proposed technology will confront the concurrency explosion problem that verification methods often suffer from. The project's goal is a framework under which the analysis of programs with unbounded concurrency resources (such as threads of execution) can be soundly reduced to an analysis under a small constant resource bound, making the use of state space explorers practical. As a result, the project will largely eliminate the impact of unspecified computational resources as the major cause of complexity in analyzing concurrent programs. By developing tools for detecting otherwise undetectable misbehavior and vulnerabilities in concurrent programs, the project will contribute its part to averting a looming software quality crisis.
