Difference between revisions of "Publications"

From VERASCO
Jump to navigation Jump to search
 
(41 intermediate revisions by 5 users not shown)
Line 6: Line 6:
 
===Technical reports===
 
===Technical reports===
 
* {{bibv|leroy:hal-00703441}} Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart. '''The CompCert memory model, version 2'''. Research report RR-7987, INRIA, June 2012. [http://hal.inria.fr/hal-00703441 At HAL]
 
* {{bibv|leroy:hal-00703441}} Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart. '''The CompCert memory model, version 2'''. Research report RR-7987, INRIA, June 2012. [http://hal.inria.fr/hal-00703441 At HAL]
−
 
  
 
==In 2013==
 
==In 2013==
Line 27: Line 26:
 
===Journal articles===
 
===Journal articles===
  
−
* Gilles Barthe, Delphine Demange, David Pichardie. '''A formally verified SSA-based middle-end. Static Single Assignment meets CompCert'''.  ACM Transactions on Programming Languages and Systems (TOPLAS), 36(1):article 4, March 2014. [http://dx.doi.org/10.1145/2579080 At publisher's]
+
* Gilles Barthe, Delphine Demange, David Pichardie. '''A formally verified SSA-based middle-end. Static Single Assignment meets CompCert'''.  ACM Transactions on Programming Languages and Systems (TOPLAS), 36(1):article 4, March 2014. [http://hal.inria.fr/hal-01097677 At HAL] [http://dx.doi.org/10.1145/2579080 At publisher's]
  
−
* Thomas Braibant, Jacques-Henri Jourdan, David Monniaux. '''Implementing and reasoning about hash-consed data structures in Coq'''.  Journal of Automated Reasoning (JAR), 53(3):271-304, 2014.  [http://hal.inria.fr/hal-00881085 At HAL]
+
* Thomas Braibant, Jacques-Henri Jourdan, David Monniaux. '''Implementing and reasoning about hash-consed data structures in Coq'''.  Journal of Automated Reasoning (JAR), 53(3):271-304, 2014.  [http://hal.inria.fr/hal-00881085 At HAL] [http://dx.doi.org/10.1007/s10817-014-9306-0 At publisher's]
  
−
* Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. '''Verified Compilation of Floating-Point Computations'''. Journal of Automated Reasoning (JAR), 2014.  To appear. [http://hal.inria.fr/hal-00862689 At HAL]
+
* Pierre Roux. '''Innocuous Double Rounding of Basic Arithmetic Operations'''. Journal of Formalized Reasoning, 7(1):131-142, 2014. [https://hal.inria.fr/hal-01091186 At HAL]. [http://jfr.unibo.it/article/view/4359 At publisher's]
  
 
===Conference papers===
 
===Conference papers===
  
−
* Sandrine Blazy, Vincent Laporte and David Pichardie. '''Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code'''. In ''ITP 2014: Interactive Theorem Proving'', pages 128-143.  Lecture Notes in Computer Science 8558, Springer, July 2014.  [http://dx.doi.org/10.1007/978-3-319-08970-6_8 At publisher's]
+
* Sandrine Blazy, Vincent Laporte and David Pichardie. '''Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code'''. In ''ITP 2014: Interactive Theorem Proving'', pages 128-143.  Lecture Notes in Computer Science 8558, Springer, July 2014.  [https://hal.inria.fr/hal-01102445 At HAL] [http://dx.doi.org/10.1007/978-3-319-08970-6_8 At publisher's]
  
 
* Robbert Krebbers, Xavier Leroy and Freek Wiedijk. '''Formal C semantics: CompCert and the C standard'''. In ''ITP 2014: Interactive Theorem Proving'', pages  543-548.  Lecture Notes in Computer Science 8558, Springer, July 2014. [http://hal.inria.fr/hal-00981212 At HAL] [http://dx.doi.org/10.1007/978-3-319-08970-6_36 At publisher's]
 
* Robbert Krebbers, Xavier Leroy and Freek Wiedijk. '''Formal C semantics: CompCert and the C standard'''. In ''ITP 2014: Interactive Theorem Proving'', pages  543-548.  Lecture Notes in Computer Science 8558, Springer, July 2014. [http://hal.inria.fr/hal-00981212 At HAL] [http://dx.doi.org/10.1007/978-3-319-08970-6_36 At publisher's]
  
−
* Alexis Fouilhe and Sylvain Boulmé. '''A certifying frontend for (sub)polyhedral abstract domains'''. In ''Verified Software: Theories, Tools and Experiments (VSTTE) 2014'', pages 200-215.  Lecture Notes in Computer Science 8471, Springer,  July 2014.  [http://hal.archives-ouvertes.fr/hal-00991853 At HAL]
+
* Alexis Fouilhe and Sylvain Boulmé. '''A certifying frontend for (sub)polyhedral abstract domains'''. In ''Verified Software: Theories, Tools and Experiments (VSTTE) 2014'', pages 200-215.  Lecture Notes in Computer Science 8471, Springer,  July 2014.  [http://hal.archives-ouvertes.fr/hal-00991853 At HAL] [http://dx.doi.org/10.1007/978-3-319-12154-3_13 At publisher's]
  
 
===Workshops without proceedings===
 
===Workshops without proceedings===
Line 52: Line 51:
  
 
==In 2015==
 
==In 2015==
 +
 +
===PhD theses===
 +
 +
* Alexis Fouilhé. '''Revisiting the abstract domain of polyhedra : constraints-only representation and formal proof'''.  PhD thesis, Université Grenoble Alpes, October 2015. [https://hal.inria.fr/tel-01286086 At HAL].
 +
 +
* Vincent Laporte. '''Verified static analyzes for low-level languages'''.  PhD thesis, Université Rennes 1, November 2015. [https://hal.inria.fr/tel-01285624 At HAL].
 +
 +
===Journal articles===
 +
 +
* Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. '''Verified Compilation of Floating-Point Computations'''.  Journal of Automated Reasoning (JAR), 54(2):135-163, 2015.  [http://hal.inria.fr/hal-00862689 At HAL] [http://dx.doi.org/10.1007/s10817-014-9317-x At publisher's]
 +
 +
* Érik Martin-Dorel and Guillaume Melquiond. '''Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq'''. Journal of Automated Reasoning (JAR), 2015. [http://hal.inria.fr/hal-01086460 At HAL] [http://dx.doi.org/10.1007/s10817-015-9350-4 At publisher's]
  
 
===Conference papers===
 
===Conference papers===
  
−
* Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie. '''A formally-verified C static analyzer'''. In POPL'15, 42nd symposium Principles of Programming Languages. ACM Press, 2015. To appear. [http://gallium.inria.fr/~xleroy/publi/verasco-popl2015.pdf Local copy] [http://dx.doi.org/10.1145/2676726.2676966 At publisher's]
+
* Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie. '''A formally-verified C static analyzer'''. In ''POPL 2015: 42nd symposium Principles of Programming Languages'', pp 247-259. ACM Press, January 2015. [http://hal.inria.fr/hal-01078386 At HAL] [http://dx.doi.org/10.1145/2676726.2676966 At publisher's]
 +
 
 +
* Sandrine Blazy, Andre Maroneze, and David Pichardie. '''Verified Validation of Program Slicing'''.  In ''CPP 2015: conference on Certified Programs and Proofs'', pp 109-117. ACM Press, January 2015. [https://hal.inria.fr/hal-01110821 at HAL] [http://dx.doi.org/10.1145/2676724.2693169 At publisher's]
 +
 
 +
* Sylvie Boldo. '''Stupid is as Stupid Does: Taking the Square Root of the Square of a Floating-Point Number'''. In ''Proceedings of the Seventh and Eighth International Workshop on Numerical Software Verification'', Electronic Notes in Theoretical Computer Science, pages 50-55, Seattle, WA, USA, April 2015. [http://hal.inria.fr/hal-01148409 At HAL]
 +
 
 +
* Sandrine Blazy, Delphine Demange, David Pichardie. '''Validating Dominator Trees for a Fast, Verified Dominance Test'''.  In ''ITP 2015: 6th international conference on Interactive Theorem Proving'', pp 84-99.  Lecture Notes in Computer Science 9236, Springer, August 2015.  [https://hal.inria.fr/hal-01193281 At HAL]. [http://dx.doi.org/10.1007/978-3-319-22102-1_6 At publisher's].
 +
 
 +
* Sylvain Boulmé, Alexandre Maréchal. '''Refinement to certify abstract interpretations, illustrated on linearization for polyhedra'''.  In ''ITP 2015: 6th international conference on Interactive Theorem Proving'', pp 100-116.  Lecture Notes in Computer Science 9236, Springer, August 2015. [https://hal.inria.fr/hal-01133865 At HAL] [http://dx.doi.org/10.1007/978-3-319-22102-1_7 At publisher's].
 +
 
 +
* Sylvie Boldo. '''Formal Verification of Programs Computing the Floating-Point Average'''.  In ''ICFEM 2015: 17th International Conference on Formal Engineering Methods'', pp 17-32.  Lecture Notes in Computer Science 9407, Springer, November 2015. [https://hal.inria.fr/hal-01174892 At HAL].
 +
 
 +
==In 2016==
 +
 
 +
===PhD thesis===
 +
 
 +
* Jacques-Henri Jourdan. '''Verasco: a formally verified C static analyzer'''.  PhD thesis, Université Paris Diderot (Paris 7), May 2016.  [https://hal.inria.fr/tel-01327023 At HAL]. [https://jhjourdan.mketjh.fr/thesis_jhjourdan.pdf Local copy].
 +
 
 +
===Journal articles===
 +
 
 +
* Sandrine Blazy, Vincent Laporte, and David Pichardie. '''Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code'''. Journal of Automated Reasoning (JAR), 56(3):283-308, 2016. [https://hal.inria.fr/hal-01243700 At HAL]. [http://dx.doi.org/10.1007/s10817-015-9359-8 At publisher's]
 +
 
 +
===Conference papers===
 +
 
 +
* Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, Christian Ferdinand. '''CompCert - A Formally Verified Optimizing Compiler'''.  In ''ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress'', January 2016. [https://hal.inria.fr/hal-01238879 At HAL] [http://www.erts2016.org/ At publisher's].
 +
 
 +
* Alexandre Maréchal, Alexis Fouilhé, Tim King, David Monniaux, Michaël Périn. '''Polyhedral Approximation of Multivariate Polynomials using Handelman's Theorem'''.  In ''VMCAI 2016: International Conference on Verification, Model Checking, and Abstract Interpretation'', January 2016. [https://hal.inria.fr/hal-01223362 At HAL]. [http://dx.doi.org/10.1007/978-3-662-49122-5_8 At publisher's]
 +
 
 +
* Sandrine Blazy,  Vincent Laporte, David Pichardie. '''An Abstract Memory Functor for Verified C Static Analyzers'''. In ''ICFP 2016: 21th International Conference on Functional Programming'', ACM Press, September 2016. [https://hal.inria.fr/hal-01339969v1 At HAL]. [http://doi.acm.org/10.1145/2951913.2951937 At publisher's]
 +
 
 +
* Jacques-Henri Jourdan. '''Sparsity Preserving Algorithms for Octagons'''.  In ''NSAD 2016: Numerical and symbolic abstract domains workshop'', September 2016, Edinburgh, United Kingdom. Electr. Notes Theor. Comput. Sci. 331: 57-70 (2017).  [https://hal.inria.fr/hal-01406795 At HAL]. [https://doi.org/10.1016/j.entcs.2017.02.004 At publisher's]
  
−
==Under submission==
+
==Drafts==
  
−
* Sylvie Boldo. '''How to Compute the Area of a Triangle: a Formal Revisit with  a Tighter Error Bound''', submitted to a journal, Sept 2013. [http://hal.inria.fr/hal-00862653 At HAL]
+
* Sylvie Boldo. '''How to Compute the Area of a Triangle: a Formal Revisit with  a Tighter Error Bound''', Sept 2013. [http://hal.inria.fr/hal-00862653 At HAL]
 +
* Jacques-Henri Jourdan. '''Formalizing Communication Between Numerical Abstract Domains''', March 2015. [http://pauillac.inria.fr/~jjourdan/SAS2015ARTIFACT/paper.pdf Draft]

Latest revision as of 19:14, 3 May 2017

In 2012

Conference papers

  • [Robert_Leroy_CPP2012] Valentin Robert and Xavier Leroy. A formally-verified alias analysis. In Certified Programs and Proofs (CPP 2012), volume 7679 of Lecture Notes in Computer Science, pages 11-27. Springer, December 2012. At HAL

Technical reports

  • [leroy:hal-00703441] Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart. The CompCert memory model, version 2. Research report RR-7987, INRIA, June 2012. At HAL

In 2013

Conference papers

  • [Boldo_et_al_ARITH21] Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. A Formally-Verified C Compiler Supporting Floating-Point Arithmetic. In ARITH, 21st IEEE International Symposium on Computer Arithmetic, pages 91-98. IEEE Press, April 2013. At HAL
  • [Boldo_ARITH21] Sylvie Boldo. How to Compute the Area of a Triangle: a Formal Revisit. In ARITH, 21st IEEE International Symposium on Computer Arithmetic, pages 107-115. IEEE Press, April 2013. At HAL
  • [Blazy_et_al_VSTTE2013] Sandrine Blazy, Vincent Laporte, André Maronèze, and David Pichardie. Formal Verification of Loop Bound Estimation for WCET Analysis. In VSTTE - Verified Software: Theories, Tools and Experiments, volume 8164 of Lecture Notes in Computer Science, pages 281-303. Springer, May 2013. At HAL
  • [Blazy_et_al_SAS2013] Sandrine Blazy, André Maronèze, and David Pichardie. Formal Verification of a C Value Analysis Based on Abstract Interpretation. In 20th Static Analysis Symposium (SAS 2013), volume 7935 of Lecture Notes in Computer Science, pages 324-344. Springer, June 2013. At HAL
  • [Fouilhe_et_al_SAS2013] Alexis Fouilhé, David Monniaux, and Michaël Périn. Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra. In 20th Static Analysis Symposium (SAS 2013), volume 7935 of Lecture Notes in Computer Science, pages 345-365. Springer, June 2013. At HAL
  • [Braibant_Jourdan_Monniaux_ITP2013] Thomas Braibant, Jacques-Henri Jourdan, and David Monniaux. Implementing hash-consed structures in Coq. In Interactive Theorem Proving (ITP 2013), volume 7998 of Lecture Notes in Computer Science, pages 477-483. Springer, July 2013. At HAL

In 2014

Journal articles

  • Gilles Barthe, Delphine Demange, David Pichardie. A formally verified SSA-based middle-end. Static Single Assignment meets CompCert. ACM Transactions on Programming Languages and Systems (TOPLAS), 36(1):article 4, March 2014. At HAL At publisher's
  • Thomas Braibant, Jacques-Henri Jourdan, David Monniaux. Implementing and reasoning about hash-consed data structures in Coq. Journal of Automated Reasoning (JAR), 53(3):271-304, 2014. At HAL At publisher's
  • Pierre Roux. Innocuous Double Rounding of Basic Arithmetic Operations. Journal of Formalized Reasoning, 7(1):131-142, 2014. At HAL. At publisher's

Conference papers

  • Sandrine Blazy, Vincent Laporte and David Pichardie. Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. In ITP 2014: Interactive Theorem Proving, pages 128-143. Lecture Notes in Computer Science 8558, Springer, July 2014. At HAL At publisher's
  • Robbert Krebbers, Xavier Leroy and Freek Wiedijk. Formal C semantics: CompCert and the C standard. In ITP 2014: Interactive Theorem Proving, pages 543-548. Lecture Notes in Computer Science 8558, Springer, July 2014. At HAL At publisher's
  • Alexis Fouilhe and Sylvain Boulmé. A certifying frontend for (sub)polyhedral abstract domains. In Verified Software: Theories, Tools and Experiments (VSTTE) 2014, pages 200-215. Lecture Notes in Computer Science 8471, Springer, July 2014. At HAL At publisher's

Workshops without proceedings

  • Alexis Fouilhe, Sylvain Boulmé and Michaël Périn. Modular and lightweight certification of polyhedral abstract domain. TYPES meeting, May 2014. Abstract
  • Xavier Leroy. Formal verification of a static analyzer: abstract interpretation in type theory. TYPES meeting, May 2014. At HAL

Book chapters

  • Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart. The CompCert memory model. In Andrew W. Appel, Program Logics for Certified Compilers, pp. 237-271. Cambridge University Press, April 2014. At publisher's

In 2015

PhD theses

  • Alexis Fouilhé. Revisiting the abstract domain of polyhedra : constraints-only representation and formal proof. PhD thesis, Université Grenoble Alpes, October 2015. At HAL.
  • Vincent Laporte. Verified static analyzes for low-level languages. PhD thesis, Université Rennes 1, November 2015. At HAL.

Journal articles

  • Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. Verified Compilation of Floating-Point Computations. Journal of Automated Reasoning (JAR), 54(2):135-163, 2015. At HAL At publisher's
  • Érik Martin-Dorel and Guillaume Melquiond. Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq. Journal of Automated Reasoning (JAR), 2015. At HAL At publisher's

Conference papers

  • Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie. A formally-verified C static analyzer. In POPL 2015: 42nd symposium Principles of Programming Languages, pp 247-259. ACM Press, January 2015. At HAL At publisher's
  • Sandrine Blazy, Andre Maroneze, and David Pichardie. Verified Validation of Program Slicing. In CPP 2015: conference on Certified Programs and Proofs, pp 109-117. ACM Press, January 2015. at HAL At publisher's
  • Sylvie Boldo. Stupid is as Stupid Does: Taking the Square Root of the Square of a Floating-Point Number. In Proceedings of the Seventh and Eighth International Workshop on Numerical Software Verification, Electronic Notes in Theoretical Computer Science, pages 50-55, Seattle, WA, USA, April 2015. At HAL
  • Sandrine Blazy, Delphine Demange, David Pichardie. Validating Dominator Trees for a Fast, Verified Dominance Test. In ITP 2015: 6th international conference on Interactive Theorem Proving, pp 84-99. Lecture Notes in Computer Science 9236, Springer, August 2015. At HAL. At publisher's.
  • Sylvain Boulmé, Alexandre Maréchal. Refinement to certify abstract interpretations, illustrated on linearization for polyhedra. In ITP 2015: 6th international conference on Interactive Theorem Proving, pp 100-116. Lecture Notes in Computer Science 9236, Springer, August 2015. At HAL At publisher's.
  • Sylvie Boldo. Formal Verification of Programs Computing the Floating-Point Average. In ICFEM 2015: 17th International Conference on Formal Engineering Methods, pp 17-32. Lecture Notes in Computer Science 9407, Springer, November 2015. At HAL.

In 2016

PhD thesis

  • Jacques-Henri Jourdan. Verasco: a formally verified C static analyzer. PhD thesis, Université Paris Diderot (Paris 7), May 2016. At HAL. Local copy.

Journal articles

  • Sandrine Blazy, Vincent Laporte, and David Pichardie. Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. Journal of Automated Reasoning (JAR), 56(3):283-308, 2016. At HAL. At publisher's

Conference papers

  • Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, Christian Ferdinand. CompCert - A Formally Verified Optimizing Compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, January 2016. At HAL At publisher's.
  • Alexandre Maréchal, Alexis Fouilhé, Tim King, David Monniaux, Michaël Périn. Polyhedral Approximation of Multivariate Polynomials using Handelman's Theorem. In VMCAI 2016: International Conference on Verification, Model Checking, and Abstract Interpretation, January 2016. At HAL. At publisher's
  • Sandrine Blazy, Vincent Laporte, David Pichardie. An Abstract Memory Functor for Verified C Static Analyzers. In ICFP 2016: 21th International Conference on Functional Programming, ACM Press, September 2016. At HAL. At publisher's
  • Jacques-Henri Jourdan. Sparsity Preserving Algorithms for Octagons. In NSAD 2016: Numerical and symbolic abstract domains workshop, September 2016, Edinburgh, United Kingdom. Electr. Notes Theor. Comput. Sci. 331: 57-70 (2017). At HAL. At publisher's

Drafts

  • Sylvie Boldo. How to Compute the Area of a Triangle: a Formal Revisit with a Tighter Error Bound, Sept 2013. At HAL
  • Jacques-Henri Jourdan. Formalizing Communication Between Numerical Abstract Domains, March 2015. Draft
Retrieved from "http://verasco.imag.fr/w/index.php?title=Publications&oldid=384"