• Encode nonfunctional requirements
• Prune the synthesis search space

New Release: Synudic Tool Code and Examples

Older Release: Synthesis Tool: Code and Examples

• README: See readme file for requirements and how to run the tool
• prog_synth.py: The main program
• sexpParser.py: Used by the main program
• oeap.sketch: Sketch for synthesizing padding schemes
• ot.sketch: Sketch for synthesizing oblivious transfer protocol

Documentation

• Summary.pdf: A report summarizing the work around synthesis of cryptographic protocols.
• synudic.pdf: Paper describing the Synudic approach.
• dual.pdf: A new paper describing an extension of the Synudic approach, where primals are not used!
• report.pdf: See for details of the language, tool, case study and results.

References:

• Ashish Tiwari, Adria Gascon, Bruno Dutertre: Program Synthesis Using Dual Interpretation. CADE 2015: 482-497
  

  @inproceedings{DBLP:conf/cade/TiwariGD15,
    author    = {Ashish Tiwari and Adria Gascon and Bruno Dutertre},
    title     = {Program Synthesis Using Dual Interpretation},
    booktitle = {Automated Deduction - {CADE-25} - 25th International Conference on
                 Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings},
    series    = {LNCS},
    volume    = 9195,
    pages     = {482--497},
    year      = {2015},
    url       = {http://dx.doi.org/10.1007/978-3-319-21401-6_33},
    doi       = {10.1007/978-3-319-21401-6_33},
  }
   

Talks

• "Synthesis using EF-SMT Solvers". Slides (pdf), Talk presented at the 3rd Workshop on Synthesis, Colocated with FLoC 2014, July 2014, Vienna.