Aarti Gupta - US grants

Program verification has broad applications, from ensuring safety of mission-critical software to improving program robustness and programmer productivity. Automatic program verification techniques employ various forms of learning to enhance scalability on large programs. These include deductive learning in modern logic-based solvers and learning from counterexamples in abstraction refinement procedures. Modular verification is essential for scaling verification to large software, and concurrent program verification is critical due to the wide prevalence of multi-core hardware.

This project develops techniques for learning inductive invariants for modular verification in a teacher-learner setting. The research objectives include studying suitable languages of invariants at procedure boundaries, identifying requirements for progress in learning, and developing effective techniques for guiding the learner. The project also addresses verification of concurrent programs, where learning over different event sequences is performed by dynamic and predictive analysis over program traces. The goal is to drive the learning toward unexplored program behaviors by automatically generating test inputs. The research objectives include studying new trace abstractions and coverage metrics for concurrent programs, and developing techniques for coverage-guided test generation. The methods for driving learning include directed testing to target specific scenarios relevant for learning. Beyond these specific contributions, the results will provide insights on applying machine learning techniques in combination with static and dynamic analysis for advancing program verification. The project includes development of educational material, tools, and benchmarks that will be made publicly available.

This grant will enable students to attend the Verification Mentoring Workshop (VMW 2015) which will be co-located with the International Conference on Computer Aided Verification (CAV), to be held in San Francisco, July 19-24, 2015. CAV is one of the premier conferences in computer science, dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems. The purpose of Verification Mentoring Workshop is to provide mentoring and career advice to early-stage graduate students, to attract them to pursue research careers in the area of computer-aided verification. Funded students will benefit greatly from the opportunity to engage in the critical technical, professional, and social exchanges that both conferences foster.

Computer-aided verification covers a broad range of applications, from ensuring the correctness and safety of computer systems, to improving design and development productivity. The funded students will attend CAV, a top conference where they will learn about current research problems and interact with leaders in the field, and the VMW workshop which will focus on mentoring and career advice specific to early-stage graduate students who aim to pursue research careers in the area of computer-aided verification.

This grant will enable students to attend the Verification Mentoring Workshop (VMW 2016) which will be co-located with the International Conference on Computer Aided Verification (CAV), in Toronto (Canada), July 17-23, 2016. CAV is one of the premier conferences in computer science, dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems. The purpose of Verification Mentoring Workshop is to provide mentoring and career advice to early-stage graduate students, to attract them to pursue research careers in the area of computer-aided verification. Funded students will benefit greatly from the opportunity to engage in the critical technical, professional, and social exchanges that both conferences foster.

Computer-aided verification covers a broad range of applications, from ensuring the correctness and safety of computer systems, to improving design and development productivity. The funded students will attend CAV, a top conference where they will learn about current research problems and interact with leaders in the field, and the VMW workshop which will focus on mentoring and career advice specific to early-stage graduate students who aim to pursue research careers in the area of computer-aided verification.

Computer networks, whether connecting servers across a data center or users across the globe, are an important part of society's critical infrastructure. However, existing network protocols and services are simply not worthy of the trust society now places in them. Today's networks suffer from poor performance, cyberattacks, configuration errors, software bugs, and more, leading to serious consequences for consumers, businesses, and governments alike. The goal of this project is to enable the design and operation of better networks which requires enabling both innovation (to create better protocols and services) and verification (to ensure these services work correctly). A major part of the functionality of the network depends on the software running in the control plane, which computes routes, collects and analyzes network measurement data, balances load over multiple paths or servers and even hosts in-network applications. This project involves the theory, design, and implementation of OpenRDC, a new platform constructed for programming reliable, distributed network control planes.

The technical core of OpenRDC centers around computations of Stable Information Trees (SITs) that communicate information (e.g., traffic conditions, failure information, available external routes, end-host job statistics, etc.) across a network, and then perform local actions to change network functionality or record information gathered. These structured computations suffice to express core control plane algorithms and yet can also be converted into logical representations that can be used to verify a variety of important properties of operational networks ranging from reachability to access control to multi-path consistency. The OpenRDC platform will simultaneously: (1) allow researchers to develop new control-plane algorithms, (2) enable automatic verification of network properties, and (3) make use of emerging programmable switch capabilities. The project involves acceleration of the development of new control-plane algorithms, via new abstractions for network programming. The project will also define new compiler technology for translating these abstractions to programmable network hardware. In addition, its open source infrastructure will lay a foundation for academic and industrial engagement and for the training of students. The project will also have impact on formal methods, with new algorithms for the verification of graph-oriented programming languages based on abstraction and modular decomposition.

This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

The success of formal methods has enabled widespread applications in ensuring correctness, safety, and reliability of computing systems. This project on automated word-level synthesis is providing a core utility for diverse applications since the bit-vector representation of various computing systems is well-suited for both hardware designs and low-level software. By virtue of the underlying formal reasoning, the programs synthesized by the automated methods are guaranteed to be correct-by-construction, thus improving their quality and improving developer productivity. The two application domains targeted in this project – computer networks and systems-on-chips – form core components of the computing infrastructure that provides numerous products and services of interest to society. The research activities involve training and mentoring graduate students, and development of teaching material.

Real-world applications that require bit-precise reasoning for synthesis and verification, such as in the domains of computer networks and hardware, remain challenging in terms of performance and scalability. One main reason is that existing techniques for synthesis over bitvectors rely largely on a translation of multi-bit words down to bits, called bit-blasting, which destroys the high-level structure in the application programs. This project aims to improve automated synthesis of word-level bit-precise programs, with applications in network packet processing and verification of systems-on-chip (SoCs). The core research activities include development of a new approach to word-level synthesis. The synthesizer is guided by word-level quantifier elimination over bit-vectors without bit-blasting. It also leverages the well-known framework of Syntax-Guided Synthesis (SyGuS), where the search for a program is guided by domain knowledge captured in the form of context-free grammars, program sketches, and partial specifications comprising input-output examples. The project develops suitable grammars and synthesis methods in two application domains: (1) synthesis of code for programmable network switches from high-level packet processing programs, and (2) synthesis of verified architecture-level abstractions from hardware designs of accelerators and processors in modern SoCs. These improve techniques for code generation (from high-level to low-level programs) and verified abstraction (from low-level to high-level programs), respectively.

This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.