Polynomial function intervals for floatingpoint software verification

References
(34)
1. Ada Reference Manual, ISO/IEC 8652:2007(E) Ed. 3. Ada Europe (2007). URL http://www.adaic. org/standards/05rm/html/RMTTL.html
2. Abramowitz, M., Stegun, I.A.: Handbook of Mathematical Functions with Formulas, Graphs, and Mathematical Tables, ninth dover printing, tenth gpo printing edn. Dover, New York (1964)
3. Akbarpour, B., Paulson, L.C.: Metitarski: An automatic theorem prover for realvalued special functions. J. Autom. Reasoning 44(3), 175205 (2010)
4. Amey, P.: Correctness by construction: Better can also be cheaper. CrossTalk Magazine pp. 2428 (2002)
5. Barnes, J.: The spark way to correctness is via abstraction. Ada Lett. XX(4), 6979 (2000). DOI http://doi.acm.org/10.1145/369264.369271
6. Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security, 2 edn. AddisonWesley (2003)
7. Barnes, J., Chapman, R., Johnson, R., Widmaier, J., Cooper, D., Everett, B.: Engineering the tokeneer enclave protection software. In: Proceedings of IEEE International Symposium on Secure Software Engineering (2006)
8. Boldo, S.: Floats & Ropes: a case study for formal numerical program verification. In: 36th International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science  ARCoSS, vol. 5556, pp. 91102. Springer, Rhodos, Greece (2009)
9. Boldo, S.: How to compute the area of a triangle: a formal revisit. In: Proceedings of the 21th IEEE Symposium on Computer Arithmetic. Austin, Texas, USA (2013). URL http://hal.inria.fr/ hal00790071
10. Boldo, S., Filliaˆtre, J.C., Melquiond, G.: Combining coq and gappa for certifying floatingpoint programs. In: Calculemus '09/MKM '09: Proceedings of the 16th Symposium, 8th International Conference. Held as Part of CICM '09 on Intelligent Computer Mathematics, pp. 5974. SpringerVerlag, Berlin, Heidelberg (2009). DOI http://dx.doi.org/10.1007/9783642026140 10
 Software (1)

Metrics
No metrics available

 Download from


Cite this publication