Geodesic
Sketch completion for predicate programs by counterexamples guided synthesis
Prikladnaya Diskretnaya Matematika. Supplement, no. 10 (2017), pp. 151-153 Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice de l'article

Predicate programs are presented in the language P by sets of computable predicates. For programs in P, the formal operational semantics is developed. On the base of this semantics, a formula describing the total correctness of a predicate program with respect to its specification is presented. The problem of sketch completion for programs in P is considered. The sketch of a program is defined as a typical program with arbitrary expressions. The idea of arbitrary expressions is inspired by the synthesis of programs by a sketching method. Arbitrary expressions are synthesized by counterexample guided synthesis method. The correctness formulas for completed programs are generated. Some methods to synthesize expressions are developed. These methods can be successfully used in our project instead of counterexample guided synthesis. The overall project objective is to develop the program synthesis methods starting from a program specification and the specification of additional programs used in the decomposition of the source program. The nearest project objective is to be able to synthesize elementary expressions in constructed programs.
Keywords: predicate programs, formal operation semantics, program synthesis, counterexample guided synthesis, deductive verification. 
@article{PDMA_2017_10_a58,
     author = {M. S. Chushkin},
     title = {Sketch completion for predicate programs by counterexamples guided synthesis},
     journal = {Prikladnaya Diskretnaya Matematika. Supplement},
     pages = {151--153},
     year = {2017},
     number = {10},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/PDMA_2017_10_a58/}
}
TY  - JOUR
AU  - M. S. Chushkin
TI  - Sketch completion for predicate programs by counterexamples guided synthesis
JO  - Prikladnaya Diskretnaya Matematika. Supplement
PY  - 2017
SP  - 151
EP  - 153
IS  - 10
UR  - http://geodesic.mathdoc.fr/item/PDMA_2017_10_a58/
LA  - ru
ID  - PDMA_2017_10_a58
ER  - 
%0 Journal Article
%A M. S. Chushkin
%T Sketch completion for predicate programs by counterexamples guided synthesis
%J Prikladnaya Diskretnaya Matematika. Supplement
%D 2017
%P 151-153
%N 10
%U http://geodesic.mathdoc.fr/item/PDMA_2017_10_a58/
%G ru
%F PDMA_2017_10_a58
M. S. Chushkin. Sketch completion for predicate programs by counterexamples guided synthesis. Prikladnaya Diskretnaya Matematika. Supplement, no. 10 (2017), pp. 151-153. http://geodesic.mathdoc.fr/item/PDMA_2017_10_a58/

[1] Karnaukhov N. S., Pershin D. Yu., Shelekhov V. I., Yazyk predikatnogo programmirovaniya P, Preprint No 153, ISI SO RAN, Novosibirsk, 2010, 42 pp.

[2] Shelekhov V. I., “Semantika yazyka predikatnogo programmirovaniya”, ZONT-15, Novosibirsk, 2015, 15

[3] Chushkin M. S., “Metody deduktivnoi verifikatsii predikatnykh programm”, Tr. 2-i Mezhdunar. konf. “Instrumenty i metody analiza programm”, Kostroma, 2014, 205–214

[4] Solar-Lezama A., Tancau L., Bodik R., et al., “Combinatorial sketching for finite programs”, Proc. ASPLOS XII, ACM, N.Y., 2006, 404–415 | DOI

[5] https://gist.github.com/mchushkin/8e1a6a28fd6d342623cd97cd5fa395ac

[6] Udupa A., Raghavan A., Deshmukh J. V., et al., “TRANSIT: specifying protocols with concolic snippets”, Proc. PLDI'13, ACM, N.Y., 2013, 287–296