| Description | Given a compiler, in our case, GCC 4.7.2, a translation validator checks whether the compiled program has the same behaviour as the source program for all possible runs. This is extremely important in applications like aviation, space missions, etc. where the cost of a bug introduced by a compiler can be exorbitant. Modern compilers perform ~100 optimization passes, making translation validation extremely challenging. A certified translation validator is also required to produce a certificate of correctness of its verdict, that can be independently and efficiently checked by a third party. In this ongoing project, we have developed a translation validator for GCC 4.7.2 based on SAT/SMT solving and static analysis techniques. The current WURP will be focused on developing a compact certificate of correctness and on developing checkers that can efficiently check such certificates. |
|---|---|
| Number of students | 2 |
| Year of study | Students in their 3rd year (Semester 5) |
| CPI | 8.5 and above |
| Prerequisites | Required: Proficiency in C++ programming, good understanding of algorithms and data structures Preferred: General knowledge about compilers, should have used GCC (along with some of its options turned on/off through command line switches), understanding of mathematical logic, prior exposure to SAT/SMT/constraint solvers |
| Duration | 6 months |
| Learning outcome |
|
| Weekly time commitment | 4-5 hours |
| General expectations | Should be willing to collaborate and build on top of a significant codebase developed by others |
| Assignment |
https://people.eecs.berkeley.edu/~necula/Papers/tv_pldi00.pdf
https://llvm.org/pubs/2008-11-PASTE-CompilerValidation.html
https://www.sciencedirect.com/science/article/pii/S1571066104803931
Video link: https://drive.google.com/file/d/14ySrVLp9Ploo6z5_SSRS34XdFoC2C8dP/view?usp=share_link |
| Instructions for assignment | Read the three papers and go through the video, and describe the core ideas in translation validation in a couple of pages. |
| Description | Automatically synthesizing a program or circuit from a specification is one of the holy grails of computer science. In recent years, there has been significant interest and advance in this area. Specifically, our group has designed algorithms and tools that are capable of automatically synthesizing highly non-trivial programs/circuits, like ones that factorize numbers (up to a certain bit-width). In this project, we will be pushing the frontier of this technology further by considering the synthesis of functions from Dependency Quantified Boolean Formulas (DQBF). DQBFs can specify relations between multiple functions (to be synthesized) while specifying which function depends on what variables. This project will be in collaboration with researchers in Germany, with whom we have been working on this project for some time. |
|---|---|
| Number of students | 1-2 |
| Year of study | Students in their 3rd year (Semester 5), Students in their 4th/5th year (Semester 7/9) |
| CPI | 8.5 and above |
| Prerequisites | Good Python coding skills, a good understanding of propositional and quantified Boolean formulas (preferably should have done a logic course), a good understanding of algorithms and data structures. |
| Duration | 6 months, but can be easily extended to a year (working on enhancements) |
| Learning outcome | Learning how to build state-of-the-art automated synthesis tools, understanding the inner workings of SAT, QBF, and DQBF solvers, skill development for modeling and solving real-world problems using constraint solvers. |
| Weekly time commitment | 4-5 hours |
| General expectations | Willingness to dabble with both theory and implementation (as with any meaningful project) |
| Assignment |
An overview talk on program synthesis: https://www.youtube.com/watch?v=-Dpwr1eT4-A Papers to read (details of proofs can be omitted on first reading) https://arxiv.org/pdf/2105.09221.pdf https://arxiv.org/abs/2301.10556 https://rdcu.be/dpvG https://drops.dagstuhl.de/opus/volltexte/2022/16694/pdf/LIPIcs-SAT-2022-20.pdf |
| Instructions for assignment |
1. Summarize the key ideas in the four papers, without talking
of proof details, in about 2 pages 2. Come up with your own list of weaknesses in the papers (it's ok if some of these turn out to be not real weaknesses) |
Dive deep in the realm of Academic and Industry related research projects
Created with ❤️ by UGAC Web Team, 2023-2024