CAREER: Verifying Threaded Software Using Resource Bounds -- An Approach Towards Dependable Concurrency

点击翻译按钮获取中文摘要

Software development is facing a paradigm shift towards ubiquitousconcurrent programming, giving rise to software that is among the mostcomplex technical artifacts ever created by humans. Concurrent programmingpresents 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, byproducing verification technology that assists non-specialist programmersin detecting concurrency errors, or demonstrating their absence. Theproposed technology will confront the concurrency explosion problem thatverification methods often suffer from. The project's goal is a frameworkunder which the analysis of programs with unbounded concurrency resources(such as threads of execution) can be soundly reduced to an analysis undera small constant resource bound, making the use of state space explorerspractical. As a result, the project will largely eliminate the impact ofunspecified computational resources as the major cause of complexity inanalyzing 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.