For instance: Humanities and Science University Journal
About consortium subscription Contacts
(812) 4095364 Non-commercial partnership
St. Petersburg


"Humanities and Science University Journal" №19 (Physical and mathematical, biological and technical science), 2016

On Specifi cation and Verifi cation of Standard Mathematical Functions

N. V. Shilov, A. V. Promsky
Price: 50 руб.
 The problem of validating standard mathematical functions and libraries is well-recognized by industrial and academic professional community, but still is poorly understood by freshmen and inexperienced developers. The paper gives three examples (from authors’ pedagogical and research experience) when formal specifi cation and verifi cation of standard functions are useful and essential.
Keywords: mathematical functions, standard libraries, formal specifi cation, formal program verifi cation.
1. Harrison, J. Formal verifi cation of square root algorithms. Formal Methods in
System Design, 2003, 22(2), 143–153. doi:10.1023/A:1022973506233
2. Kuliamin, V.V. Standardization and testing of mathematical functions. Lecture
Notes in Computer Science, 2010, 5947, 257–268. doi:10.1007/978-3-642-11486-
3. Kuliamin, V.V. Standardization and testing of mathematical functions in fl oating point numbers. Programming and Computer Software, 2007, 33(3), 154–173.
4. Promsky, A. Verifying the standard C library: the C-light approach. Nepomnyaschy, V.A., Sokolov, V.A. (Eds.) Proceeding of the Third Workshop “Program Semantics,
Specifi cation and Verifi cation: Theory and Applications”, 2012, Nizhniy Novgorod,
Russia, pp. 96–103.
5. Promsky, A.V. Experiments on self-applicability in the C-light verifi cation system. Bulletin of Novosibirsk Computing Center, Computer Science Series, 2013, 35,
6. Kochan, S.G. Programming in C: A complete introduction to the C programming
language (3rd ed.). 2005, USA: Sam’s Publishing.
7. How to make a program that solves the quadratic formula. Retrieved May 15,
2016, from http://www.youtube.com/watch?v=15NbFrBUdu0
8. Write a C++ program that solves quadratic equation to fi nd its roots. Retrieved
May 15, 2016, from http://www.cplusplus.com/forum/general/36313/
9. C++ refernce. Sqrt, sqrtf, sqrtl. Retrieved May 15, 2016, from http://
10. Gries, D. The science of programming. 1981, USA & Germany: SpringerVerlag.
11. Ayad, A., & Marche, C. Multi-prover verifi cation of fl oating-point programs.
Lecture Notes in Artifi cial Intelligence, 2010, 6173, 127–141. doi:10.1007/978-3-642-
12. Monniaux, D. The pitfalls of verifying floating-point computations.
ACM Transactions on Programming Languages and Systems, 2008, 30(3), 1–41.
13. C++ reference. Rand. Retrieved May 15, 2016, from http://en.cppreference.
14. Plauger, P.J. The standard C library. 1992, USA: Prentice Hall.
15. Itsykson, V. The formalism for semantics specifi cation of software libraries.
System Informatics, 2016, 8, 43–52.
Price: 50 рублей
To order