FSU Computer Science Assistant Professor, Dr. Grigory Fedyukovich has been awarded a $449,882 grant from the National Science Foundation titled “Automated Word Level Synthesis for Hardware Code Generation and Verified Abstraction”.
The success of formal methods has enabled widespread applications in ensuring the correctness, safety, and reliability of computing systems. This project on automated word-level synthesis will provide a core utility for diverse applications since the bitvector 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 the core components of the computing infrastructure that provides numerous products and services of interest to society. The research activities will involve training and mentoring graduate students, and the 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 the 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 will include the development of a new approach to word-level synthesis. The synthesizer will be guided by word-level quantifier elimination over bitvectors without bit-blasting. It will also leverage 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 will develop 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 will improve techniques for code generation (from high-level to low-level programs) and verified abstraction (from low-level to high-level programs), respectively.
The project is a collaboration with Prof. Dr. Aarti Gupta at Princeton University.