Wiki Agenda Contact Version française

Publications : Thierry Hubert

Back
[8] Thierry Hubert. Analyse Statique et preuve de Programmes Industriels Critiques. Thèse de doctorat, Université Paris-Sud, June 2008. [ bib | .pdf ]
[7] Jean-François Couchot and Thierry Hubert. A Graph-based Strategy for the Selection of Hypotheses. In FTP 2007 - International Workshop on First-Order Theorem Proving, Liverpool, UK, September 2007. [ bib | PDF | .pdf ]
In previous works on verifying C programs by deductive approaches based on SMT provers, we proposed the heuristic of separation analysis to handle the most difficult problems. Nevertheless, this heuristic is not sufficient when applied on industrial C programs: it remains some Verification Conditions (VCs) that cannot be decided by any SMT prover, mainly due to their size. This work presents a strategy to select relevant hypotheses in each VC. The relevance of an hypothesis is the combination of two separated dependency analysis obtained by some graph traversals. The approach is applied on a benchmark issued from an industrial program verification.

[6] Thierry Hubert and Claude Marché. Separation analysis for deductive verification. In Heap Analysis and Verification (HAV'07), pages 81--93, Braga, Portugal, March 2007. [ bib | full text on HAL ]
[5] Thierry Hubert and Claude Marché. Separation analysis for deductive verification. Technical report, Université Paris XI, 2007. http://www.lri.fr/~marche/separation.pdf. [ bib | PDF | .pdf ]
[4] Thierry Hubert and Claude Marché. A case study of C source code verification: the Schorr-Waite algorithm. In Bernhard K. Aichernig and Bernhard Beckert, editors, 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), Koblenz, Germany, September 2005. IEEE Comp. Soc. Press. [ bib | .ps ]
[3] Thierry Hubert and Claude Marché. A case study of C source code verification: the Schorr-Waite algorithm. 2005. [ bib | .ps ]
[2] Thierry Hubert. Certification des preuves de terminaison en Coq. Rapport de DEA, Université Paris 7, September 2004. http://www.lri.fr/~marche/hubert04rr.ps. [ bib | .ps ]
[1] Jean-Christophe Filliâtre, Thierry Hubert, and Claude Marché. The Caduceus tool for the verification of C programs. http://caduceus.lri.fr/. [ bib ]

Back
This page was generated by bibtex2html.