Sites Inria

English version

Equipe de recherche GALLIUM

Publications de l'équipe GALLIUM

2019

Communication dans un congrès

titre
Formal Proof and Analysis of an Incremental Cycle Detection Algorithm
auteur
Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, François Pottier
article
ITP 2019 - 10th Conference on Interactive Theorem Proving, Sep 2019, Portland, United States
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02167236/file/main.pdf BibTex
titre
Time Credits and Time Receipts in Iris
auteur
Glen Mével, Jacques-Henri Jourdan, François Pottier
article
ESOP 2019 - European Symposium on Programming, Apr 2019, Prague, Czech Republic. pp.3-29, ⟨10.1007/978-3-030-17184-1_1⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-02183311/file/main.pdf BibTex
titre
Provably and Practically Efficient Granularity Control
auteur
Umut Acar, Vitaly Aksenov, Arthur Charguéraud, Mike Rainey
article
PPoPP 2019 - Principles and Practice of Parallel Programming, Feb 2019, Washington DC, United States. ⟨10.1145/3293883.3295725⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01973285/file/long_version.pdf BibTex
titre
Learn-OCaml : un assistant à l'enseignement d'OCaml
auteur
Cagdas Bozman, Benjamin Canou, Roberto Di Cosmo, Pierrick Couderc, Louis Gesbert, Grégoire Henry, Fabrice Le Fessant, Michel Mauny, Carine Morel, Loïc Peyrot
article
Journées Francophones des Langages Applicatifs (JFLA), Jan 2019, Les Rousses, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01962838/file/main.pdf BibTex

Ouvrage (y compris édition critique et traduction)

titre
Cybersecurity
auteur
Steve Kremer, Ludovic Mé, Didier Rémy, Vincent Roca
article
Inria, pp.172, 2019, Inria white book
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01993308/file/Livre%20blanc%20Cybers%C3%A9curit%C3%A9%20Inria.pdf BibTex

2018

Article dans une revue

titre
A Principled Approach to Ornamentation in ML
auteur
Thomas Williams, Didier Rémy
article
Proceedings of the ACM on Programming Languages, ACM, 2018, pp.1-30. ⟨10.1145/3158109⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01666104/file/ornaments-popl18-final.pdf BibTex

Communication dans un congrès

titre
Disornamentation
auteur
Lucas Baudin, Didier Rémy
article
ML 2018 - ML Family Workshop, Sep 2018, St. Louis, Missouri, United States
Accès au bibtex
BibTex
titre
Brief Announcement: Performance Prediction for Coarse-Grained Locking
auteur
Vitalii Aksenov, Dan Alistarh, Petr Kuznetsov
article
PODC 2018 - ACM Symposium on Principles of Distributed Computing, Jul 2018, Egham, United Kingdom. ⟨10.1145/3212734.3212785⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01887733/file/main.pdf BibTex
titre
Ornamentation put into Practice in ML
auteur
Didier Rémy
article
Seventh Workshop on Mathematically Structured Functional Programming (MSFP 2018), Jul 2018, Oxford, United Kingdom
Accès au bibtex
BibTex
titre
A more precise, more correct stack and register model for CompCert
auteur
Gergö Barany
article
LOLA 2018 - Syntax and Semantics of Low-Level Languages 2018, Jul 2018, Oxford, United Kingdom
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01799629/file/LOLA_2018_paper_4.pdf BibTex
titre
Embedded Program Annotations for WCET Analysis
auteur
Bernhard Schommer, Christoph Cullmann, Gernot Gebhard, Xavier Leroy, Michael Schmidt, Simon Wegener
article
WCET 2018: 18th International Workshop on Worst-Case Execution Time Analysis, Jul 2018, Barcelona, Spain. ⟨10.4230/OASIcs.WCET.2018.8⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01848686/file/wcet2018_embedded_program_annotations.pdf BibTex
titre
Heartbeat scheduling: provable efficiency for nested parallelism
auteur
Umut Acar, Arthur Charguéraud, Adrien Guatto, Mike Rainey, Filip Sieczkowski
article
PLDI’18 - 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, Jun 2018, Philadelphia, United States. ⟨10.1145/3192366.3192391⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01937946/file/pldi_final_with_appendix.pdf BibTex
titre
On Helping and Stacks
auteur
Vitalii Aksenov, Petr Kuznetsov, Anatoly Shalyto
article
The International Conference on Networked Systems, May 2018, Essaouira, Morocco
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01888607/file/main.pdf BibTex
titre
A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification
auteur
Armaël Guéneau, Arthur Charguéraud, François Pottier
article
ESOP 2018 - 27th European Symposium on Programming, Apr 2018, Thessaloniki, Greece. ⟨10.1007/978-3-319-89884-1_19⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01926485/file/gueneau-chargeraud-pottier-esop2018.pdf BibTex
titre
Frightening Small Children and Disconcerting Grown-ups
auteur
Jade Alglave, Luc Maranget, Paul Mckenney, Andrea Parri, Alan Stern
article
ASPLOS2018 - 23rd ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Mar 2018, Williamsburg, VA, United States. ⟨10.1145/3173162.3177156⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01873636/file/asplos2018.pdf BibTex
titre
Finding Missed Compiler Optimizations by Differential Testing
auteur
Gergö Barany
article
CC'18 - 27th International Conference on Compiler Construction, Feb 2018, Vienna, Austria. ⟨10.1145/3178372.3179521⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01682683/file/cc2018.pdf BibTex
titre
Poster: Performance challenges in modular parallel programs
auteur
Vitalii Aksenov, Umut Acar, Arthur Charguéraud, Mike Rainey
article
PPoPP 2018 - 23rd ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming, Feb 2018, Vienna, Austria. ⟨10.1145/3178487.3178516⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01887717/file/main.pdf BibTex
titre
CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler
auteur
Daniel Kästner, Jörg Barrho, Ulrich Wünsche, Marc Schlickling, Bernhard Schommer, Michael Schmidt, Christian Ferdinand, Xavier Leroy, Sandrine Blazy
article
ERTS2 2018 - 9th European Congress Embedded Real-Time Software and Systems, 3AF, SEE, SIE, Jan 2018, Toulouse, France. pp.1-9
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01643290/file/ERTS_2018_paper_59.pdf BibTex
titre
Génération aléatoire de programmes guidée par la vivacité
auteur
Gergö Barany, Gabriel Scherer
article
JFLA 2018 - Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-Mer, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01682691/file/jfla2018.pdf BibTex

Autre publication

titre
À la recherche du logiciel parfait
auteur
Xavier Leroy
article
2018
Accès au bibtex
BibTex

Document associé à des manifestations scientifiques

titre
Procrastination: A proof engineering technique
auteur
Armaël Guéneau
article
Coq Workshop 2018, Jul 2018, Oxford, United Kingdom
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01962659/file/procrastination.pdf BibTex

Rapport

titre
The CompCert C verified compiler: Documentation and user’s manual
auteur
Xavier Leroy
article
[Intern report] Inria. 2018, pp.1-77
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01091802/file/manual.pdf BibTex
titre
The OCaml system release 4.07: Documentation and user's manual
auteur
Xavier Leroy, Damien Doligez, Alain Frisch, Jacques Garrigue, Didier Rémy, Jérôme Vouillon
article
[Intern report] Inria. 2018, pp.1-752
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00930213/file/ocaml-4.07-refman.pdf BibTex
titre
Compiling Programs and Proofs: FoCaLiZe Internals
auteur
François Pessaux, Damien Doligez
article
[Research Report] Ensta ParisTech. 2018
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01801276/file/compil-fcl.pdf BibTex

Thèse

titre
Synchronization Costs in Parallel Programs and Concurrent Data Structures
auteur
Vitalii Aksenov
article
Distributed, Parallel, and Cluster Computing [cs.DC]. ITMO University; Paris Diderot University, 2018. English
Accès au texte intégral et bibtex
https://hal.inria.fr/tel-01887505/file/main.pdf BibTex

2017

Article dans une revue

titre
A Simple, Possibly Correct LR Parser for C11
auteur
Jacques-Henri Jourdan, François Pottier
article
ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2017, 39 (4), pp.1 - 36. ⟨10.1145/3064848⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01633123/file/jourdan2017simple.pdf BibTex
titre
Visitors unchained
auteur
François Pottier
article
Proceedings of the ACM on Programming Languages, ACM, 2017, 1 (ICFP), pp.1 - 28. ⟨10.1145/3110272⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01670735/file/fpottier-visitors-unchained.pdf BibTex

Communication dans un congrès

titre
Liveness-Driven Random Program Generation
auteur
Gergö Barany
article
Logic-Based Program Synthesis and Transformation. LOPSTR 2017, Oct 2017, Namur, Belgium
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01860621/file/lopstr2017.pdf BibTex
titre
Certified Gathering of Oblivious Mobile Robots: survey of recent results and open problems
auteur
Thibaut Balabonski, Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain
article
Formal Methods for Industrial Critical Systems and Automated Verification of Critical Systems (FMICS/AVOCS), Sep 2017, Turin, Italy. pp.165-181, ⟨10.1007/978-3-319-67113-0_11⟩
Accès au bibtex
BibTex
titre
Tezos: the OCaml Crypto-Ledger
auteur
Benjamin Canou, Grégoire Henry, Pierre Chambart, Fabrice Le Fessant, Cagdas Bozman, Vincent Bernardoff, Guillem Rieu, Mohamed Iguernelala, Alain Mebsout, Arthur Breitman
article
OCaml 2017 - OCaml Users and Developers Workshop, Sep 2017, Oxford, United Kingdom. pp.1-2
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01661696/file/main.pdf BibTex
titre
Ornaments: exploiting parametricity for safer, more automated code refactorization and code reuse (invited talk)
auteur
Didier Rémy
article
the 10th ACM SIGPLAN Symposium on Haskell, Sep 2017, Oxford, France. pp.1-1
Accès au bibtex
BibTex
titre
A Concurrency-Optimal Binary Search Tree
auteur
Vitalii Aksenov, Vincent Gramoli, Petr Kuznetsov, Anna Malova, Srivatsan Ravi
article
23rd International European Conference on Parallel and Distributed Computing - Euro-Par 2017, Aug 2017, Santiago de Compostella, Spain
Accès au bibtex
https://arxiv.org/pdf/1702.04441 BibTex
titre
Brief Announcement: Parallel Dynamic Tree Contraction via Self-Adjusting Computation
auteur
Umut Acar, Vitalii Aksenov, Sam Westrick
article
The 29th Annual ACM Symposium on Parallelism in Algorithms and Architectures (SPAA '17), Jul 2017, Washington, United States. ⟨10.1145/3087556.3087595⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01664903/file/main.pdf BibTex
titre
Hybrid Information Flow Analysis for Real-World C Code
auteur
Gergö Barany, Julien Signoles
article
TAP 2017 - 11th International Conference on Tests & Proofs, Jul 2017, Marburg, Germany. pp.23-40, ⟨10.1007/978-3-319-61467-0_2⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01658653/file/hybrid_information_flow.pdf BibTex
titre
A Formally Verified Compiler for Lustre
auteur
Timothy Bourke, Lélio Brun, Pierre-Evariste Dagand, Xavier Leroy, Marc Pouzet, Lionel Rieg
article
PLDI 2017 - 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, ACM, Jun 2017, Barcelone, Spain
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01512286/file/velus-pldi17.pdf BibTex
titre
Challenges in Validating FLOSS Conguration
auteur
Markus Raab, Gergö Barany
article
13th IFIP International Conference on Open Source Systems (OSS), May 2017, Buenos Aires, Argentina. pp.101-114, ⟨10.1007/978-3-319-57735-7_11⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01658595/file/oss.pdf BibTex
titre
Adoption of Academic Tools in Open Source Communities: The Debian Case Study
auteur
Pietro Abate, Roberto Cosmo
article
13th IFIP International Conference on Open Source Systems (OSS), May 2017, Buenos Aires, Argentina. pp.139-150, ⟨10.1007/978-3-319-57735-7_14⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01776283/file/432701_1_En_14_Chapter.pdf BibTex
titre
Introducing Context Awareness in Unmodified, Context-unaware Software
auteur
Markus Raab, Gergö Barany
article
ENASE 2017 - 12th International Conference on Evaluation of Novel Approaches to Software Engineering, Apr 2017, Porto, Portugal. pp.1-8
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01658620/file/enase_submission.pdf BibTex
titre
Contention in Structured Concurrency: Provably Efficient Dynamic Non-Zero Indicators for Nested Parallelism
auteur
Umut Acar, Naama Ben-David, Mike Rainey
article
22nd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, Feb 2017, Austin, United States. ⟨10.1145/3018743.3018762⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01416531/file/dynsnzi.pdf BibTex
titre
Mixed-size Concurrency: ARM, POWER, C/C++11, and SC
auteur
Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn Gray, Ali Sezgin, Mark Batty, Peter Sewell
article
44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017), ACM, Jan 2017, Paris, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01413221/file/mixed-size.pdf BibTex
titre
Verifying a Hash Table and Its Iterators in Higher-Order Separation Logic
auteur
François Pottier
article
Certified Programs and Proofs, Jan 2017, Paris, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01417102/file/fpottier-hashtable.pdf BibTex

Autre publication

titre
The Coq Proof Assistant, version 8.7.1
auteur
The Coq Development Team
article
2017, pp.1-571. ⟨10.5281/zenodo.1133970⟩
Accès au bibtex
BibTex
titre
VOCAL – A Verified OCAml Library
auteur
Arthur Charguéraud, Jean-Christophe Filliâtre, Mário Pereira, François Pottier
article
2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01561094/file/main.pdf BibTex
titre
How I found a crash bug with hyperthreading in Intel's Skylake processors
auteur
Xavier Leroy
article
2017
Accès au bibtex
BibTex
titre
A formal kernel memory-ordering model (Part 1 and 2)
auteur
Jade Alglave, Luc Maranget, Paul Mckenney, Alan Stern, Andrea Parri
article
2017
Accès au bibtex
BibTex

Poster

titre
Efficient Representations for Large Dynamic Sequences in ML
auteur
Arthur Charguéraud, Mike Rainey
article
ML Family Workshop, Sep 2017, Oxford, United Kingdom. 2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01669407/file/chunkseq_ml.pdf BibTex

Rapport

titre
A Principled Approach to Ornamentation in ML
auteur
Thomas Williams, Didier Rémy
article
[Research Report] RR-9117, Inria. 2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01628060/file/ornaments-long.pdf BibTex

Pré-publication, Document de travail

titre
Introducing Context Awareness in Unmodified, Context-unaware Software
auteur
Markus Raab, Gergö Barany
article
2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01658638/file/document.pdf BibTex
titre
Liveness-Driven Random Program Generation
auteur
Gergö Barany
article
2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01658563/file/lopstr2017.pdf BibTex
titre
Generic Programming in OCAML
auteur
Florent Balestrieri, Michel Mauny
article
2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01664286/file/generic.submitted.pdf BibTex

2016

Article dans une revue

titre
The Design and Formalization of Mezzo, a Permission-Based Programming Language
auteur
Thibaut Balabonski, François Pottier, Jonathan Protzenko
article
ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2016, 38 (4), pp.94. ⟨10.1145/2837022⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01246534/file/bpp-mezzo-journal.pdf BibTex
titre
Testing Noninterference, Quickly
auteur
Cătălin Hriţcu, Leonidas Lampropoulos, Antal Spector-Zabusky, Arthur Azevedo Amorim, Maxime Dénès, John Hughes, Benjamin C. Pierce, Dimitrios Vytiniotis
article
Journal of Functional Programming (JFP); Special issue for ICFP 2013, 2016, 26, e4 (62 p.). ⟨10.1017/S0956796816000058⟩
Accès au bibtex
https://arxiv.org/pdf/1409.0393 BibTex
titre
Phase I/II dose-finding design for molecularly targeted agent: Plateau determination using adaptive randomization
auteur
Marie-Karelle Riviere, Ying Yuan, Jacques-Henri Jourdan, Frédéric Dubois, Sarah Zohar
article
Statistical Methods in Medical Research, SAGE Publications, 2016, ⟨10.1177/0962280216631763⟩
Accès au texte intégral et bibtex
https://hal.sorbonne-universite.fr/hal-01298681/file/Riviere_2016_Phase_I-II.pdf BibTex
titre
dfcomb: An R-package for phase I/II trials of drug combinations
auteur
Marie-Karelle Riviere, Jacques-Henri Jourdan, Sarah Zohar
article
Computer Methods and Programs in Biomedicine, Elsevier, 2016, 125, pp.117-133. ⟨10.1016/j.cmpb.2015.10.018⟩
Accès au texte intégral et bibtex
https://hal.sorbonne-universite.fr/hal-01297367/file/packages_CMPB.pdf BibTex

Communication dans un congrès

titre
Transfinite Step-Indexing: Decoupling Concrete and Logical Steps
auteur
Kasper Svendsen, Filip Sieczkowski, Lars Birkedal
article
25th European Symposium on Programming Languages and Systems, Dec 2016, Eindhoven, Netherlands. pp.727 - 751, ⟨10.1007/978-3-662-49498-1_28⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01408649/file/biglater-conf%20%281%29.pdf BibTex
titre
A Certified Universal Gathering Algorithm for Oblivious Mobile Robots
auteur
Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain
article
Distributed Computing (DISC), Sep 2016, Paris, France
Accès au bibtex
BibTex
titre
ocp-lint, A Plugin-based Style-Checker with Semantic Patches
auteur
Çagdas Bozman, Théophane Huffschmitt, Michael Laporte, Fabrice Le Fessant
article
OCaml Users and Developers Workshop 2016, Sep 2016, Nara, Japan
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01352013/file/ocaml-2016-typerex-lint.pdf BibTex
titre
Learn OCaml, An Online Learning Center for OCaml
auteur
Benjamin Canou, Grégoire Henry, Çagdas Bozman, Fabrice Le Fessant
article
OCaml Users and Developers Workshop 2016, Sep 2016, Nara, Japan
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01352015/file/ocaml-2016-learn-ocaml.pdf BibTex
titre
Statistically profiling memory in OCaml
auteur
Jacques-Henri Jourdan
article
OCaml 2016, Sep 2016, Nara, Japan
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01406809/file/jourdan2016statistically.pdf BibTex
titre
Ambiguous pattern variables
auteur
Gabriel Scherer, Luc Maranget, Thomas Réfis
article
OCaml 2016: The OCaml Users and Developers Workshop, Sep 2016, Nara, Japan. pp.2
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01413241/file/ml-workshop-abstract.pdf BibTex
titre
Generic Programming in OCaml
auteur
Florent Balestrieri, Michel Mauny
article
OCaml 2016 - The OCaml Users and Developers Workshop, Sep 2016, Nara, Japan
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01413061/file/OUD_2016_paper_2.pdf BibTex
titre
Hierarchical Memory Management for Parallel Programs
auteur
Ram Raghunathan, Stefan Muller, Umut Acar, Guy Blelloch
article
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, Sep 2016, Nara, Japan. ⟨10.1145/3022670.2951935⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01416237/file/icfp2016-steel.pdf BibTex
titre
Sparsity Preserving Algorithms for Octagons
auteur
Jacques-Henri Jourdan
article
NSAD 2016 - Numerical and symbolic abstract domains workshop , Sep 2016, Edinburgh, United Kingdom. pp.14
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01406795/file/jourdan2016sparsity.pdf BibTex
titre
Brief announcement: Certified Universal Gathering in R2 for Oblivious Mobile Robots
auteur
Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain
article
ACM Conference on Principles of Distributed Computing (PODC), ACM, Jul 2016, Chicago, United States
Accès au bibtex
BibTex
titre
A Type Inference System Based on Saturation of Subtyping Constraints
auteur
Benoît Vaugon, Michel Mauny
article
Trends in Functional Programming, Jun 2016, College Park (MD), United States
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01413043/file/article.pdf BibTex
titre
Reachability and Error Diagnosis in LR(1) Parsers
auteur
François Pottier
article
CC 2016 - 25th International Conference on Compiler Construction, Mar 2016, Barcelone, Spain. pp.11, ⟨10.1145/2892208.2892224⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01417004/file/fpottier-reachability-cc2016.pdf BibTex
titre
CompCert - A Formally Verified Optimizing Compiler
auteur
Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, Christian Ferdinand
article
ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, SEE, Jan 2016, Toulouse, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01238879/file/erts2016_compcert.pdf BibTex
titre
Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA
auteur
Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, Peter Sewell
article
Principles of Programming Languages 2016 (POPL 2016), Jan 2016, Saint Petersburg, United States
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01244776/file/top.pdf BibTex
titre
Reachability and error diagnosis in LR(1) automata
auteur
François Pottier
article
Journées Francophones des Langages Applicatifs, Jan 2016, Saint-Malo, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01248101/file/fpottier-reachability-jfla2016.pdf BibTex

Thèse

titre
Verasco: a Formally Verified C Static Analyzer
auteur
Jacques-Henri Jourdan
article
Programming Languages [cs.PL]. Universite Paris Diderot-Paris VII, 2016. English
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/tel-01327023/file/thesis.pdf BibTex

2015

Communication dans un congrès

titre
Global Semantic Analysis on OCaml programs
auteur
Thomas Blanc, Pierre Chambart, Michel Mauny, Fabrice Le Fessant
article
OCaml 2015 - The OCaml Users and Developers Workshop, Sep 2015, Vancouver, Canada
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01413319/file/OCaml_2015_submission_3.pdf BibTex
titre
Micro-Policies: Formally Verified, Tag-Based Security Monitors
auteur
Arthur Azevedo de Amorim, Maxime Dénès, Nick Giannarakis, Cătălin Hriţcu, Benjamin Pierce, Antal Spector-Zabusky, Andrew Tolmach
article
2015 IEEE Symposium on Security and Privacy, May 2015, San Jose, United States. pp.813 - 830, ⟨10.1109/SP.2015.55⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01265666/file/micro-policies.pdf BibTex

Autre publication

titre
Towards a Formalization of the HSA Memory Model in the cat Language
auteur
Luc Maranget, Jade Alglave
article
2015, pp.57
Accès au bibtex
BibTex

2014

Communication dans un congrès

titre
Nullable Type Inference
auteur
Michel Mauny, Benoît Vaugon
article
OCaml 2014 - The OCaml Users and Developers Workshop, Sep 2014, Gothenbourg, Sweden
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01413294/file/ocaml2014_14.pdf BibTex
titre
Finding Non-Polynomial Positive Invariants and Lyapunov Functions for Polynomial Systems through Darboux Polynomials
auteur
Eric Goubault, Jacques-Henri Jourdan, Sylvie Putot, Sriram Sankaranarayanan
article
American Control Conference (ACC), Jun 2014, Portland, United States
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01633155/file/goubault2014finding.pdf BibTex

Suivez Inria