Список литературы

1. Карнаухов Н.С., Першин Д.Ю., Шелехов В.И. Язык предикатного программирования P. — Новосибирск, 2009. – 44с. – (Препр. / ИСИ СО РАН; N 153).

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

3. Шелехов В.И. Модель корректности программ на языке исчисления вычислимых предикатов. — Новосибирск, 2007. — 50с. — (Препр. / ИСИ СО РАН; N 145).

4. PVS Specification and Verification System. – SRI International. – http://pvs.csl.sri.com/

5. Basin D., DeVille Y., Flener P., Hamfelt A., and Nilsson J. Synthesis of programs in computational logic // LNCS, 3049.  P.30 – 65, 2004.

6. Sorensen M.H., Urzyczyn P. Lectures on the Curry-Howard Isomorphism. — 2006. — 457 p.

7. E.C.R.Hehner. A Practical Theory of Programming, second edition. – 2004. –

http://www.cs.toronto.edu/~hehner/aPToP/

8. O'Leary J., Leeser M., Hickey J., Aagaard M. Non-Restoring Integer Square Root: A Case Study in Design by Principled Optimization. // Theorem Provers in Circuit Design, 1994 – P.52-71.

9. Creitz C. Derivation of a fast integer square root algorithm. – 2003. –

http://www.nuprl.org/Algorithms/03cucs-intsqrt.pdf.

10. Srivastava S., Gulwani S., and Foster J. From Program Verification to Program Synthesis. –POPL, 2010. – P. 313-326.

11. Шелехов В.И. Предикатное программирование. Учебное пособие. — НГУ, Новосибирск, 2009. — 109с.

12. Souris J., Wiels V. Delmas D. and Delseny H. Formal Verification of Avionics Software Products // LNCS, 5850. – P.532 – 546, 2009.

13. O'Halloran C. Guess and Verify – Back to the Future // LNCS, 5850. – P.23 – 32, 2009.

14. Ball T., Hackett B., Lahiri S., Qadeer S. and Vanegue J. Towards scalable modular checking of user-defined properties // LNCS, 6217. – P.1 – 24, 2010.

15. C. A. R. Hoare. An axiomatic basis for computer programming // Communications of the ACM, 12(10). – P. 576 – 580, 1969.

16. Floyd R. Assigning meanings to programs // Mathematical Aspects of Computer Science. – P. 19–32, 1967.

17. Cohen E., Dahlweid M., Hillebrand M., Leinenbach D., Moskal M., Santen T., Schulte W., Tobies S. VCC: A Practical System for Verifying Concurrent C // LNCS, 5674, P. 1–22. 2009.

18. Ануреев И.С., Марьясов И.В., Непомнящий В.А. Верификация C-программ на основе смешанной аксиоматической семантики // Моделирование и анализ информационных систем, Ярославский государственный университет, т. 17, № 3, 2010, c. 5-28.

1 «математик-верификатор» было бы, возможно, более подходящим переводом для «verifiсation engineer»

2 экспертная оценка автора

3 Здесь и далее термин "корректность"используется в смысле тотальной корректности

4 Однозначность спецификации следует из ее тотальности и формулы (3). Доказана однозначность программы при условии, что все используемые базисные операции являются однозначными

5 Истинность правил определяется как истинность формул, получающихся заменой ├ на .

6 Из стандарта не очевидно, что floor(-0)=0.