publis.bib

@inproceedings{conchon:hal-01960203,
  title = {{Alt-Ergo 2.2}},
  author = {Conchon, Sylvain and Coquereau, Albin and  Iguernlala, Mohamed and Mebsout, Alain},
  url = {https://hal.inria.fr/hal-01960203},
  booktitle = {{SMT Workshop: International Workshop on Satisfiability Modulo Theories}},
  address = {Oxford, United Kingdom},
  year = {2018},
  month = jul,
  pdf = {https://hal.inria.fr/hal-01960203/file/Alt-Ergo-2.2--SMT-Workshop-2018.pdf},
  hal_id = {hal-01960203},
  hal_version = {v1}
}
@inproceedings{pereira16jfla,
  topics = {team},
  author = {Jean-Christophe Filli\^atre and M\'ario Pereira},
  title = {It\'erer avec confiance},
  crossref = {jfla16},
  hal = {https://hal.inria.fr/hal-01240891}
}
@inproceedings{pereira16nfm,
  topics = {team},
  author = {Jean-Christophe Filli\^atre and M\'ario Pereira},
  title = {A Modular Way to Reason About Iteration},
  crossref = {nfm16},
  abstract = { In this paper we present an approach to specify
                  programs performing iterations. The idea is to
                  specify iteration in terms of the nite sequence of
                  the elements enumerated so far, and only those. In
                  particular, we are able to deal with
                  non-deterministic and possibly innite iteration. We
                  show how to cope with the issue of an iteration no
                  longer being consistent with mutable data. We
                  validate our proposal using the deductive verication
                  tool Why3 and two iteration paradigms, namely
                  cursors and higher-order iterators. For each
                  paradigm, we verify several implementations of
                  iterators and client code. This is done in a modular
                  way, i.e., the client code only relies on the
                  specication of the iteration. },
  hal = {https://hal.inria.fr/hal-01281759}
}
@inproceedings{filliatre16,
  topics = {team},
  author = {Jean-Christophe Filli\^atre and M\'ario Pereira},
  title = {Producing All Ideals of a Forest, Formally (Verification Pearl)},
  crossref = {vstte16},
  hal = {https://hal.inria.fr/hal-01316859}
}
@inproceedings{clochard16,
  topics = {team},
  author = {Martin Clochard and L\'eon Gondelman and M\'ario Pereira},
  title = {The Matrix Reproved},
  crossref = {vstte16},
  hal = {https://hal.inria.fr/hal-01316902}
}
@proceedings{jfla16,
  title = {Journ\'ees Francophones des Langages Applicatifs},
  year = 2016,
  booktitle = {Vingt-septi\`emes Journ\'ees Francophones des Langages Applicatifs},
  month = jan,
  address = {Saint-Malo, France},
  x-international-audience = {no},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA}
}
@proceedings{vstte16,
  title = {VSTTE 2016},
  booktitle = {8th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE)},
  month = jul,
  year = 2016,
  address = {Toronto, Canada},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {VSTTE},
  editor = {Sandrine Blazy and Marsha Chechik},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer}
}
@proceedings{nfm16,
  booktitle = {8th NASA Formal Methods Symposium},
  address = {Minneapolis, MN, USA},
  audience = {internationale},
  year = 2016,
  month = jun,
  series = {Lecture Notes in Computer Science},
  volume = {9690},
  publisher = {Springer}
}
@inproceedings{chargueraud-pottier-15,
  author = {Arthur Chargu\'eraud and Fran\c{c}ois Pottier},
  title = {Machine-Checked Verification of the Correctness and
                 Amortized Complexity of an Efficient Union-Find
                 Implementation},
  booktitle = {Proceedings of the 6th Conference on Interactive
                 Theorem Proving (ITP 2015)},
  month = aug,
  year = {2015},
  volume = {9236},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  pages = {137--153},
  url = {http://gallium.inria.fr/~fpottier/publis/chargueraud-pottier-uf.pdf}
}
@inproceedings{chargueraud-horepr-16,
  author = {Chargu\'{e}raud, Arthur},
  title = {Higher-Order Representation Predicates in Separation Logic},
  year = {2016},
  isbn = {9781450341271},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  url = {https://doi.org/10.1145/2854065.2854068},
  doi = {10.1145/2854065.2854068},
  booktitle = {Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs},
  pages = {3–14},
  numpages = {12},
  keywords = {Representation Predicates, Separation Logic},
  location = {St. Petersburg, FL, USA},
  series = {CPP 2016}
}
@inproceedings{chargueraud-pottier-slro-16,
  author = {Arthur Chargu\'eraud and Fran\c{c}ois Pottier},
  title = {Temporary Read-Only Permissions for Separation Logic},
  booktitle = {Proceedings of the European Symposium on Programming
                 (ESOP 2017)},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  editor = {Hongseok Yang},
  month = apr,
  year = {2017},
  url = {http://gallium.inria.fr/~fpottier/publis/chargueraud-pottier-slro.pdf}
}
@inproceedings{pottier-cpp-17,
  author = {Fran\c{c}ois Pottier},
  title = {Verifying a hash table and its iterators in
                 higher-order separation logic},
  booktitle = {Proceedings of the 6th ACM SIGPLAN Conference on
                 Certified Programs and Proofs (CPP 2017)},
  month = jan,
  year = {2017},
  pages = {3--16},
  url = {http://gallium.inria.fr/~fpottier/publis/fpottier-hashtable.pdf}
}
@article{chargueraud-pottier-uf-sltc-17,
  author = {Arthur Chargu\'eraud and Fran\c{c}ois Pottier},
  title = {Verifying the Correctness and Amortized Complexity of
                 a Union-Find Implementation in Separation Logic with
                 Time Credits},
  journal = {Journal of Automated Reasoning},
  month = sep,
  year = 2017,
  url = {http://gallium.inria.fr/~fpottier/publis/chargueraud-pottier-uf-sltc.pdf},
  hal = {https://hal.inria.fr/hal-01652785}
}
@misc{cfpp17,
  topics = {team},
  author = {Arthur Chargu\'eraud and Jean-Christophe Filli{\^a}tre and
                  M{\'a}rio Pereira and Fran\c{c}ois Pottier},
  title = {{VOCAL} -- {A} {V}erified {OC}aml {L}ibrary},
  howpublished = {ML Family Workshop},
  month = {September},
  year = {2017},
  hal = {https://hal.inria.fr/hal-01561094}
}
@inproceedings{pereira17jfla,
  topics = {team},
  title = {{D{\'e}fonctionnaliser pour prouver}},
  author = {Pereira, M{\'a}rio},
  hal = {https://hal.inria.fr/hal-01378068},
  crossref = {jfla17}
}
@proceedings{jfla17,
  topics = {team},
  hal = {https://hal.inria.fr/hal-01662072},
  title = {Journ\'ees Francophones des Langages Applicatifs},
  editor = {Boldo, Sylvie and Signoles, Julien},
  year = 2017,
  booktitle = {Vingt-huiti\`emes Journ\'ees Francophones des Langages Applicatifs},
  month = jan,
  address = {Gourette, France},
  x-international-audience = {no},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA}
}
@unpublished{boulme:hal-01558252,
  title = {{Toward Certification for Free!}},
  author = {Boulm{\'e}, Sylvain and Mar{\'e}chal, Alexandre},
  url = {https://hal.archives-ouvertes.fr/hal-01558252},
  note = {working paper or preprint},
  year = {2017},
  month = jul,
  keywords = { Linear Programming ; Coq ; Type theory ; Abstract Domain of Polyhedra ; Polymorphism ; Program verification ;  Parametricity ; CCS Concepts: $\bullet$Software and its engineering $\rightarrow$ Polymorphism ; $\bullet$Theory of computation $\rightarrow$ Program veriication ; Invariants ; $\bullet$Mathematics of computing $\rightarrow$ Solvers ; Additional Key Words and Phrases: Abstract Domain of Polyhedra ;  CCC},
  pdf = {https://hal.archives-ouvertes.fr/hal-01558252/file/PFS.pdf},
  hal_id = {hal-01558252},
  hal_version = {v2}
}
@inproceedings{boulme:synasc18,
  title = {{The Verified Polyhedron Library: an overview}},
  author = {Boulm{\'e}, Sylvain and Mar{\'e}chal, Alexandre and
Monniaux, David and P{\'e}rin, Micha{\"e}l and Yu, Hang},
  url = {https://hal.archives-ouvertes.fr/hal-02100006},
  booktitle = {{20th International Symposium on Symbolic and Numeric
Algorithms for Scientific Computing (SYNASC)}},
  address = {Timișoara, Romania},
  organization = {{Universitatea de Vest din Timișoara}},
  editor = {Erika {\'A}brah{\'a}m and Viorel Negru and Dana Petcu and
Daniela Zaharie and Tetsuo Ida and Tudor Jebelean and Stephen Watt},
  publisher = {{IEEE Computer Society}},
  series = {20th International Symposium on Symbolic and Numeric
Algorithms for Scientific Computing},
  pages = {9-17},
  year = {2018},
  month = sep,
  hal_id = {hal-02100006},
  hal_version = {v1}
}
@article{boulme:jar18,
  title = {{Refinement to Certify Abstract Interpretations, Illustrated
on Linearization for Polyhedra}},
  author = {Boulm{\'e}, Sylvain and Mar{\'e}chal, Alexandre},
  url = {https://hal.archives-ouvertes.fr/hal-01133865},
  journal = {{Journal of Automated Reasoning}},
  publisher = {{Springer Verlag}},
  year = {2018},
  month = nov,
  doi = {10.1007/s10817-018-9492-2},
  keywords = {Continuation-Passing Style ; Linear arithmetic ;
Refinement calculus ; Abstract Interpretation ; The Coq proof assistant
; Monad ; Weakest precondition ; Certified Software ; Proof Assistants ;
Result Certification}
}
@article{six:oopsla20,
  title = {{Certified and efficient instruction scheduling. Application
to interlocked VLIW processors.}},
  author = {Six, Cyril and Boulm{\'e}, Sylvain and Monniaux, David},
  url = {https://hal.archives-ouvertes.fr/hal-02185883},
  journal = {{Proceedings of the ACM on Programming Languages}},
  publisher = {{ACM}},
  series = {OOPSLA 2020},
  pages = {129},
  year = {2020},
  month = nov,
  doi = {10.1145/3428197}
}
@inproceedings{chargueraud-ml-17,
  author = {Arthur Chargu\'eraud and Mike Rainey},
  title = {Efficient Representations for Large Dynamic Sequences in {ML}},
  booktitle = {ML Family Workshop},
  year = 2017,
  hal = {https://hal.inria.fr/hal-01669407}
}
@inproceedings{gueneau-chargueraud-pottier-esop-2018,
  author = {Arma\"el Gu\'eneau and Arthur Chargu\'eraud and Fran\c{c}ois
                 Pottier},
  title = {A Fistful of Dollars: Formalizing Asymptotic
                 Complexity Claims via Deductive Program Verification},
  booktitle = {Proceedings of the European Symposium on Programming
                 (ESOP 2018)},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  editor = {Amal Ahmed},
  month = apr,
  year = {2018},
  volume = {10801},
  pages = {533--560},
  url = {http://gallium.inria.fr/~agueneau/publis/gueneau-chargueraud-pottier-coq-bigO.pdf}
}
@article{clochard17jar,
  topics = {team},
  title = {The {Matrix} Reproved},
  author = {Clochard, Martin and Gondelman, L{\'e}on and Pereira, M{\'a}rio},
  hal = {https://hal.inria.fr/hal-01617437},
  journal = jar,
  pages = {365--383},
  volume = 60,
  number = 3,
  publisher = sv,
  year = 2018,
  doi = {10.1007/s10817-017-9436-2}
}
@inproceedings{fpds18jfla,
  topics = {team},
  crossref = {jfla18},
  title = {V{\'e}rification de programmes fortement imp{\'e}ratifs avec {W}hy3},
  author = {Jean-Christophe Filli{\^a}tre and M{\'a}rio Pereira and
  Sim{\~a}o Melo de Sousa},
  hal = {https://hal.inria.fr/hal-01649989},
  pdf = {https://hal.inria.fr/hal-01649989/file/main.pdf},
  hal_id = {hal-01649989},
  hal_version = {v2}
}
@proceedings{jfla18,
  topics = {team},
  title = {Vingt-neuvi\`emes Journ\'ees Francophones des Langages Applicatifs},
  booktitle = {Vingt-neuvi\`emes Journ{\'e}es Francophones des Langages Applicatifs},
  address = {Banyuls-sur-mer, France},
  year = 2018,
  month = jan,
  editor = {Boldo, Sylvie and Magaud, Nicolas},
  hal = {https://hal.inria.fr/hal-01707376}
}
@techreport{fgpps18,
  author = {Jean-Christophe Filli{\^a}tre and L{\'e}on Gondelman and
            Andrei Paskevich and M{\'a}rio Pereira and Sim{\~a}o Melo de Sousa},
  title = {A Toolchain to {P}roduce {C}orrect-by-{C}onstruction {OC}aml
           {P}rograms},
  hal = {https://hal.inria.fr/hal-01783851},
  pdf = {https://hal.inria.fr/hal-01783851/file/main.pdf},
  note = {\url{https://hal.inria.fr/hal-01783851}}
}
@article{krebbers-al-mosel-18,
  author = {Krebbers, Robbert and Jourdan, Jacques-Henri and Jung, Ralf and Tassarotti, Joseph and Kaiser, Jan-Oliver and Timany, Amin and Chargu\'{e}raud, Arthur and Dreyer, Derek},
  title = {MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic},
  year = {2018},
  issue_date = {September 2018},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {2},
  number = {ICFP},
  url = {https://doi.org/10.1145/3236772},
  doi = {10.1145/3236772},
  journal = {Proc. ACM Program. Lang.},
  month = jul,
  articleno = {77},
  numpages = {30},
  keywords = {modal logic, Coq proof assistant, logic of bunched implications, Separation logic, interactive theorem proving}
}
@inproceedings{gospelfm19,
  topics = {team},
  crossref = {fm19},
  author = {Arthur Chargu\'eraud and Jean-Christophe Filli\^atre and Cl\'audio Louren\c{c}o and M\'ario Pereira},
  title = {{GOSPEL} --- Providing {OCaml} with a Formal Specification Language},
  hal = {https://hal.inria.fr/hal-02157484}
}
@proceedings{fm19,
  title = {FM 2019 23rd International Symposium on Formal Methods},
  year = 2019,
  editor = {Annabelle McIver and Maurice ter Beek},
  month = {October}
}
@misc{vocal,
  author = {The VOCaL project},
  title = {The {VOCaL} Library},
  howpublished = {Open Source Software, with MIT license},
  year = 2018,
  note = {\url{https://github.com/vocal-project/vocal}}
}
@misc{tis-report-1,
  author = {TrustInSoft},
  title = {Report on the deployment of the {VOCaL} library in {TrustInSoft} Kernel},
  year = 2019,
  month = {May}
}
@inproceedings{mevel-jourdan-pottier-19,
  author = {Glen Mével and Jacques-Henri Jourdan and François
                 Pottier},
  title = {Time credits and time receipts in {Iris}},
  booktitle = {European Symposium on Programming (ESOP)},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {11423},
  month = apr,
  year = {2019},
  pages = {1--27},
  url = {http://gallium.inria.fr/~fpottier/publis/mevel-jourdan-pottier-time-in-iris-2019.pdf}
}
@article{de-vilhena-pottier-jourdan-19,
  author = {Paulo Em{\'\i}lio de Vilhena and Fran\c{c}ois Pottier and
                 Jacques-Henri Jourdan},
  title = {Spy Game: Verifying a Local Generic Solver in {Iris}},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {4},
  number = {POPL},
  month = jan,
  year = {2020},
  url = {http://gallium.inria.fr/~fpottier/publis/de-vilhena-pottier-jourdan-spy-game-2020.pdf},
  abstract = {We verify the partial correctness of a ``local generic
                 solver'', that is, an on-demand, incremental, memoizing
                 least fixed point computation algorithm. The
                 verification is carried out in Iris, a modern breed of
                 concurrent separation logic. The specification is
                 simple: the solver computes the optimal least fixed
                 point of a system of monotone equations. Although the
                 solver relies on mutable internal state for memoization
                 and for ``spying'', a form of dynamic dependency
                 discovery, it is apparently pure: no side effects are
                 mentioned in its specification. As auxiliary
                 contributions, we provide several illustrations of the
                 use of prophecy variables, a novel feature of Iris; we
                 establish a restricted form of the infinitary
                 conjunction rule; and we provide a specification and
                 proof of Longley's $\mathit{modulus}$ function, an
                 archetypical example of spying.}
}
@inproceedings{gueneau-al-cycles-19,
  author = {Arma{\"e}l Gu{\'e}neau and Jacques-Henri Jourdan and Arthur Chargu{\'e}raud and Fran{\c{c}}ois Pottier},
  title = {{Formal Proof and Analysis of an Incremental Cycle Detection Algorithm}},
  booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages = {18:1--18:20},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  isbn = {978-3-95977-122-1},
  issn = {1868-8969},
  year = {2019},
  volume = {141},
  editor = {John Harrison and John O'Leary and Andrew Tolmach},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address = {Dagstuhl, Germany},
  url = {http://drops.dagstuhl.de/opus/volltexte/2019/11073},
  urn = {urn:nbn:de:0030-drops-110739},
  doi = {10.4230/LIPIcs.ITP.2019.18},
  annote = {Keywords: interactive deductive program verification, complexity analysis}
}
@inproceedings{types18-indrec,
  pdf = {http://www-verimag.imag.fr/~monin/Publis/Docs/types2018-indrec.pdf},
  author = {Dominique Larchey-Wendling and Jean{-}Fran{\c{c}}ois Monin},
  title = {Simulating induction-recursion for partial algorithms},
  booktitle = {TYPES 2018 Abstracts},
  year = 2018,
  editor = {Jos\`{e} Esp\`{i}rito Santo and Lu\`{i}s Pinto},
  month = {June},
  address = {Braga},
  abstract = {We describe a generic method to implement and extract
                  partial recursive algorithms in Coq in a purely
                  constructive way, using
                  L. Paulson's if-then-else normalization as a running
                  example.  }
}
@inproceedings{DBLP:conf/birthday/DengM19,
  pdf = {http://www-verimag.imag.fr/~monin/Publis/Docs/fc19-probatesting_long.pdf},
  author = {Yuxin Deng and
               Jean{-}Fran{\c{c}}ois Monin},
  title = {Formalisation of Probabilistic Testing Semantics in Coq},
  booktitle = {The Art of Modelling Computational Systems: {A} Journey from Logic
               and Concurrency to Security and Privacy - Essays Dedicated to Catuscia
               Palamidessi on the Occasion of Her 60th Birthday},
  pages = {276--292},
  year = {2019},
  editor = {M{\'{a}}rio S. Alvim and
               Kostas Chatzikokolakis and
               Carlos Olarte and
               Frank Valencia},
  series = {Lecture Notes in Computer Science},
  volume = {11760},
  publisher = {Springer},
  timestamp = {Thu, 07 Nov 2019 17:02:36 +0100},
  biburl = {https://dblp.org/rec/bib/conf/birthday/DengM19},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  abstract = {Van Breugel et al. [F. van Breugel et al,
                  Theor. Comput. Sci. 333(1-2):171-197, 2005] have
                  given an elegant testing framework that can
                  characterise probabilistic bisimulation, but its
                  completeness proof is highly involved. Deng and Feng
                  [Y. Deng and Y. Feng, Inf.  Comput. 257:58-64, 2017]
                  have simplified that result for finite-state
                  processes. The crucial part in the latter work is an
                  algorithm that can construct enhanced tests. We
                  formalise the algorithm and prove its correctness by
                  maintaining a number of subtle invariants in Coq. To
                  support the formalisation, we develop a reusable
                  library for manipulating finite sets. This sets an
                  early example of formalising probabilistic
                  concurrency theory or quantitative aspects of
                  concurrency theory at large, which is a rich field
                  to be pursued }
}
@article{filliatre20jlamp,
  author = {Jean-Christophe Filli\^atre},
  title = {Simpler Proofs with Decentralized Invariants},
  journal = {Journal of Logical and Algebraic Methods in Programming},
  publisher = {Elsevier},
  year = 2021,
  topics = {team},
  month = jan,
  note = {See \url{http://why3.lri.fr/spdi/}},
  hal = {https://hal.inria.fr/hal-02518570},
  doi = {https://doi.org/10.1016/j.jlamp.2021.100645}
}
@inproceedings{paskevich20isola,
  author = {Jean-Christophe Filli\^atre and Andrei Paskevich},
  title = {Abstraction and Genericity in Why3},
  booktitle = {9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)},
  month = oct,
  year = 2020,
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = 12476,
  pages = {122--142},
  editor = {Tiziana Margaria and Bernhard Steffen},
  address = {Rhodes, Greece},
  topics = {team},
  note = {\url{http://why3.lri.fr/isola-2020/}},
  hal = {https://hal.inria.fr/hal-02696246}
}
@article{mevel-jourdan-pottier-20,
  author = {Glen Mével and Jacques-Henri Jourdan and François
                 Pottier},
  title = {Cosmo: A Concurrent Separation Logic for {Multicore
                 OCaml}},
  month = jun,
  year = {2020},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {4},
  number = {ICFP},
  url = {http://cambium.inria.fr/~fpottier/publis/mevel-jourdan-pottier-cosmo-2020.pdf}
}
@article{chargueraud-sep-20,
  author = {Chargu\'{e}raud, Arthur},
  title = {Separation Logic for Sequential Programs (Functional Pearl)},
  year = {2020},
  issue_date = {August 2020},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {4},
  number = {ICFP},
  url = {https://doi.org/10.1145/3408998},
  doi = {10.1145/3408998},
  journal = {Proc. ACM Program. Lang.},
  month = aug,
  articleno = {116},
  numpages = {34},
  keywords = {Separation Logic, Coq, Program verification}
}
@article{de-vilhena-pottier-21,
  author = {Paulo Emílio de Vilhena and François Pottier},
  title = {A Separation Logic for Effect Handlers},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {5},
  number = {POPL},
  month = jan,
  year = {2021},
  url = {http://cambium.inria.fr/~fpottier/publis/de-vilhena-pottier-sleh.pdf}
}
@inproceedings{pottier-monolith-21,
  author = {François Pottier},
  title = {Strong Automated Testing of {OCaml} Libraries},
  booktitle = {Journées Francophones des Langages Applicatifs
                 (JFLA)},
  month = feb,
  year = {2021},
  url = {http://cambium.inria.fr/~fpottier/publis/pottier-monolith-2021.pdf}
}
@inbook{braga21,
  author = {Dominique Larchey{-}Wendling and Jean{-}Fran{\c{c}}ois Monin},
  editor = {Klaus Mainzer and Peter Schuster and Helmut Schwichtenberg},
  chapter = 8,
  title = {{The Braga Method:  Extracting Certified Algorithms from Complex Recursive Schemes in Coq}},
  booktitle = {Proof and Computation II: From Proof Theory and Univalent Mathematics to Program Extraction and Verification},
  publisher = {World Scientific},
  year = 2021,
  crossref = {proof-comput-II},
  month = {September},
  pages = {305--386}
}
@book{proof-comput-II,
  editor = {Klaus Mainzer and Peter Schuster and Helmut Schwichtenberg},
  title = {Proof and Computation II: From Proof Theory and Univalent Mathematics to Program Extraction and Verification},
  publisher = {World Scientific},
  year = 2021,
  month = {September}
}
@techreport{filliatrepascutto21,
  author = {Jean-Christophe Filli\^atre and Cl\'ement Pascutto},
  title = {{Ortac}: Runtime Assertion Checking for {OCaml}},
  year = 2021,
  topics = {team},
  institution = {Universit{\'e} Paris-Saclay},
  month = may,
  hal = {https://hal.inria.fr/hal-03252901},
  abstract = {Runtime assertion checking (RAC) is a convenient set of
    techniques that lets developers abstract away the
    process of verifying the correctness of their
    programs by writing formal specifications and
    automating their verification at runtime.  In this
    work, we present ortac, a runtime assertion checking
    tool for OCaml libraries and programs. OCaml is a
    functional programming lan- guage in which idioms
    rely on an expressive type system, modules, and
    interface abstractions. ortac consumes interfaces
    annotated with type invariants and function
    contracts and produces code wrappers with the same
    signature that check these specifications at
    runtime. It provides a flexible framework for
    traditional assertion checking, monitoring mis-
    behaviors without interruptions, and automated fuzz
    testing for OCaml programs.  This paper presents an
    overview of ortac features and highlights its main
    design choices.}
}
@inproceedings{filliatre19ifm,
  author = {Jean-Christophe Filli\^atre},
  title = {Deductive Verification of {OCaml} Libraries},
  booktitle = {15th International Conference on integrated Formal Methods},
  year = 2019,
  month = dec,
  address = {Bergen, Norway},
  note = {Invited talk},
  topics = {team, lri},
  hal = {https://hal.inria.fr/hal-02406253},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL},
  x-type = {invitation},
  x-invited-conference = {yes},
  x-international-audience = {yes}
}
@inproceedings{filliatre17framacsparkday,
  author = {Jean-Christophe Filli\^atre},
  title = {The {Why3} tool for deductive verification and verified {OCaml} libraries},
  booktitle = {Frama-C \& SPARK Day 2019},
  year = 2019,
  month = jun,
  address = {Paris, France},
  note = {Invited talk},
  topics = {team, lri},
  type_publi = {colloque},
  x-equipes = {demons PROVAL},
  x-type = {invitation},
  x-invited-conference = {yes},
  x-international-audience = {yes}
}

This file was generated by bibtex2html 1.99.