Geodesic
Verification and synthesis of addition programs under the rules of statement correctness
Modelirovanie i analiz informacionnyh sistem, Tome 17 (2010) no. 4, pp. 101-110.

Voir la notice de l'article provenant de la source Math-Net.Ru

Deductive verification and synthesis of binary addition programs are performed on the base of the rules of program correctness for statements of the predicate programming $P$ language. The paper presents the sketch of verification and synthesis of the programs for the Ripple carry, Carry look-ahead and Ling adders. The correctness conditions of the programs were translated into the specification language of the PVS verification system. The time needed to prove the program correctness conditions in the PVS is more than the time of the ordinary programming by a factor of 10. However, for program synthesis, development of PVS theories and proofs are easier and faster than that for program verification.
Keywords: predicate programming, deductive verification, program synthesis, total correctness of program. 
@article{MAIS_2010_17_4_a10,
     author = {V. I. Shelekhov},
     title = {Verification and synthesis of addition programs under the rules of statement correctness},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {101--110},
     publisher = {mathdoc},
     volume = {17},
     number = {4},
     year = {2010},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a10/}
}
TY  - JOUR
AU  - V. I. Shelekhov
TI  - Verification and synthesis of addition programs under the rules of statement correctness
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2010
SP  - 101
EP  - 110
VL  - 17
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a10/
LA  - ru
ID  - MAIS_2010_17_4_a10
ER  - 
%0 Journal Article
%A V. I. Shelekhov
%T Verification and synthesis of addition programs under the rules of statement correctness
%J Modelirovanie i analiz informacionnyh sistem
%D 2010
%P 101-110
%V 17
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a10/
%G ru
%F MAIS_2010_17_4_a10
V. I. Shelekhov. Verification and synthesis of addition programs under the rules of statement correctness. Modelirovanie i analiz informacionnyh sistem, Tome 17 (2010) no. 4, pp. 101-110. http://geodesic.mathdoc.fr/item/MAIS_2010_17_4_a10/

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

[2] V. Shelekhov, “The language of calculus of computable predicates as a minimal kernel for functional languages”, BULLETIN of the Novosibirsk Computing Center. Series: Computer Science, 29, IIS Special Issue (2009), 107–117

[3] V. I. Shelekhov, Model korrektnosti programm na yazyke ischisleniya vychislimykh predikatov, Prepr. No 145, ISI SO RAN, Novosibirsk, 2007, 50 pp.

[4] M. J. Flynn , S. F. Oberman, Advanced computer arithmetic design, Wiley, New York, 2001, 344 pp. http://en.wikipedia.org/wiki/Adder_(electronics) | MR

[5] S. Owre, J. M. Rushby, N. Shankar, “PVS: A Prototype Verification System”, LNCS, 607, 1992, 748–752 http://pvs.csl.sri.com/

[6] M. H. Sorensen, P. Urzyczyn, Lectures on the Curry-Howard Isomorphism, Logic and the Foundations of Mathematics, 149, 2006, 457 pp.

[7] V. I. Shelekhov, “Verifikatsiya i sintez effektivnykh programm standartnykh funktsii floor, isqrt i ilog2 v tekhnologii predikatnogo programmirovaniya”, Tr. 12-i mezhd. konf. “Problemy upravleniya i modelirovaniya v slozhnykh sistemakh”, Samarskii nauchnyi tsentr RAN, 2010, 622–630

[8] E. C. R. Hehner, A Practical Theory of Programming, ON M5S 2E4, second edition, University of Toronto, 2004, 242 pp. http://www.cs.toronto.edu/~hehner/aPToP/

[9] R. W. Doran, “Variants of an Improved Carry Look-Ahead Adder”, IEEE Transactions on Computers, 37:9 (1988), 1110–1113 | DOI | MR

[10] D. Basin, Y. DeVille, P. Flener, A. Hamfelt, J. Nilsson, “Synthesis of programs in computational logic”, LNCS, 3049, 2004, 30–65 | Zbl

[11] S. Srivastava, S. Gulwani, J. Foster, “From Program Verification to Program Synthesis”, POPL, 2010, 313–326

[12] D. Kapur, M. Subramaniam, “Mechanical verification of adder circuits using Rewrite Rule Laboratory”, Formal Methods in System Design, 13:2 (1998), 127–158 | DOI