See also note on:

  • Constrained Horn Clauses
  • Invariant Synthesis
  • Prolog/Minikanren
  • SMT
  • Inductive logic programming syntax guided synthesis syntehsis withotu syntactic templates RbSyn: Type- and Effect-Guided Program Synthesis Perfect Is the Enemy of Good: Best-Effort Program Synthesis - Peleg PSB2: The Second Program Synthesis Benchmark Suite parser synthesis, grammar




  • Armando Solar-lezama
  • Hila Peleg
  • Yotam Feldman
  • Nadia Polikarpova
  • Isil Dillig
  • rahul sharma

Hoare logic in +-+ mode?

synquid - type driven program synthesis

rosetta? Cosette - sql synthesis

type inference is a form of synthesis

Minikanren - barliman. Inseven examples there is also an interpreter run backwards syntheiss of heap maniuplation programs from seperation lgoic Structuring the Synthesis of Heap-Manipulating Programs Synthesis in reverse engineering Synesthesia

Program Syntehsis book gulwani polozov singh


Induction vampire approach to induction

Chatper of auotmated reasoning handbook

cyclic proofs Induction with Generalization in Superposition Reasoning indcution for smt solvers eydnolds

induction vs termination. Termination is kind of saying that execution is well founded. Induction is saying that the proof is well-founded.

Cyclic Proofs

cycleq cyclegg inductionless induction a cut free cyclic proof system for kleene

Suppose I had a termination certificate of a program. Is induction for the program then easy? Since I can use induction over the structure of the termination certificate (well founded induction)? i mean the program I’ve given is already a proof of some kind.


Bottom Up Enumerative synthesis

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)
;(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?



Question about survey on synethesizing inductive ivanraints

Yotam Feldman answers:

  1. Houdini: invariant inference for conjunctive propositional invariants. I like the exposition in
  2. Interpolation: McMillan’s seminal paper on unbounded SAT-based model checking, which is hugely influential.

  1. 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:
  2. Spacer: PDR for software, with arithmetic, also hugely influential in this domain.
  3. Syntax-guided methods: less familiar with these ones, but I’d hit the survey and work by Grigory Fedyukovich (e.g. syntax guided synthesis sygus-if CVC4 supports it. LoopInvGen, OASES, DryadSynth, CVC4

polikarpova, peleg, isil dillig - automated formal program reapir “fault localization” refinement types constrained horn lcauses. Describes using simple houdini algorithm,. Sara Achour synthesis/compilation for analog computation decided