| NSF Org: |
CCF Division of Computing and Communication Foundations |
| Recipient: |
|
| Initial Amendment Date: | July 6, 2011 |
| Latest Amendment Date: | July 6, 2011 |
| Award Number: | 1115448 |
| Award Instrument: | Standard Grant |
| Program Manager: |
Jack S. Snoeyink
CCF Division of Computing and Communication Foundations CSE Directorate for Computer and Information Science and Engineering |
| Start Date: | September 1, 2011 |
| End Date: | August 31, 2015 (Estimated) |
| Total Intended Award Amount: | $341,341.00 |
| Total Awarded Amount to Date: | $341,341.00 |
| Funds Obligated to Date: |
|
| History of Investigator: |
|
| Recipient Sponsored Research Office: |
101 COMMONWEALTH AVE AMHERST MA US 01003-9252 (413)545-0698 |
| Sponsor Congressional District: |
|
| Primary Place of Performance: |
101 COMMONWEALTH AVE AMHERST MA US 01003-9252 |
| Primary Place of
Performance Congressional District: |
|
| Unique Entity Identifier (UEI): |
|
| Parent UEI: |
|
| NSF Program(s): | Algorithmic Foundations |
| Primary Program Source: |
|
| Program Reference Code(s): |
|
| Program Element Code(s): |
|
| Award Agency Code: | 4900 |
| Fund Agency Code: | 4900 |
| Assistance Listing Number(s): | 47.070 |
ABSTRACT
Descriptive Complexity measures the richness of a language or sentence needed to describe a given property. There is a profound relationship between the traditional computational complexity of a problem and the descriptive complexity of the problem. In particular, the trade-off between parallel time and amount of hardware, which is a fundamental issue in computation, has been characterized as the trade-off between formula size and number of variables.
Informed by descriptive complexity, PI will use modern SAT solvers, SMT solvers and AI planners to automatically derive efficient algorithms from high-level specifications. PI and his research group will also develop a system that uses solvers to automatically derive low-level reductions between combinatorial problems. Thus methods will be developed to automatically go from high-level specifications to efficient programs as well as to automatically derive lower bounds on how efficient such implementations can be. In using and building these systems, students and established researchers will gain knowledge on what makes problems computationally complex, and how to use state-of-the art solvers to automatically build efficient and reliable software.
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.
PROJECT OUTCOMES REPORT
Disclaimer
This Project Outcomes Report for the General Public is displayed verbatim as submitted by the Principal Investigator (PI) for this award. Any opinions, findings, and conclusions or recommendations expressed in this Report are those of the PI and do not necessarily reflect the views of the National Science Foundation; NSF has not approved or endorsed its content.
This reseach project made contributions leading to eleven published papers in database theory, the static analysis of programs and the automatic synthesis of correct and efficient programs from high-level specifications. Two highlights of our research contributions are the following.
We introduced the concept of "resilience" of a boolean query. The resilience of a query with respect to a database, D, is the minimum number of tuples that must be removed from D to make the query false. Computing resilience is important for understanding why a tuple is present in a query or view, and to compute how to change it in the simplest way. We developed a natural criterion that classifies queries according to the complexity of their resilience problem, showing that this problem exhibits a dichotomy. We defined the "triad" and showed that resilience is NP complete in the presence of a triad; whereas in the absence of a triad resilience is in P. We also extended our result to determine dichotomies in the presence of functional dependencies and to compute the responsibility of such a query, and also for the case of responsibility in the presence of functional dependencies. These four main results give elegant characterizations of complexity dichotomies for each of these four important database problems.
We also introduced and then extended a new method for automatically reasoning about programs. In particular, we reason about reachability between dynamically allocated memory locations. We use a simple logic which includes a relation, n*, denoting the reflexive, transitive closure of the functional pointer field, n.
The key idea is that while reasoning about reachability is undecidable, when we restrict the allowed data structures we can automatically do incremental reasoning about reachability. We showed that each formula, phi, in our language is satisfiable if and only if a corresponding propositional formula, psi, is satisfiable. We can thus use a SAT solver to check psi, giving a proof of correctness if psi is unsatisfiable and a counter-example execution sequence when psi is satisfiable. We call our reasoning system EPR*, effectively propositional reasoning about reachability. The development of effectively propositional reasoning about reachability is probably the most important body of work resulting from this grant. In particular, we and others are continuing to use and extend this work to make it more widely applicable.
Part of the broader impact of the supported research was the training of two young computer scientists. Our research developing new methods to automatic check the correctness of programs may lead in the future to improvements in the security and reliablity of software.
Last Modified: 12/08/2015
Modified by: Neil Immerman
Please report errors in award information by writing to: awardsearch@nsf.gov.
