-
Notifications
You must be signed in to change notification settings - Fork 39
Completed Projects
The following course projects have been completed as a result of this class in Winter 2023.
JUSTIN DU, RANA LULLA, MELODY RUTH
We present Pebbles, a synthesizer for minimal-depth Boolean circuits which uses bottom-up enumeration with observational equivalence reduction, top-down constraint propagation, and counterexample guided inductive synthesis. On the SyGuS Cryptographic Circuit benchmarks, Pebbles is 10–10,000× faster than CVC4. Furthermore, Pebbles’ specialized thread-safe data structures enable parallel execution on a GPU, yielding an additional 38× speedup.
EMMANUEL ANAYA-GONZALEZ, ADITYA GIRIDHARAN, COLE KURASHIGE
Applications of e-graphs to program synthesis have seen a rise in popularity in recent years. The efficient equality saturation workload that they enable has made then an ideal tool for program search and optimization. However, domains in which syntactic equivalence does not imply semantic equivalence - or vice-versa - face performance penalties caused by this discrepancy. A prototypical example is the untyped lambda calculus, in which the meaning of a variable name depends on the context in which it is used. Alpha-equivalence and the non-locality of the definition of Beta-reduction lead to a cumbersome implementation as purely syntactic rewrite rules, which in turn result in bigger e-graphs and more expensive equality saturation. In this project, we explore different mitigations for these issues.
CHRISTOPHER PRIEBE and MATTHEW PENG
In this project, we plan to compare two superoptimizers for RISC-V assembly code, each one using one of the two aforementioned program generation techniques. For the enumerative approach, we will be using LENS as the search algorithm (Phothilimthana et al., 2016). For the stochastic approach, we will be using an incomplete stochastic search with Markov Chain Monte Carlo (Schkufza et al., 2013). We intend to reimplement both tools in Python and test them against a shared set of benchmarks.
RACHEL S. LIM and DARLENE JIANG
ALEXANDER YU and ARJUN SAMPATH
Recent work in program synthesis has demonstrated the ability to generate structurally recursive functional programs from non- recursive expressions. We present a similar approach to synthesizing functional programs from input-output examples. Synthesizing
ML-like languages can be difficult due to its expressive nature, featuring algebraic data types and recursive functions. Our method addresses this challenge by using a combination of bottom-up enumeration and top-down propagation, first by generating candidate components for using input output example, pruning inconsistent programs, and later through with top-down propagation leveraging these candidates. We implement our approach in a tool called Mono and evaluate it on basic synthesis benchmarks.
SANDHYA JAYARAMAN, VENKAT KRISHNAMOHAN, NICOLAS NEBEL
SnipPy is a Programming By Examples (PBE) small-step synthesizer that currently supports synthesis on a small subset of Python. It has been demonstrated in a study that SnipPy allowed users to solve harder problems faster, and that for certain types of queries, users preferred it to searching the web. However, SnipPy’s grammar is still quite restrictive. We implemented an extension to SnipPy called FunPy that adds user-defined functions to the synthesizer’s grammar. We observed code reuse through user-defined functions can expand SnipPy’s synthesis capabilities significantly. We evaluated FunPy on 4 custom benchmarks that highlight the ability of FunPy to use 1) recursive user-defined functions 2) user-defined functions that use library functions, and 3) compose various user-defined functions to solve synthesis tasks.
MINH VO, PRAVEEN RAMESH, ADITYA SHARMA
In this paper, we describe Blink+Fill, and extension to BlinkFill that allows for matching against concatenated base BlinkFill tokens. We describe the implementation of token concatenation, as well as a user interactivity extension for synthesizing outputs. We find that token concatenation can help with the expressiveness of BlinkFill, allowing for generation of outputs that base BlinkFill would fail. However, token concatenation support comes at a big runtime cost, and is not sufficient to replace certain base BlinkFill tokens such as αs.
The following course projects have been completed as a result of this class in Winter 2022.
SHUHUA XIE, ETHAN NAGOLA, and SHIKHA DIXIT
Input-output examples are a simple and accessible way of describing program behaviour. We present SnapFill, a PBE tool that re-implements the core features of BlinkFill in Python and extends it towards conditionals. While not typically used for synthesis, Python as the language of choice allows us to achieve a better understanding of the algorithm. Given the goal of synthesizing with relatively few examples, using Python does not pose a performance issue. Furthermore, since SnapFill is not integrated with any spreadsheet like tool, the programs must be exported somehow in order for the synthesized scripts to be useful. We have chosen to output python programs that can process csv files, which we believe is reasonably suited for nearly any application of this tool. SnapFill is available at: https://github.com/shuhua-xie/SnapFill
MARK BARBONE, ELIZAVETA PERTSEVA, and JOEY RUDEK
Despite their utility and ubiquity, regular expressions (regexes) are a common pain point for novice and experienced programmers alike. Programmers can intuitively provide behavioral descriptions of regexes; hence, a popular approach for regex generation is programming by example (PBE). State of the art PBE synthesizers typically need negative examples to narrow their search space, which can be difficult for users to come up with. Thus we present Regex+, a novel synthesizer which generates regexes from only positive examples through a combination of version space algebra (VSA) algorithms extended from BlinkFill [9] and ranking techniques informed by logistic regression.
MEGAN CHU, WEI-CHENG HUANG, and MAYANK SHARAN
Program synthesis for well-specified programs, especially programming by example (PBE), is a well studied area with widely accepted solutions that employ constraint-based or enumerative search. Stochastic search methods like genetic programming (GP) have had success in the related domain of program repair. However, there have been surprisingly limited attempts at applying genetic programming methods to program synthesis tasks or performing comparisons on standard benchmarks with existing state-of-the-art methods. In this work, we present our implementation of a genetic programming-based synthesizer (GPSolver) for SyGuS PBE tasks. We also present a comparison with EUSolver which shows that GPSolver can outperform it in the number of benchmarks solved with the correct set of hyperparameters.
YORK LIU, RUOCHEN WANG, and JIARUI HAN
In this project we implemented bottom-up enumeration with observational equivalence using egg. Instead of storing one program per equivalence class, we store all of the explored inside an e-graph. We implemented our method in a tool called EgSolver and compared our method with a baseline solver that only stores one program per equivalence class.
JIACHEN NIU and XUANDA YANG
Equality saturation is a powerful technique that operates on e-graph to implement optimizers and program synthesizers. Recently, the egg framework improved the equality saturation to make it faster and extensible. In our project, we follow the egg paper and re-implement the core algorithm in Python, aiming to provide a easy-to-understand and correct framework.
ABHISHEK SHARMA and AIDAN DENLINGER
SuSLik is an implementation of Synthetic Separation Logic (SLL) which is a framework for deductive synthesis of imperative programs with pointers. Since the synthesis procedure corresponds to a proof search, the derived programs are correct by construction and are guaranteed to satisfy the pre/postconditions in the specification. However, these guarantees can only be as strong as the abstractions that SuSLik currently supports in its specification language allows. An example of this is that SuSLiK currently supports only Sets and Intervals to abstractly model the collection of Integers in a Linked List. Because of this, the programs synthesized by SuSLik for operations on Linked Lists like copy and append can only guarantee that the set/range of items in the output is the same but cannot guarantee that the correct ordering of items is preserved. In this project we modify SuSLik and some of the rules in its underlying logic to allow the use of Sequences in specifications. With this, we are now able to synthesize new programs and provide stronger guarantees to the existing programs that can take advantage of the properties of Sequences. The code is accessible at https://github.com/abhishekc-sharma/suslik/tree/wi22-cse291/sequences.
PATRICK BROWN, RICHARD GU, and ALEX MARTAKIS
Searching for desired programs in a space of possible programs is a challenge in programming synthesis. The tool Euphony, a program built atop of EUSolver, made great strides in effective searches by utilizing a Probabilistic High Order Grammar (PHOG) model. In this paper, we demonstrate the robustness of the PHOG model in search-based programming synthesis by implementing n-grams in Euphony and comparing the benchmark results. Our findings displayed that the n-gram model, while powerful in its own right when compared to other models such as Probabilistic Context Free Grammar (PCFG), was not as effective and efficient as the PHOG model for a majority of the benchmarks.
WEICHEN LIU and DUN MA
Pruning based on observational equvalence is a common practices in program synthesis with a bottom-up enumerative search strategy. While such technique can effectively reduce the search space, the terms that leads to the correct programs can be discarded mistakenly due to limited observations. Therefore, in the situation where the observations are constantly updated, e.g. CEGIS, simply discarding the observational equivalent terms can be undesired. In this project, we explored utilizing egg, a rust implementation of e-graphs data structure, for observation equivalence reduction in a bottom-up enumerative synthesizer within CEGIS. We evaluate different variants of egg integration on a bit-vector benchmark in the SyGuS project.
The following course projects have been completed as a result of this class in Winter 2021.
David Cao
Library learning is a general technique for extracting out common auxiliary functions present across a set of input programs. Because of its generality, library learning has found use across a variety of domains, including in augmented program synthesis and graphical structure analysis. However, existing library learning solutions require a trade-off between exhaustiveness (being able to find more hidden common auxiliary functions, but at extremely high compute cost) and speed (being able to find trivial common functions quickly, but being unable to find less trivial common subroutines). Our work uses egg, an efficient implementation of e-graphs in Rust, to create a more efficient library learning approach targeted towards a simple graphical DSL. We evaluate the effectiveness of babble, a prototype which implements this approach, and evaluate its effectiveness on a set of simple library learning examples.
Bili Dong and Mac Lee
Euphony utilizes A* together with PHOG to prioritize the search in program synthesis, which is successful with SyGuS benchmarks. Inspired by AO*, we noticed that Euphony's fixed, left-first unroll policy can be made more flexible to allow for a general unroll prioritization. In this project, we explore several different unroll policies and demonstrate synthesizer performance difference under these policies.
standalone implementation fork of Euphony
Ruanqianqian (Lisa) Huang
A common and intuitive user-synthesizer interaction model (IM) is Programming-by-Example, where the user provides output examples to specify the desired program's behavior on the inputs. However, providing large examples can be tedious. This paper presents Programming by Partial Examples (PBPE), a new IM where the user can provide partial output specifications which are completed by the synthesizer. We pose the following research question: Would a PBPE synthesizer be more usable than one that requires full outputs? A pilot study (N=4) on PopPy, a PBPE synthesizer, shows that it can be more usable because (1) partial output specifications were used extensively and did not increase confusion, and (2) users spent less time per synthesis call providing specifications with PopPy. Results from the pilot study also suggest refinement to the study design.
Chunyu Xia and Zac Blanco
A key challenge with program synthesis when using Programming by Example (PBE) is generating enough examples in the set of constraints such that the synthesized program conforms to a user’s actual desired specifications. In this work we build a system described by Laich et al.. The original work focused on synthesizing code for UI layouts in Android applications with minimal examples. Our project attempts to apply the concepts from that system into the domain of strings on SyGuS problems.
Nathan Liittschwager, Zhiyuan Guo, and Liu Le
This project explores the instantiation of the Neo algorithm on a new domain. The Neo algorithm is an enumerative program synthesizer whose architecture intentionally resembles that of a conflict-driven clause learning SAT solver in that the synthesizer can actually learn the root cause of failed synthesis attempts, and then utilize that knowledge to prune the search space. One of Neo's reputed strengths is its flexibility and adaptivity to new domains. To this end, we adapt Neo to work on the Programming by Example Strings + LIA track for SyGuS by developing a custom component specification for the SyGuS Strings + LIA grammar in terms of Presburger Arithmetic formulas. We also adapt the search strategy to use a Probabilistic Context Free Grammar. We rigorously test the performance of this new instantiation of Neo on the 2018 SyGuS competition benchmarks, and find that the conflict-driven learning framework towards synthesis shows promise for future research efforts.
The following course projects have been completed as a result of this class in Winter 2020
Alex Chew, Avinash Kondareddy
This project introduces an approach to syntax-guided stochastic superoptimization supporting non-linear context-free grammars, and in which the optimization objective is textual similarity. We name this problem superplagiarism. Given a target program, a SyGuS grammar, and a black-box similarity metric, our algorithm synthesizes a rewrite in the grammar which is functionally equivalent to the target program, but is dissimilar with respect to the similarity metric. We describe an MCMC sampling method to explore the program space via a novel set of program mutations, and integrate it into a CEGIS procedure to perform synthesis. We implement and evaluate a prototype of our approach, named SuPl, and demonstrate that it is capable of plagiarizing simple bit-vector programs against a popular fingerprinting-based similarity metric.
Sean Kinzer, Byung Hoon Ahn, and Joon Kyung Kim
One of the central challenges in program synthesis is on accelerating the search over the space of possible programs. Recent work Lee et al. 2018, dubbed Euphony, aims to accelerate the top-down enumerative search by (1) learning a probabilistic higher order grammar and (2) using A* search to efficiently navigate through the space. However, as top-down approach visits numerous unground candidate solutions, search speed of the search depends heavily on the quality of the probabilistic high order grammar learned from the domain. On the other hand, every candidate visited by the bottom-up approach are ground, hence provides an opportunity for an even faster search. As such, this work builds on the idea of using the probabilistic high order grammar for enumerative search to develop Bottom-Up Euphony which uses the probabilistic grammar to prune the search space. Results on the subset of string benchmarks show that the proposed approach finds the solution in 9.82 seconds.
Miranda Go, Edward Chen
Navigator is a Pyret synthesizer that employs type-driven top-down enumeration to find a program that satisfies a student’s test suite and help students understand the importance of writing fully comprehensive test suites. Navigator includes a simple interaction model to enhance the enumerative search strategy and aid in the student’s learning. A small scale user study was conducted to measure the results of the program synthesis tool and gain insights on the educational benefits this tool provides.
Zhao Gang, Shaobo Cui
We extend a SQL synthesizer, Scythe Wang et al. 2017, to work with semi-structured data and synthesize SQL++ queries that conforms with the example inputs and outputs provided by the user. We then propose a type system for semi-structured data in JSON format and SQL++ queries, as well as several possible optimizations to the synthesis procedure based on the type system. We show how these optimizations could potentially handle the enlarged search space of SQL++ queries better than the approach used for SQL synthesis with some examples.
Shuyang Li, Bodhisattwa Prasad Majumder
In this work, we extend DeepCoder Balog et al. 2017, exploring contextualized representation learning approaches with the given behavioral constraints. Specifically, we survey the various neural architectures in place of DeepCoder’s original attribute predictive modelign component and analyze their performance in terms of speedup and synthesis problems solved.
Kasra Ferdowsifard, Allen Ordookhanians
Projection Boxes are a novel live programming paradigm giving instant visual feedback on the runtime value of variables in a program. We extended this idea in SnipPy, a program synthesis framework to allow for direct manipulation of the data through the box itself, using techniques from program synthesis to recommend a new program that could satisfy the modified runtime values. This feature not only allows the programmer to alter the program to get new values, but also be able to change the values and get a new program.
Darya Verzhbinsky, Daniel Wang, Maria Paula Parga Nina
The problem we address is the problem of synthesizing a term of a given type using a set of given components. We test how a top-down solution to type-directed synthesis fares against the currently leading solution for this problem, type-guided abstraction refinement (TYGAR). Our tool is built on top of the same project that introduced TYGAR, H+, only it utilizes top-down synthesis instead. The purpose is to show a comparison of a different program synthesis method compares to TYGAR’s approach. Specifically, we seek to compare speed of synthesis and the quality of synthesized programs, using the same benchmarks for H+.
David Thien, Nico Lehmann
Despite many advances in program synthesis for functional languages, the problem of synthesizing expressions in the untyped lambda calculus remains largely unexplored. In this work we study this problem, identifying that its key challenge is coming up with a practical approach for the definition of behavioral constraints. We develop some general principles serving as the basis to specify functions beyond their extensional behavior. This idea is expressive enough to specify in detail the behavior of functions over a given data encoding. We then show how to extend these principles to build co-specifications for data types and functions on them, unlocking the possibility of automatically deriving data encodings as a product of synthesis. Finally, we implemented these ideas in a prototype enumerative synthesizer proving they are useful in practice to specify the behavior of functions for their synthesis.
Danlu Chen, Zehao Chen, Ziyang Wang
In this project, we successfully induced context free grammars (CFGs) using datalog synthesis with input- output examples, which is a completely novel task in program synthesis. To achieve this, we explored how to encode CFGs using the datalog language and represented the grammar induction problem in the input-output format following ProSynth, a state-of-the-art datalog synthesizer. We also implemented a new rule generator with premises lters to accelerate the synthesizer. We demonstrated our new system can successfully solve two benchmark grammar induction problems, arithmetic expression and Lambda Calculus, in less than one minute.
Kyle Vigil, Scott Howland
In this project we develop a method of polymorphic type driven program synthesis using a Datalog encoding. The synthesizer is fed input argument types, a desired output type, and a component list and encodes everything into a Datalog script. The output of running the generated Datalog code is all simple and complex paths through the components that will produce a correctly typed program. The components, input types, and output type can be defined with concrete, polymorphic, or a mix of both elements which encompasses nearly all (minus some polymorphic component edge cases) of the components available to modern programming languages. The output from the Datalog execution can be decoded and all solution programs reconstructed. We implemented this with a synthesizer called Hooglelog using Haskell-like types and component list as well as a Python based encoder and decoder.
Huanian Song, Manik Narang, Priyan Vaithilingam
Students taking introductory programming courses come from diverse backgrounds. Providing quick and real-time feedback is very important for their learning. Our idea is to use Constraint Based Program Synthesis to generate near real-time hints for introductory programming assignments. We focus our efforts on the Pyret programming language which is built ground up for education - where students are encouraged to write tests first. We built a synthesizer, PyretSketch, that can currently synthesize list-based recursive programs in Pyret from test cases within seconds. We currently generate hints to ensure the students write robust test cases. We also propose methods to generate semantic hints in the future. We evaluate our tool using list programming assignments from the PAPL website.
Evan Johnson, Zijie Zhao
Control flow hijacking techniques have been one of the most dangerous vulnerabilities in software for several decades. The most common method of control flow hijacking is Return Oriented Programming, a technique by which existing code in an application is used by an attacker to achieve the attacker’s goals. Constructing a ROP exploit is a costly time investment, since each attacker has different goals, and each victim application has different code that can be exploited in order to reach those goals. In order to achieve a general method for automatically synthesizing ROP exploits, we develop a technique for synthesizing ROP exploits based on Counter Example Guided Inductive Synthesis, leveraging efficient synthesis techniques used by existing program synthesis tools.
Ziteng Wang
We propose a test-based solution filtering framework, Check+, for the Haskell synthesizer Hoogle+. The underlying principles and strategies are discussed, and we further extend Check+ with optimizations to make real-time input-output generation possible, which includes the transition to SmallCheck and the introduction of the uniform differentiating examples.
Haoliang Wang, Shraddha Barke
Many aspects of human reasoning require learning rules from very little data. Humans can do this, often learning systematic rules from very few examples, and combining these rules to form compositional rule-based systems. However, current successful approaches to program induction require a hand-engineered domain specific language (DSL), constraining the space of allowed programs and imparting prior knowledge of the domain. In this work, we choose the domain of human hand-drawn sketches and present a model which learns the DSL by itself in a bootstrapping way from a small set of examples. Our DSL-synthesis approach can substantially shorten the time taken to synthesize complex programs.
The following course projects have been completed as a result of this class in Fall 2018
Ariel Weingarten, Dylan Lukes, Cora Coleman
There are more than 5 billion mobile devices in use in the world today. To maintain consistency across screen conformations (size and density) developers define user interfaces using constraint-based layout systems. Constraints are capable of expressing conformation-independent layout behavior but require a great deal of error-prone mechanical thinking on the part of the user. We introduce a method for synthesizing layout constraints from mockups. We apply a representation-based search over version space algebras constructed by back propagation of specifications derived from concrete examples down a restricted grammar of linear integer arithmetic constraints. We evaluate our technique on several example layouts and find that we generate equivalent constraints as the ground truth (plus a few thousand extras), and suggest several directions for future work to refine this system.
David Justo, Michael James
We explore large-scale component- and type-based synthesis in Haskell. Popular open source packages contain knowledge beyond their types and natural language documentation about how functions are typically composed. Hoogle Plus seeks to generate community-inspired straight-line code snippets from a type signature and a set of components, utilizing Haskell's strong type system and common function compositions in the wild.
Chris Lamb, Erin McGinnis, Kaiser Pister
Trial and error has previously been the only method to experimentally design and optimize approximate floating point algorithms. Due to the nature of these approximate algorithms, it is computationally straining to produce and verify new designs. Leveraging new advances in real number satisfiability modulo theories solvers (SMT), we construct a program synthesizer to enumeratively generate efficient, approximate copies of previously expensive floating point algorithms. Once an algorithm is generated, we can verify its functionality and the bounds of its approximation across a range of floating points. In this paper we are able to achieve this goal for the inverse square root function.
Shraddha Barke, Rose Kunkel, Qian Xiong
Phonological rules are general principles that apply to all words of a natural class that is defined in terms of phonological properties. We propose constraint based synthesis from examples to the problem of learning phonological rules. The phonological rules are expressed as constraints over the features of speech sounds. We divide the problem into inferring the change and inferring the condition, and give an encoding of these subproblems as SAT queries. Using these SAT queries, together with Z3’s soft constraints, we synthesize Russian devoicing and Korean deaspiration rules. We conclude that constraint-based synthesis is a viable approach for synthesizing phonological rules.
Georgios Sakkas, Jacob Imola
With our ever-increasing demand for fast computing, processors are becoming more complicated than ever before making hardware more susceptible to design and manufacturing bugs. When bugs are present, it is desirable to fix them without replacing the expensive chips if possible. We propose a method for synthesizing a program equivalent to a sequence of faulty assembly instructions using one Turing-complete instruction, subleq. Our method fixes these instruction-level bugs with just the addition of a cheap coprocessor that computes subleq. We synthesize equivalents for single instructions like add and conditional branching as well as sequences of 3-4 instructions. We find that our method usually performs as well their hand-written counterparts, and for sequences of 3-4 instructions, discovers nontrivial shortcuts over the naive method of replacing each instruction individually. Our code can be found at:
John Messerly, Patrick Liu
We explore the use of examples and specifications for building compilers. Tandoph can be given a mixture of specifications and hard examples in a novel (functional) programming language, and uses representation based search to design an x86 compiler that satisfies all constraints. It builds on the older project META II, and can synthesize most x86 compilers that use numbers, variables, conditionals and loops.
Anirudh Shekhawat
We explore an approach for automated completion of API calls. Given a program with holes (missing method invocations), we make use of program analysis and statistical models to predict the most likely method invocation. The project involved designing a static program analysis process to extract useful sequences of method calls from publicly available code, a statistical model to learn the likelihood of sequences, and an algorithm to choose the most optimal completion for a given hole.
The following course projects have been completed as a result of this class in Fall 2017
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.
Anish Tondwalkar, John Renner
We explore using counter-example guided synthesis to infer refinement types. Current techniques compute a Cartesian abstraction of conjunctions over an abstract domain, which fails to scale to the inference of disjunctive invariants, whose running time can be worst-case exponential in the domain. We find that such a counter-example-based approach is even slower than standard approaches, and propose several improvements that might make such an approach more practical.
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.
Hanzheng Li, Zheng Guo
Generic stream fusion is a problem of automatically writing a stream function equivalent to a given list function. We present two approaches to this problem. The first is to rewrite the list function into a stream function, with the help of a set of term-rewriting rules. In the second approach, we compose the stream function via program synthesis, where we generate a program sketch and use component-based synthesis to fill in the holes. We test them on some list functions, and discuss the strengths and limitations of each approach.
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.
Tristan Knoth, Gaurav Mahajan
We present an approach to synthesizing safe control systems for hybrid systems with non-linear dynamics on continuous real domain. By simultaneously searching for both the control program and its corresponding proof of safety, our method reduces the complexity of the control synthesis problem and expresses it as a Counter-Example Guided Inductive Synthesis (CEGIS) problem. Thus, our approach scales effectively and can provide unbounded guarantees about the system’s safety. We also present a variant of CEGIS for use on continuous real domains as well as sufficient conditions necessary for finding solutions to such a problem. We evaluate our techniques by synthesizing a provably safe control system for UAVs working as "data mules". This work, to the best of our knowledge, presents the first such use of CEGIS for non-linear systems on a continuous real-valued domain.
Sourav Anand
The last decade has seen an incredible improvement in GPUs. The major difference between a GPU and a CPU is that a GPU can have a lot of threads which run in parallel. An ideal use case for GPU program is to perform same computations on the elements of an array containing a lot of data points. This project looks into this aspect and proposes a method to synthesize GPU kernels using Input-Output pairs of small sized arrays.
Asbjoern Lystrup
The goal of this project is synthesis of hash functions with pseudorandom distribution. The synthesizer uses stochastic search in the form of genetic programming, with a fitness function based on tests from the NIST statistical analysis suite. The implementation is explained through a review of its components, and results are presented for a long run of the synthesizer.