Synthesis
See also note on:
- Constrained Horn Clauses
- Invariant Synthesis
- Prolog/Minikanren
- SMT
Sketch
Courses:
People:
- Armando Solar-lezama
- Hila Peleg
- Yotam Feldman
- Nadia Polikarpova
- Isil Dillig
- rahul sharma
https://github.com/logic-and-learning-lab/Popper
synquid - type driven program synthesis
rosetta?
Minikanren - barliman. Inseven examples there is also an interpreter run backwards
https://github.com/TyGuS/suslik syntheiss of heap maniuplation programs from seperation lgoic
https://www.youtube.com/watch?v=mFjSbxV_1vw&ab_channel=Fastly Synthesis in reverse engineering Synesthesia
Alternating Quantifiers
Exists forall problems
There exists instanitations of holes in your program such that for all possible inputs, the program is correct. Vaguely speaking: \(\exists H \forall x \phi(x)\)
However, what is phi? One approach would be to define it using weakest precondition semantics. Or strongest postcondition
\[\exists H \psi(H) \land \forall x pre(x) \rightarrow WP(Prog,post(x))\]\(\forall\) is kind of like an infinite conjunction. For finite types you’re quantifying it over, you can expand it into conjunction. \(\forall c \phi(c) = \phi(red) \land \phi(blue) \land \phi(green)\)
You can also attempt to partially expand these quantifiers as a method to solve the alternating quantifier problem. This is CEGIS
\[\exists H. finite expansion\]In some sense, constraint solvers/smt/mathematical programming solvers are solving problems with implicit existential quantification over all the free variables.
Fixing the synthesis parameters, we
inductive logic programming
Syntax Guided Synthesis (Sygus)
Sygus - syntax guided synthesis demo of sygus sygus 2 compatbile with smtlib2? search based program synthesis
(set-option :lang sygus2)
()
;(check-synth)
;(define-fun spec ((x (BitVec 4)) (y BitVec 4)) (BitVec 4)
; (ite (bvslt x y) y x)
;)
invariant synthesis: Spec = Inv /\ body /\ Test' => Inv'
Proof synthesis?
Sketch
PDR
Question about survey on synethesizing inductive ivanraints
Yotam Feldman answers:
- Houdini: invariant inference for conjunctive propositional invariants. I like the exposition in https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.153.3511&rep=rep1&type=pdf
- Interpolation: McMillan’s seminal paper on unbounded SAT-based model checking, which is hugely influential.
https://people.eecs.berkeley.edu/~alanmi/courses/2008_290A/papers/mcmillan_cav03.pdf
- IC3/PDR: Another hugely influential technique, originally also for propositional programs. I like the exposition in the extension to universally quantified invariants over uninterpreted domains: https://tau.ac.il/~sharonshoham/papers/jacm17.pdf
- Spacer: PDR for software, with arithmetic, also hugely influential in this domain. https://t.co/gVlNrL6xts
- Syntax-guided methods: less familiar with these ones, but I’d hit the survey https://sygus.org/assets/pdf/Journal_SyGuS.pdf and work by Grigory Fedyukovich (e.g. https://ieeexplore.ieee.org/document/8603011)
https://www.youtube.com/watch?v=-eH2t8G1ZkI&t=3413s syntax guided synthesis sygus-if https://sygus.org/ CVC4 supports it. LoopInvGen, OASES, DryadSynth, CVC4
polikarpova, peleg, isil dillig
https://www.youtube.com/watch?v=h2ZsstWit9E&ab_channel=SimonsInstitute - automated formal program reapir “fault localization” https://github.com/eionblanc/mini-sygus
https://arxiv.org/pdf/2010.07763.pdf refinement types constrained horn lcauses. Describes using simple houdini algorithm,.