Home > Research > Étudiants/Post-docs > Julien Henry (M2R)

Julien Henry (M2R)

Static Analysis by Path Focusing

Thursday 16 June 2011

Years: 2010, 2011 (M2R)
Co-supervisor: David Monniaux
Subject: Static Analysis by Path Focusing
Abstract:

Program verification aims at statically discovering properties on programs, such as the values that can take the different variables during execution. Abstract Interpretation is a technique that computes an over-approximation of the set of these values, since it is impossible to compute the real set in general. This report takes place in the many attempts to improve the precision of static Analysis by Abstract Interpretation. It proposes a technique that takes benefit of SMT-solving to obtain more precise results at reasonable cost.


Publications HAL de Julien,Henry

2014

Conference papers

ref_biblio
Julien Henry, Mihail Asavoae, David Monniaux, Claire Maïza. How to Compute Worst-Case Execution Time by Optimization Modulo Theory and a Clever Encoding of Program Semantics. ACM SIGPLAN/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems 2014, Jun 2014, Edimbourg, United Kingdom. Association for Computing Machinery, pp.1-10, 2014. 〈hal-00998138〉
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00998138/file/Henry_et_al_LCTES2014.pdf BibTex

Theses

ref_biblio
Julien Henry. Static Analysis by Abstract Interpretation and Decision Procedures. Software Engineering [cs.SE]. Université de Grenoble, 2014. English. 〈tel-01102418〉
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01102418/file/these.pdf BibTex
ref_biblio
Julien Henry. Analyse statique par interprétation abstraite et procédures de décision. Logic in Computer Science [cs.LO]. Université de Grenoble, 2014. English. 〈NNT : 2014GRENM037〉. 〈tel-01485202〉
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01485202/file/41754_HENRY_2014_archivage.pdf BibTex

2012

Conference papers

ref_biblio
Julien Henry, David Monniaux, Matthieu Moy. PAGAI: a path sensitive static analyzer. Tools for Automatic Program AnalysiS (TAPAS 2012), Sep 2012, Deauville, France. pp.3, 2012. 〈hal-00718438〉
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00718438/file/pagai_article.pdf BibTex
ref_biblio
Nicolas Halbwachs, Julien Henry. When the Decreasing Sequence Fails. Antoine Miné. SAS 2012 The 19th International Static Analysis Symposium, Sep 2012, Deauville, France. Springer Verlag, 7460, pp.198-213, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-33125-1_15〉. 〈hal-00734340〉
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00734340/file/sas-14.pdf BibTex
ref_biblio
Julien Henry, David Monniaux, Matthieu Moy. Succinct Representations for Abstract Interpretation. Static analysis symposium (SAS), Sep 2012, Deauville, France. Springer, pp.283-299, 2012, Lecture notes in Computer Science. 〈10.1007/978-3-642-33125-1_20〉. 〈hal-00709833〉
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00709833/file/implicitization_article.pdf BibTex

2010

Journal articles

ref_biblio
Franck Chotel, Julien Henry, Romain Seil, Julien Chouteau, Bernard Moyen, et al.. Growth disturbances without growth arrest after ACL reconstruction in children. Knee Surgery, Sports Traumatology, Arthroscopy, Springer Verlag, 2010, 18 (11), pp. 1496-1500. 〈10.1007/s00167-010-1069-5〉. 〈hal-00983736〉
Accès au bibtex
BibTex

Attached documents

  • Report

    16 June 2011
    info document : PDF
    978.6 kb

Valid XHTML 1.0 Transitional
SPIP | | Site Map | Follow site activity RSS 2.0
Graphic design (c) styleshout under License Creative Commons Attribution 2.5 License