Award Abstract # 1526270
SHF: Small: New Frontiers in Constraint-Based Program Analysis

NSF Org: CCF
Division of Computing and Communication Foundations
Recipient: GEORGIA TECH RESEARCH CORP
Initial Amendment Date: June 24, 2015
Latest Amendment Date: June 24, 2015
Award Number: 1526270
Award Instrument: Standard Grant
Program Manager: Anindya Banerjee
abanerje@nsf.gov
 (703)292-7885
CCF
 Division of Computing and Communication Foundations
CSE
 Directorate for Computer and Information Science and Engineering
Start Date: September 1, 2015
End Date: April 30, 2017 (Estimated)
Total Intended Award Amount: $450,000.00
Total Awarded Amount to Date: $450,000.00
Funds Obligated to Date: FY 2015 = $24,460.00
History of Investigator:
  • Mayur Naik (Principal Investigator)
    mhnaik@cis.upenn.edu
Recipient Sponsored Research Office: Georgia Tech Research Corporation
926 DALNEY ST NW
ATLANTA
GA  US  30318-6395
(404)894-4819
Sponsor Congressional District: 05
Primary Place of Performance: Georgia Institute of Technology
225 North Ave NW
Atlanta
GA  US  30332-0001
Primary Place of Performance
Congressional District:
05
Unique Entity Identifier (UEI): EMW9FC8J3HN4
Parent UEI: EMW9FC8J3HN4
NSF Program(s): Software & Hardware Foundation
Primary Program Source: 01001516DB NSF RESEARCH & RELATED ACTIVIT
Program Reference Code(s): 7923, 7943
Program Element Code(s): 779800
Award Agency Code: 4900
Fund Agency Code: 4900
Assistance Listing Number(s): 47.070

ABSTRACT

Title: SHF:Small:New Frontiers in Constraint-Based Program Analysis

Constraint-based analysis is a popular approach to program analysis: it allows to separate analysis specification from analysis implementation, it enables sophisticated implementations by leveraging advances in off-the-shelf solvers, and it provides natural program specifications as constraints. This project proposes Dominoes, a framework that extends the benefits of constraint-based analysis by enabling automatic synthesis of common and emerging use-cases of program analyses, such as finding good abstractions, analyzing incomplete programs, and incorporating user feedback. The intellectual merit of this project is to fundamentally advance demand-driven, compositional, and learning-based analysis techniques. By automatically synthesizing use-cases once and for all, Dominoes amplifies the traditional benefits of constraint-based analysis, liberating analysis designers from having to re-implement those use-cases for their analyses. The project's broader significance and importance lies in enhancing the applicability and usefulness of program analyses by making them more automated, scalable, and flexible. Artifacts embodying these analyses will improve software quality in aspects of reliability, security, performance, and energy efficiency. Dominoes will also improve the productivity of analysis users by allowing them to adapt analyses to their feedback.

Dominoes automatically synthesizes implementations of use-cases for any program analysis expressed in Datalog, a popular declarative logic programming language. Existing constraint-based analysis frameworks predominantly focus on solving hard constraints, whereas Dominoes also accommodates soft constraints that arise naturally in diverse use-cases of program analysis, e.g., to model various tradeoffs, intuitions of analysis users, and missing program specifications. The versatility of Dominoes is demonstrated by applying it to three important use-cases: client-driven analysis, summary-based analysis, and user-guided analysis. Despite their diversity, all three use-cases entail solving instances of the maximum satisfiability (MaxSAT) problem, which consists of a combination of hard (inviolable) constraints and soft (violable) constraints. Solving such mixed constraints is not only computationally hard but also poses the problem of specifying weights or confidences of soft constraints. Dominoes develops MaxSAT optimizations comprising demand-driven, compositional, and learning-based methods that are general and independent of any analysis, use-case, or solver, and aim to scale to instances well beyond the reach of existing MaxSAT solvers.

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.

Ravi Mangal, Xin Zhang, Aditya Kamath, Aditya V. Nori, Mayur Naik. "Scaling Relational Inference Using Proofs and Refutations." AAAI'16: Conference on Artificial Intelligence. , 2016
Ravi Mangal, Xin Zhang, Aditya V. Nori, Mayur Naik. "Volt: A Lazy Grounding Framework for Solving Very Large MaxSAT Instances." SAT'15: International Conference on Theory and Applications of Satisfiability Testing. , 2015
Xin Zhang, Ravi Mangal, Aditya V. Nori, Mayur Naik. "Query-Guided Maximum Satisfiability." POPL'16: ACM Symposium on Principles of Programming Languages. , 2016

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

Print this page

Back to Top of page