Evolutionary Program Sketching (EPS)

Evolutionary Program Sketching (EPS) is an automatic programming method combining Genetic Programming (GP) and formal synthesis based on checking satisfiability of the SMT formula encoding the program. SMT stands for Solvability Modulo Theories, and is an extension of the satisfiability (SAT) problem in the first-order logic in which formulas may contain expressions from certain theories. For example, the theory of integer arithmetic allows to define constraints such as (and (> x 0) (y > 0)), where semantics of the arithmetic operators is provided by the theory. The task of the solver is to find such a valuation of all variables (the model), which satisfies all constraints.

EPS evolves program trees containing holes and evaluates them using SMT solver with optimization utilities. The main idea of this approach was inspired by the paper written by Armando Solar-Lezama et al., where sketch of the program (containing holes) was provided by a user and SMT solver was used to check correctness and generate counterexamples.

In EPS, sketches are being automatically evolved instead. During evaluation phase, a query to SMT solver (e.g. Z3) is generated by the PySV framework. The query is unique in that it asks for a model which maximizes the number of passed test cases (Z3 supports this) instead of simply finding any model.

You may find more details in the paper specified in the How to cite section.

Supported types of the holes

Holes are categorized with regard to the content they may be filled with. Currently there are two supported types of holes: constant holes (may be filled with constant of the certain type) and variable holes (may be filled with any input variable of the synthesized function).

Dependencies

• FUEL - main evolution engine.
• SWIM - GP utilities for FUEL.
• PySV - construction of queries in SMT-LIB language to the SMT solver.

How to build

Scala 2.11.8 must be installed on the system (newer versions were not tested). Currently supported are two methods of building EPS from source:

• Eclipse/ScalaIDE project. Just import the project in the IDE. From there you may run the application or export it to jar.
• SBT. build.sbt is configured so that fuel and swim folders with sources are assumed to be placed at the same directory level as the directory containing EPS folder downloaded from this repository. You can just type in the command line sbt package to produce jar in the target/scalaX.Y directory.

How to run

Scripts for running the main variants of EPS described in the paper (EPS-B, EPS-L) are stored in the scripts folder. Jars of fuel, swim and EPS must be on the classpath (example in the scripts). pysv sources directory is specified with the --eps.pathToPySV option. To get information about other options run jar with -h or --help.

How to cite

@Inbook{Błądek2017,
  author="B{\l}{\k{a}}dek, Iwo
  and Krawiec, Krzysztof",
  editor="McDermott, James
  and Castelli, Mauro
  and Sekanina, Lukas
  and Haasdijk, Evert
  and Garc{\'i}a-S{\'a}nchez, Pablo",
  title="Evolutionary Program Sketching",
  bookTitle="Genetic Programming: 20th European Conference, EuroGP 2017, Amsterdam, The Netherlands, April 19-21, 2017, Proceedings",
  year="2017",
  publisher="Springer International Publishing",
  address="Cham",
  pages="3--18",
  isbn="978-3-319-55696-3",
  doi="10.1007/978-3-319-55696-3_1",
  url="http://dx.doi.org/10.1007/978-3-319-55696-3_1"
}

Bibliography

[1]: Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Sanjit Seshia, and Vijay Saraswat. 2006. "Combinatorial Sketching for Finite Programs". SIGPLAN Not. 41, 11 (Oct. 2006), 404–415.