text-only page produced automatically by Usablenet Assistive Skip all navigation and go to page content Skip top navigation and go to directorate navigation Skip top navigation and go to page navigation
National Science Foundation
Awards
design element
Search Awards
Recent Awards
Presidential and Honorary Awards
About Awards
Grant Policy Manual
Grant General Conditions
Cooperative Agreement Conditions
Special Conditions
Federal Demonstration Partnership
Policy Office Website



Award Abstract #1253331

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

NSF Org: CCF
Division of Computing and Communication Foundations
divider line
Initial Amendment Date: January 18, 2013
divider line
Latest Amendment Date: April 17, 2016
divider line
Award Number: 1253331
divider line
Award Instrument: Continuing grant
divider line
Program Manager: Nina Amla
CCF Division of Computing and Communication Foundations
CSE Direct For Computer & Info Scie & Enginr
divider line
Start Date: May 1, 2013
divider line
End Date: April 30, 2018 (Estimated)
divider line
Awarded Amount to Date: $410,453.00
divider line
Investigator(s): Thomas Wahl wahl@ccs.neu.edu (Principal Investigator)
divider line
Sponsor: Northeastern University
360 HUNTINGTON AVE
BOSTON, MA 02115-5005 (617)373-2508
divider line
NSF Program(s): SOFTWARE & HARDWARE FOUNDATION,
SOFTWARE ENG & FORMAL METHODS
divider line
Program Reference Code(s): 1045, 7944, 9251
divider line
Program Element Code(s): 7798, 7944

ABSTRACT

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.


PUBLICATIONS PRODUCED AS A RESULT OF THIS RESEARCH

Note:  When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external site maintained by the publisher. Some full text articles may not yet be available without a charge during the embargo (administrative interval).

Some links on this page may take you to non-federal websites. Their policies may differ from this site.


ALEXANDER KAISER and DANIEL KROENING and THOMAS WAHL. "A Widening Approach to Multi-Threaded Program Verification," ACM Transactions on Programming Languages and Systems (TOPLAS), 2014.

 

Please report errors in award information by writing to: awardsearch@nsf.gov.

 

 

Print this page
Back to Top of page
  FUNDING   AWARDS   DISCOVERIES   NEWS   PUBLICATIONS   STATISTICS   ABOUT NSF   FASTLANE  
Research.gov  |  USA.gov  |  National Science Board  |  Recovery Act  |  Budget and Performance  |  Annual Financial Report
Web Policies and Important Links  |  Privacy  |  FOIA  |  NO FEAR Act  |  Inspector General  |  Webmaster Contact  |  Site Map
National Science Foundation Logo
The National Science Foundation, 4201 Wilson Boulevard, Arlington, Virginia 22230, USA
Tel: (703) 292-5111, FIRS: (800) 877-8339 | TDD: (800) 281-8749
  Text Only Version