Статьи

Для знакомства с теоретическими основами дедуктивной верификации и подходами к реализации их инструментальной поддержки мы рекомендуем следующие статьи:

  1. P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles and B. Yakobowski. FRAMA-C, A Software Analysis Perspective // Proceedings of International Conference on Software Engineering and Formal Methods 2012 (SEFM’12), October 2012

  2. Dillon Pariente, Emmanuel Ledinot. Formal Verification of Industrial C Code using Frama-C: a Case Study // Proceedings of First International Conference on Formal Verification of Object-Oriented Software (FoVeOOS'10), June 2010

  3. Yannick Moy. Automatic Modular Static Safety Checking for C Programs // Phd Thesis. January 2009

  4. Romain Bardou. Verification of Pointer Programs Using Regions and Permissions // Thèse de doctorat, Université Paris-Sud, October 2011

  5. Yannick Moy and Claude Marché. Modular inference of subprogram contracts for safety checking // Journal of Symbolic Computation, 2010

  6. Claude Marché. Verification of the functional behavior of a floating-point program: an industrial case study // Science of Computer Programming, March 2014

  7. Ali Ayad. On formal methods for certifying floating-point C programs // Research Report RR-6927, INRIA, 2009

  8. Sylvie Boldo. Floats and Ropes: A Case Study for Formal Numerical Program Verification // Automata, Languages and Programming, 36th Internatilonal Collogquium, ICALP 2009, Rhodes, greece, July 5-12, 2009, Proceedings, Part II

  9. Sylvie Boldo and Thi Minh Tuyen Nguyen. Hardware-independent proofs of numerical programs // Proceedings of the Second NASA Formal Methods Symposium, April 2010

  10. Mickaël Delahaye, Nikolai Kosmatov, Julien Signoles. Common Specification Language for Static and Dynamic Analysis of C Programs // SAC'13 Proceedings of the 28th Annual ACM Symposium on Applied Computing, 2013