Journal "Software Engineering"
a journal on theoretical and applied science and technology
ISSN 2220-3397

Issue N2 2011 year

Verification and Synthesis of Effective Programs for Standard Functions under Predicate Programming Technology
V. I. Shelekhov , E-mail: vshel@iis.nsk.su

The technology of development of the effective standard functions isqrt, floor, and ilog2 is described. Correctness of the programs is achieved by application of deductive verification and program synthesis methods. The proof of program correctness conditions is supported by the PVS Verification System.

Keywords: predicate programming, deductive verification, program synthesis, total correctness of program
pp. 14–21