Hisseo documents
Publications
PhD thesis
Thi Minh Tuyen Nguyen. Taking architecture and compiler into account
in formal proofs of numerical programs. Thèse de doctorat, Université
Paris-Sud, June
2012. PDF
Articles in International Journals
- Sylvie Boldo and Thi Minh Tuyen Nguyen. Proofs of numerical
programs when the compiler optimizes. Innovations in Systems and
Software Engineering, 7:151-160, 2011.
- Sylvie Boldo and Claude Marché. Formal verification of
numerical programs: from C annotated programs to mechanical
proofs. Mathematics in Computer Science, 5:377-393, 2011.
Keynote Speakers
- Sylvie Boldo. Formal verification of numerical programs: from C annotated programs to Coq proofs. Third International Workshop on Numerical Software Verification, Edinburgh, Scotland, July 2010. NSV-8.
Communications in International Conferences
- Thi Minh Tuyen Nguyen and Claude Marché. Hardware-dependent proofs of
numerical programs. In Jean-Pierre Jouannaud and Zhong Shao, editors,
Certified Programs and Proofs, Lecture Notes in Computer
Science. Springer, December 2011.
- Sylvie Boldo and Thi Minh Tuyen
Nguyen. Hardware-independent proofs of numerical
programs. In Proceedings of the Second NASA Formal Methods Symposium,
NASA Conference Publication, Washington D.C., USA, April 2010.
- Ali Ayad and Claude
Marché. Multi-prover verification
of floating-point programs . In Jürgen Giesl and Reiner Hähnle,
editors, Fifth International Joint Conference on Automated Reasoning,
Lecture Notes in Artificial Intelligence, Edinburgh, Scotland, July
2010. Springer.
Research reports
Software Release