-
Notifications
You must be signed in to change notification settings - Fork 44
Completed Projects
The following course projects have been completed as a result of this class.
Ethan Chan, Alexander Lin
Refinement types are incredibly useful in guaranteeing program correctness over all inputs in a modular fashion. However, synthesis of intermediate refinement types currently requires the user to provide unintuitive atomic qualifiers to be used as building blocks in synthesis. We propose synthesis of intermediate refinement types through exploration of the grammar of the programming language itself, removing the necessity for atomic qualifiers.
John Sarracino, Alex Gamero-Garrido
We propose Spyder, a technique for synthesizing the Controller in MVC systems from declarative constraints. Programming for the web (and more generally, GUI programming) is hard for many reasons: programmers typically must reason about nonlocal resources (e.g. network images), multiple programming environments (e.g. the HTML DOM and the JavaScript interpreter), and asynchronous events just to develop relatively simple systems. We aim to reduce the burden of programming reactive Model-View systems by replacing tricky cross-cutting reactive logic with program synthesis and constraints. In Spyder, the programmer specifies the relationship between the Model and View as a declarative constraint. From this constraint, as well as local logic for the reactive components, Spyder spins off a correct-by-construction program. In this paper, we develop a prototype implementation of Spyder and evaluate the effectiveness and efficiency of the approach on a simplified example of SSL certificate validation in Android. In addition, we discuss how the technique can be extended to multidimensional arrays, which would allow a broad range of graphical reactive programs to be synthesized.
Dhanya Ganesh, Poornav Sargur
The aim is to make use of a Machine Learning based image recognizer to synthesize underlying tikz code from an image of flow diagrams or hand-drawn diagrams. Machine learning models generalize well to an unseen input-output example and they are robust to noisy inputs. We wish to use these advantages of Machine Learning to synthesize tikz programs from images.