Jacques-Henri Jourdan


CV: English - Francais


Email

jacques-henri.jourdan [at] cnrs [dot] fr

My PGP public key

Mail address

LMF - Laboratoire Méthodes Formelles, Bât. 650
Univerité Paris-Saclay
91405 Orsay Cedex
France

Physical address

LMF - Bât. 650, bureau 273
1, rue Raimond Castaing
91190 Gif-sur-Yvette
France

publications.bib

@inproceedings{jourdan2018rustbelt,
  author = {Jung, Ralf and Jourdan, Jacques-Henri and Krebbers, Robbert and Dreyer, Derek},
  title = {{RustBelt}: Securing the Foundations of the {Rust} Programming Language},
  booktitle = {Symposium on Principles of Programming Languages (POPL)},
  month = {January},
  year = {2018},
  organization = {ACM},
  abstract = {Rust is a new systems programming language that promises
                  to overcome the seemingly fundamental tradeoff
                  between high-level safety guarantees and low-level
                  control over resource management.  Unfortunately,
                  none of Rust's safety claims have been formally
                  proven, and there is good reason to question whether
                  they actually hold.  Specifically, Rust employs a
                  strong, ownership-based type system, but then
                  extends the expressive power of this core type
                  system through libraries that internally use unsafe
                  features.  In this paper, we give the first formal
                  (and machine-checked) safety proof for a language
                  representing a realistic subset of Rust.  Our proof
                  is extensible in the sense that, for each new Rust
                  library that uses unsafe features, we can say what
                  verification condition it must satisfy in order for
                  it to be deemed a safe extension to the language.
                  We have carried out this verification for some of
                  the most important libraries that are used
                  throughout the Rust ecosystem.},
  pdf = {pdf/jourdan2018rustbelt.pdf},
  doi = {10.1145/3158154}
}
@inproceedings{krebbers2017essence,
  author = {Krebbers, Robbert and Jung, Ralf and Bizjak, Aleš and
                  Jourdan, Jacques-Henri and Dreyer, Derek and
                  Birkedal, Lars},
  title = {The essence of higher-order concurrent separation logic},
  booktitle = {European Symposium on Programming (ESOP)},
  year = {2017},
  month = {April},
  abstract = {Concurrent separation logics (CSLs) have come of age,
                  and with age they have accumulated a great deal of
                  complexity Previous work on the Iris logic attempted
                  to reduce the complex logical mechanisms of modern
                  CSLs to two orthogonal concepts: partial commutative
                  monoids (PCMs) and invariants. However, the
                  realization of these concepts in Iris still bakes in
                  several complex mechanisms--such as weakest
                  preconditions and mask-changing view shifts--as
                  primitive notions.  In this paper, we take the Iris
                  story to its (so to speak) logical conclusion,
                  applying the reductionist methodology of Iris to
                  Iris itself. Specifically, we define a small,
                  resourceful base logic, which distills the essence
                  of Iris: it comprises only the assertion layer of
                  vanilla separation logic, plus a handful of simple
                  modalities. We then show how the much fancier
                  logical mechanisms of Iris--in particular, its
                  entire program specification layer--can be
                  understood as merely derived forms in our base
                  logic. This approach helps to explain the meaning of
                  Iris’s program specifications at a much higher level
                  of abstraction than was previously possible. We also
                  show that the step-indexed "later" modality of Iris
                  is an essential source of complexity, in that
                  removing it leads to a logical inconsistency. All
                  our results are fully formalized in the Coq proof
                  assistant.},
  pdf = {pdf/krebbers2017essence.pdf},
  publisher = {Springer},
  doi = {10.1007/978-3-662-54434-1_26}
}
@inproceedings{boldo2013formally,
  author = {Boldo, Sylvie and Jourdan, Jacques-Henri and Leroy, Xavier and Melquiond,
	Guillaume},
  title = {A Formally-Verified {C} Compiler Supporting Floating-Point Arithmetic},
  booktitle = {IEEE Symposium on Computer Arithmetic (ARITH)},
  year = {2013},
  month = {April},
  pages = {107--115},
  organization = {IEEE},
  abstract = {Floating-point arithmetic is known to be tricky:
                  roundings, formats, exceptional values. The IEEE-754
                  standard was a push towards straightening the field
                  and made formal reasoning about floating-point
                  computations easier and flourishing. Unfortunately,
                  this is not sufficient to guarantee the final result
                  of a program, as several other actors are involved:
                  programming language, compiler, architecture. The
                  Comp Certformally-verified compiler provides a
                  solution to this problem: this compiler comes with a
                  mathematical specification of the semantics of its
                  source language (a large subset of ISO C90) and
                  target platforms (ARM, PowerPC, x86-SSE2), and with
                  a proof that compilation preserves semantics. In
                  this paper, we report on our recent success in
                  formally specifying and proving correct Comp Cert's
                  compilation of floating-point arithmetic. Since
                  CompCert is verified using the Coq proof assistant,
                  this effort required a suitable Coq formalization of
                  the IEEE-754 standard, we extended the Flocq library
                  for this purpose. As a result, we obtain the first
                  formally verified compiler that provably preserves
                  the semantics of floating-point programs.},
  doi = {10.1109/ARITH.2013.30},
  pdf = {pdf/boldo2013formally.pdf}
}
@inproceedings{braibant2013implementing,
  author = {Braibant, Thomas and Jourdan, Jacques-Henri and Monniaux, David},
  title = {Implementing hash-consed structures in {C}oq},
  booktitle = {Interactive Theorem Proving (ITP)},
  year = {2013},
  month = {July},
  pages = {477--483},
  abstract = {We report on three different approaches to use
                  hash-consing in programs certified with the Coq
                  system, using binary decision diagrams (BDD) as
                  running example. The use cases include execution
                  inside Coq, or execution of the extracted OCaml
                  code. There are different trade-offs between
                  faithful use of pristine extracted code, and code
                  that is fine-tuned to make use of OCaml programming
                  constructs not available in Coq. We discuss the
                  possible consequences in terms of performances and
                  guarantees.},
  doi = {10.1007/978-3-642-39634-2_36},
  pdf = {pdf/braibant2013implementing.pdf}
}
@inproceedings{goubault2014finding,
  author = {Goubault, Eric and Jourdan, Jacques-Henri and Putot, Sylvie and Sankaranarayanan,
	Sriram},
  title = {Finding non-polynomial positive invariants and lyapunov functions
	for polynomial systems through Darboux polynomials},
  booktitle = {American Control Conference (ACC)},
  year = {2014},
  month = {June},
  pages = {3571--3578},
  publisher = {IEEE},
  abstract = {In this paper, we focus on finding positive invariants
                  and Lyapunov functions to establish reachability and
                  stability properties, respectively, of polynomial
                  ordinary differential equations (ODEs). In general,
                  the search for such functions is a hard problem. As
                  a result, numerous techniques have been developed to
                  search for polynomial differential variants that
                  yield positive invariants and polynomial Lyapunov
                  functions that prove stability, for systems defined
                  by polynomial differential equations. However, the
                  systematic search for non-polynomial functions is
                  considered a much harder problem, and has received
                  much less attention.  In this paper, we combine
                  ideas from computer algebra with the Sum-Of-Squares
                  (SOS) relaxation for polynomial positive
                  semi-definiteness to find non polynomial
                  differential variants and Lyapunov functions for
                  polynomial ODEs. Using the well-known concept of
                  Darboux polynomials, we show how Darboux polynomials
                  can, in many instances, naturally lead to specific
                  forms of Lyapunov functions that involve rational
                  function, logarithmic and exponential terms.We
                  demonstrate the value of our approach by deriving
                  non-polynomial Lyapunov functions for numerical
                  examples drawn from the literature.},
  doi = {10.1109/ACC.2014.6859330},
  pdf = {pdf/goubault2014finding.pdf}
}
@inproceedings{jourdan2015formally,
  author = {Jourdan, Jacques-Henri and Laporte, Vincent and Blazy, Sandrine and
	Leroy, Xavier and Pichardie, David},
  title = {A formally-verified {C} static analyzer},
  booktitle = {Symposium on Principles of Programming Languages (POPL)},
  month = {January},
  year = {2015},
  pages = {247--259},
  organization = {ACM},
  abstract = {This paper reports on the design and soundness proof,
                  using the Coq proof assistant, of Verasco, a static
                  analyzer based on abstract interpretation for most
                  of the ISO C 1999 language (excluding recursion and
                  dynamic allocation). Verasco establishes the absence
                  of run-time errors in the analyzed programs. It
                  enjoys a modular architecture that supports the
                  extensible combination of multiple abstract domains,
                  both relational and non-relational. Verasco
                  integrates with the CompCert formally-verified C
                  compiler so that not only the soundness of the
                  analysis results is guaranteed with mathematical
                  certitude, but also the fact that these guarantees
                  carry over to the compiled code.},
  doi = {10.1145/2676726.2676966},
  pdf = {pdf/jourdan2015formally.pdf}
}
@inproceedings{jourdan2012validating,
  author = {Jourdan, Jacques-Henri and Pottier, Fran{\c{c}}ois and Leroy, Xavier},
  title = {Validating {LR(1)} Parsers},
  booktitle = {European Symposium on Programming (ESOP)},
  year = {2012},
  month = {March},
  publisher = {Springer},
  pages = {397--416},
  abstract = {An LR(1) parser is a finite-state automaton, equipped
                  with a stack, which uses a combination of its
                  current state and one lookahead symbol in order to
                  determine which action to perform next. We present a
                  validator which, when applied to a context-free
                  grammar G and an automaton A, checks that A and G
                  agree. Validating the parser provides the
                  correctness guarantees required by verified
                  compilers and other high-assurance software that
                  involves parsing. The validation process is
                  independent of which technique was used to construct
                  A. The validator is implemented and proved correct
                  using the Coq proof assistant.  As an application,
                  we build a formally-verified parser for the C99
                  language.},
  doi = {10.1007/978-3-642-28869-2_20},
  pdf = {pdf/jourdan2012validating.pdf}
}
@inproceedings{krebbers2018mosel,
  title = {{MoSeL}: a general, extensible modal framework for interactive proofs in separation logic},
  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},
  booktitle = {International Conference on Functional Programming (ICFP)},
  month = {September},
  year = {2018},
  organization = {ACM},
  abstract = { A number of tools have been developed for carrying out
                  separation-logic proofs mechanically using an
                  interactive proof assistant. One of the most
                  advanced such tools is the Iris Proof Mode (IPM) for
                  Coq, which offers a rich set of tactics for making
                  separation-logic proofs look and feel like ordinary
                  Coq proofs. However, IPM is tied to a particular
                  separation logic (namely, Iris), thus limiting its
                  applicability.

                  In this paper, we propose MoSeL, a
                  general and extensible Coq framework that brings the
                  benefits of IPM to a much larger class of separation
                  logics. Unlike IPM, MoSeL is applicable to both
                  affine and linear separation logics (and
                  combinations thereof), and provides generic tactics
                  that can be easily extended to account for the
                  bespoke connectives of the logics with which it is
                  instantiated. To demonstrate the effectiveness of
                  MoSeL, we have instantiated it to provide effective
                  tactical support for interactive and semi-automated
                  proofs in six very different separation logics.},
  doi = {10.1145/3236772},
  pdf = {pdf/krebbers2018mosel.pdf}
}
@inproceedings{mevel2019time,
  author = {M{\'e}vel, Glen and Jourdan, Jacques-Henri and Pottier, Fran{\c{c}}ois},
  title = {Time Credits and time Receipts in {I}ris},
  booktitle = {European Symposium on Programming (ESOP)},
  year = {2019},
  month = {April},
  abstract = {We present a machine-checked extension of the program
                  logic Iris with time credits and time receipts, two
                  dual means of reasoning about time. Whereas time
                  credits are used to establish an upper bound on a
                  program’s execution time, time receipts can be used
                  to establish a lower bound. More strikingly, time
                  receipts can be used to prove that certain
                  undesirable events—such as integer overflows—cannot
                  occur until a very long time has elapsed. We present
                  several machine-checked applications of time credits
                  and time receipts, including an application where
                  both concepts are exploited.},
  doi = {10.1007/978-3-030-17184-1_1},
  pdf = {pdf/mevel2019time.pdf},
  publisher = {Springer}
}
@inproceedings{gueneau2019formal,
  author = {Gu{\'e}neau, Arma{\"e}l and Jourdan, Jacques-Henri and Chargu{\'e}raud, Arthur and Pottier Fran{\c{c}}ois},
  title = {Formal Proof and Analysis of an Incremental Cycle Detection Algorithm},
  booktitle = {Interactive Theorem Proving (ITP)},
  year = {2019},
  month = {September},
  abstract = {We study a state-of-the-art incremental cycle detection
                  algorithm due to Bender, Fineman, Gilbert, and
                  Tarjan. We propose a simple change that allows the
                  algorithm to be regarded as genuinely online. Then,
                  we exploit Separation Logic with Time Credits to
                  simultaneously verify the correctness and the
                  worst-case amortized asymptotic complexity of the
                  modified algorithm.},
  pdf = {pdf/gueneau2019formal.pdf},
  doi = {10.4230/LIPIcs.ITP.2019.18}
}
@inproceedings{vilhena2020spy,
  author = {de Vilhena, Paulo Em{\'i}lio and Pottier, François and Jourdan, Jacques-Henri},
  title = {Spy Game: Verifying a Local Generic Solver in {I}ris},
  booktitle = {Symposium on Principles of Programming Languages (POPL)},
  month = {January},
  year = {2020},
  organization = {ACM},
  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 modulus function, an archetypical example
                  of spying.},
  pdf = {pdf/vilhena2020spy.pdf},
  doi = {10.1145/3371101}
}
@inproceedings{dang2020rustbelt,
  author = {Dang, Hoang-Hai and Jourdan, Jacques-Henri and Kaiser, Jan-Oliver and Dreyer Derek},
  title = {{RustBelt} Meets Relaxed Memory},
  booktitle = {Symposium on Principles of Programming Languages (POPL)},
  month = {January},
  year = {2020},
  organization = {ACM},
  abstract = {The Rust programming language supports safe systems
                  programming by means of a strong ownership-tracking
                  type system. In their prior work on RustBelt, Jung
                  et al. began the task of setting Rust’s safety
                  claims on a more rigorous formal
                  foundation. Specifically, they used Iris, a
                  Coq-based separation logic framework, to build a
                  machine-checked proof of semantic soundness for a
                  λ-calculus model of Rust, as well as for a number of
                  widely-used Rust libraries that internally employ
                  unsafe language features. However, they also made
                  the significant simplifying assumption that the
                  language is sequentially consistent. In this paper,
                  we adapt RustBelt to account for the relaxed-memory
                  operations that concurrent Rust libraries actually
                  use, in the process uncovering a data race in the
                  Arc library. We focus on the most interesting
                  technical problem: how to reason about resource
                  reclamation under relaxed memory, using a logical
                  construction we call synchronized ghost state.},
  pdf = {pdf/dang2020rustbelt.pdf},
  doi = {10.1145/3371102}
}
@inproceedings{mevel20cosmo,
  author = {Glen Mével and Jacques-Henri Jourdan and François
                 Pottier},
  title = {Cosmo: A Concurrent Separation Logic for {Multicore
                 OCaml}},
  month = {September},
  year = {2020},
  booktitle = {International Conference on Functional Programming (ICFP)},
  organization = {ACM},
  pdf = {pdf/mevel2020cosmo.pdf},
  doi = {10.1145/3408978},
  abstract = {Multicore OCaml extends OCaml with support for
                 shared-memory concurrency. It is equipped with a weak
                 memory model, for which an operational semantics has
                 been published. This begs the question: what reasoning
                 rules can one rely upon while writing or verifying
                 Multicore OCaml code? To answer it, we instantiate
                 Iris, a modern descendant of Concurrent Separation
                 Logic, for Multicore OCaml. This yields a low-level
                 program logic whose reasoning rules expose the details
                 of the memory model. On top of it, we build a
                 higher-level logic, Cosmo, which trades off some
                 expressive power in return for a simple set of
                 reasoning rules that allow accessing nonatomic
                 locations in a data-race-free manner, exploiting the
                 sequentially-consistent behavior of atomic locations,
                 and exploiting the release/acquire behavior of atomic
                 locations. Cosmo allows both low-level reasoning, where
                 the details of the Multicore OCaml memory model are
                 apparent, and high-level reasoning, which is
                 independent of this memory model. We illustrate this
                 claim via a number of case studies: we verify several
                 implementations of locks with respect to a classic,
                 memory-model-independent specification. Thus, a
                 coarse-grained application that uses locks as the sole
                 means of synchronization can be verified in the
                 Concurrent-Separation-Logic fragment of Cosmo, without
                 any knowledge of the weak memory model.}
}
@inproceedings{mevel21formal,
  author = {Glen Mével and Jacques-Henri Jourdan},
  title = {Formal Verification of a Concurrent Bounded Queue in a Weak Memory Model},
  month = {September},
  year = {2021},
  booktitle = {International Conference on Functional Programming (ICFP)},
  organization = {ACM},
  pdf = {pdf/mevel2021formal.pdf},
  doi = {10.1145/3473571},
  abstract = {We use Cosmo, a modern concurrent separation logic, to
                  formally specify and verify an implementation of a
                  multiple-producer multiple-consumer concurrent queue
                  in the setting of the Multicore OCaml weak memory
                  model.  We view this result as a demonstration and
                  experimental verification of the manner in which
                  Cosmo allows modular and formal reasoning about
                  advanced concurrent data structures.  In particular,
                  we show how the joint use of logically atomic
                  triples and of Cosmo's views makes it possible to
                  describe precisely in the specification the
                  interaction between the queue library and the weak
                  memory model.}
}
@inproceedings{matsushita2022rusthorn,
  title = {{RustHornBelt}: A semantic foundation for functional verification of Rust programs with unsafe code},
  author = {Matsushita, Yusuke and Denis, Xavier and Jourdan, Jacques-Henri and Dreyer, Derek},
  booktitle = {Conference on Programming Language Design and Implementation (PLDI)},
  month = {June},
  year = {2022},
  organization = {ACM},
  abstract = { Rust is a systems programming language that offers both
                  low-level memory operations and high-level safety
                  guarantees, via a strong ownership type system that
                  prohibits mutation of aliased state.  In prior work,
                  Matsushita et al. developed RustHorn, a promising
                  technique for functional verification of Rust code:
                  it leverages the strong invariants of Rust types to
                  express the behavior of stateful Rust code with
                  first-order logic (FOL) formulas, whose verification
                  is amenable to off-the-shelf automated techniques.
                  RustHorn's key idea is to use prophecies to describe
                  the behavior of mutable borrows.  However, the
                  soundness of RustHorn was only established for a
                  safe subset of Rust, and it has remained unclear how
                  to extend it to support various safe APIs that
                  encapsulate unsafe code (i.e., code where Rust's
                  aliasing discipline is relaxed).  In this paper, we
                  present RustHornBelt, the first machine-checked
                  proof of soundness for RustHorn-style verification
                  which supports giving FOL specs to safe APIs
                  implemented with unsafe code.  RustHornBelt employs
                  the approach of semantic typing used in Jung et
                  al.'s RustBelt framework, but it extends RustBelt's
                  model to reason not only about safety but also
                  functional correctness.  The key challenge in
                  RustHornBelt is to develop a semantic model of
                  RustHorn-style prophecies, which we achieve via a
                  new separation-logic mechanism we call parametric
                  prophecies.},
  pdf = {pdf/matsushita2022rusthorn.pdf},
  doi = {10.1145/3519939.3523704}
}
@inproceedings{denis2022creusot,
  title = {Creusot: a Foundry for the Deductive Verication of Rust Programs},
  author = {Denis, Xavier and Jourdan, Jacques-Henri and March{\'e}, Claude},
  booktitle = {International Conference on Formal Engineering Methods (ICFEM)},
  month = {October},
  year = {2022},
  organization = {Springer Verlag},
  abstract = {Rust is a fairly recent programming language for system
                  programming, bringing static guarantees of memory
                  safety through a strict ownership policy. The strong
                  guarantees brought by this feature opens promising
                  progress for deductive verification, which aims at
                  proving the conformity of Rust code with respect to
                  a specification of its intended behavior. We present
                  the foundations of Creusot, a tool for the formal
                  specification and deductive verification of Rust
                  code.  A first originality comes from Creusot's
                  specification language, which features a notion of
                  prophecy to reason about memory mutation, working in
                  harmony with Rust's ownership system. A second
                  originality is how Creusot builds upon Rust trait
                  system to provide several advanced abstraction
                  features.  },
  pdf = {pdf/denis2022creusot.pdf},
  doi = {10.1007/978-3-031-17244-1_6}
}
@inproceedings{denis2023iterators,
  title = {Specifying and Verifying Higher-order Rust Iterators},
  author = {Denis, Xavier and Jourdan, Jacques-Henri},
  booktitle = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
  month = {April},
  year = {2023},
  organization = {Springer Verlag},
  abstract = {In Rust, programs are often written using iterators, but
                  these pose problems for verification: they are
                  non-deterministic, infinite, and often higher-order,
                  effectful and built using adapters.  We present a
                  general framework for specifying and reasoning with
                  Rust iterators in first-order logic.  Our approach
                  is capable of addressing the challenges set out
                  above, which we demonstrate by verifying real Rust
                  iterators, including a higher-order, effectful map.
                  Using the Creusot verification platform, we evaluate
                  our framework on clients of iterators, showing it
                  leads to efficient verification of complex
                  functional properties.},
  pdf = {pdf/denis2023iterators.pdf},
  doi = {10.1007/978-3-031-30820-8_9}
}
@inproceedings{pottier2023thunks,
  author = {Pottier, Fran{\c{c}}ois and Gu{\'e}neau, Arma{\"e}l and Jourdan, Jacques-Henri and M{\'e}vel, Glen},
  title = {Thunks and Debits in Separation Logic with Time Credits},
  booktitle = {Symposium on Principles of Programming Languages (POPL)},
  month = {January},
  year = {2024},
  organization = {ACM},
  abstract = {A thunk is a mutable data structure that offers a simple
                  memoization service: it stores either a suspended
                  computation or the result of this computation.
                  Okasaki (1999) presents many data structures that
                  exploit thunks to achieve good amortized time
                  complexity. He analyzes their complexity by
                  associating a debit with every thunk. A debit can be
                  paid off in several increments; a thunk whose debit
                  has been fully paid off can be forced. Quite
                  strikingly, a debit is associated also with future
                  thunks, which do not yet exist in memory. Some of
                  the debit of a faraway future thunk can be
                  transferred to a nearer future thunk. We present a
                  complete machine-checked reconstruction of Okasaki's
                  reasoning rules in Iris$, a rich separation logic
                  with time credits. We demonstrate the applicability
                  of the rules by verifying a few operations on
                  streams as well as several of Okasaki's data
                  structures, namely the physicist's queue, implicit
                  queues, and the banker's queue.},
  pdf = {pdf/pottier2023thunks.pdf},
  doi = {10.1145/3632892}
}
@article{jung2018iris,
  title = {Iris from the ground up},
  author = {Jung, Ralf and Krebbers, Robbert and Jourdan, Jacques-Henri and Bizjak, Ale{\v{s}} and Birkedal, Lars and Dreyer, Derek},
  journal = {Journal of Functional Programming (JFP)},
  year = {2018},
  volume = {28},
  number = {e20},
  abstract = {Iris is a framework for higher-order concurrent
                  separation logic, which has been implemented in the
                  Coq proof assistant and deployed very effectively in
                  a wide variety of verification projects. Iris was
                  designed with the express goal of simplifying and
                  consolidating the foundations of modern separation
                  logics, but it has evolved over time, and the design
                  and semantic foundations of Iris itself have yet to
                  be fully written down and explained together
                  properly in one place. Here, we attempt to fill this
                  gap, presenting a reasonably complete picture of the
                  latest version of Iris (version 3.1), from first
                  principles and in one coherent narrative.},
  doi = {10.1017/S0956796818000151},
  publisher = {Cambridge University Press},
  pdf = {pdf/jung2018iris.pdf}
}
@article{jourdan2017simple,
  author = {Jourdan, Jacques-Henri and Pottier, Fran{\c{c}}ois},
  title = {A simple, possibly correct {LR} parser for {C11}},
  journal = {Transactions on Programming Languages and Systems (TOPLAS)},
  year = {2017},
  month = {August},
  volume = {39},
  number = {4},
  abstract = { The syntax of the C programming language is described
                  in the C11 standard by an ambiguous context-free
                  grammar, accompanied with English prose that
                  describes the concept of “scope” and indicates how
                  certain ambiguous code fragments should be
                  interpreted. Based on these elements, the problem of
                  implementing a compliant C11 parser is not entirely
                  trivial. We review the main sources of difficulty
                  and describe a relatively simple solution to the
                  problem. Our solution employs the well-known
                  technique of combining an LALR(1) parser with a
                  “lexical feedback” mechanism. It draws on folklore
                  knowledge and adds several original aspects,
                  including: a twist on lexical feedback that allows a
                  smooth interaction with lookahead; a simplified and
                  powerful treatment of scopes; and a few amendments
                  in the grammar. Although not formally verified, our
                  parser avoids several pitfalls that other
                  implementations have fallen prey to. We believe that
                  its simplicity, its mostly-declarative nature, and
                  its high similarity with the C11 grammar are strong
                  informal arguments in favor of its correctness. Our
                  parser is accompanied with a small suite of “tricky”
                  C11 programs. We hope that it may serve as a
                  reference or a starting point in the implementation
                  of compilers and analysis tools. },
  pdf = {pdf/jourdan2017simple.pdf},
  publisher = {ACM},
  doi = {10.1145/3064848}
}
@article{boldo2015verified,
  author = {Boldo, Sylvie and Jourdan, Jacques-Henri and Leroy, Xavier and Melquiond,
	Guillaume},
  title = {Verified Compilation of Floating-Point Computations},
  journal = {Journal of Automated Reasoning (JAR)},
  year = {2015},
  month = {February},
  volume = {54},
  pages = {135--163},
  number = {2},
  abstract = {Floating-point arithmetic is known to be tricky:
                  roundings, formats, exceptional values. The IEEE-754
                  standard was a push towards straightening the field
                  and made formal reasoning about floating-point
                  computations easier and flourishing. Unfortunately,
                  this is not sufficient to guarantee the final result
                  of a program, as several other actors are involved:
                  programming language, compiler, and
                  architecture. The CompCert formally-verified
                  compiler provides a solution to this problem: this
                  compiler comes with a mathematical specification of
                  the semantics of its source language (a large subset
                  of ISO C99) and target platforms (ARM, PowerPC,
                  x86-SSE2), and with a proof that compilation
                  preserves semantics. In this paper, we report on our
                  recent success in formally specifying and proving
                  correct CompCert’s compilation of floating-point
                  arithmetic. Since CompCert is verified using the Coq
                  proof assistant, this effort required a suitable Coq
                  formalization of the IEEE-754 standard; we extended
                  the Flocq library for this purpose. As a result, we
                  obtain the first formally verified compiler that
                  provably preserves the semantics of floating-point
                  programs.},
  doi = {10.1007/s10817-014-9317-x},
  publisher = {Springer},
  pdf = {pdf/boldo2015verified.pdf}
}
@article{braibant2014implementing,
  author = {Braibant, Thomas and Jourdan, Jacques-Henri and Monniaux, David},
  title = {Implementing and reasoning about hash-consed data structures in {C}oq},
  journal = {Journal of Automated Reasoning (JAR)},
  year = {2014},
  month = {October},
  volume = {53},
  pages = {271--304},
  number = {3},
  abstract = {We report on four different approaches to implementing
                  hash-consing in Coq programs. The use cases include
                  execution inside Coq, or execution of the extracted
                  OCaml code. We explore the different trade-offs
                  between faithful use of pristine extracted code, and
                  code that is fine-tuned to make use of OCaml
                  programming constructs not available in Coq. We
                  discuss the possible consequences in terms of
                  performances and guarantees. We use the running
                  example of binary decision diagrams and then
                  demonstrate the generality of our solutions by
                  applying them to other examples of hash-consed data
                  structures.},
  doi = {10.1007/s10817-014-9306-0},
  publisher = {Springer},
  pdf = {pdf/braibant2014implementing.pdf}
}
@article{jung2020safe,
  author = {Jung, Ralf and Jourdan, Jacques-Henri and Krebbers, Robbert and Dreyer, Derek},
  title = {Safe Systems Programming in {R}ust: The Promise and the Challenge},
  journal = {Communications of The ACM},
  year = {2021},
  month = mar,
  publisher = {Association for Computing Machinery},
  volume = {64},
  number = {4},
  doi = {10.1145/3418295},
  abstract = { • Rust is the first industry-supported programming
                  language to overcome the longstanding tradeoff
                  between the safety guarantees of higher-level
                  languages (like Java) and the control over resource
                  management provided by lower-level "systems
                  programming" languages (like C and C++).

                  • It tackles this challenge using a strong type
                  system based on the ideas of ownership and borrowing,
                  which statically prohibits the mutation of shared
                  state. This approach enables many common systems
                  programming pitfalls to be detected at compile time.

                  • There are a number of data types whose
                  implementations fundamentally depend on shared
                  mutable state and thus cannot be typechecked
                  according to Rust’s strict ownership discipline. To
                  support such data types, Rust embraces the judicious
                  use of unsafe code encapsulated within safe APIs.

                  • The proof technique of semantic type soundness,
                  together with advances in separation
                  logic and machine-checked proof, has enabled us to
                  begin building rigorous formal foundations for Rust
                  as part of the RustBelt project.},
  pdf = {pdf/jung2020safe.pdf},
  pages = {144–152},
  numpages = {9}
}
@phdthesis{jourdan2016verasco,
  author = {Jourdan, Jacques-Henri},
  title = {Verasco: a Formally Verified {C} Static Analyzer},
  year = {2016},
  month = {May},
  abstract = {In order to develop safer software for critical
                  applications, some static analyzers aim at
                  establishing, with mathematical certitude, the
                  absence of some classes of bug in the input
                  program. A possible limit to this approach is the
                  possibility of a soundness bug in the static
                  analyzer itself, which would nullify the guarantees
                  it is supposed to deliver.  In this thesis, we
                  propose to establish formal guarantees on the static
                  analyzer itself: we present the design,
                  implementation and proof of soundness using Coq of
                  Verasco, a formally verified static analyzer based
                  on abstract interpretation handling most of the ISO
                  C99 language, including IEEE754 floating-point
                  arithmetic (except recursion and dynamic memory
                  allocation). Verasco aims at establishing the
                  absence of erroneous behavior of the given
                  programs. It enjoys a modular extendable
                  architecture with several abstract domains and
                  well-specified interfaces. We present the abstract
                  iterator of Verasco, its handling of bounded machine
                  arithmetic, its interval abstract domain, its
                  symbolic abstract domain and its abstract domain of
                  octagons. Verasco led to the development of new
                  techniques for implementing data structure with
                  sharing in Coq.},
  pdf = {thesis_jhjourdan.pdf},
  school = {Université Paris Diderot (Paris 7)}
}
@misc{jourdan2016statistically,
  author = {Jourdan, Jacques-Henri},
  title = {Statistically profiling memory in {OCaml}},
  howpublished = {OCaml Workshop},
  year = {2016},
  month = {September},
  pdf = {pdf/jourdan2016statistically.pdf}
}
@inproceedings{jourdan2016sparsity,
  author = {Jourdan, Jacques-Henri},
  title = {Sparsity Preserving Algorithms for Octagons},
  booktitle = {Numerical and Symbolic Abstract Domains Workshop (NSAD)},
  year = {2016},
  month = {September},
  abstract = {Known algorithms for manipulating octagons do not
                  preserve their sparsity, leading typically to
                  quadratic or cubic time and space complexities even
                  if no relation among variables is known when they
                  are all bounded. In this paper, we present new
                  algorithms, which use and return octagons
                  represented as weakly closed difference bound
                  matrices, preserve the sparsity of their input and
                  have better performance in the case their inputs are
                  sparse. We prove that these algorithms are as
                  precise as the known ones.},
  pdf = {pdf/jourdan2016sparsity.pdf},
  publisher = {Elsevier},
  pages = {57--70},
  doi = {10.1016/j.entcs.2017.02.004}
}
@inproceedings{briais20123d,
  author = {Briais, S{\'e}bastien and Caron, St{\'e}phane and Cioranesco, Jean-Michel
	and Danger, Jean-Luc and Guilley, Sylvain and Jourdan, Jacques-Henri
	and Milchior, Arthur and Naccache, David and Porteboeuf, Thibault},
  title = {{3D} Hardware Canaries},
  booktitle = {Cryptographic Hardware and Embedded Systems (CHES)},
  year = {2012},
  month = {September},
  pages = {1--22},
  publisher = {Springer},
  abstract = {3D integration is a promising advanced manufacturing
                  process offering a variety of new hardware security
                  protection opportunities. This paper presents a way
                  of securing 3D ICs using Hamiltonian paths as
                  hardware integrity verification sensors. As 3D
                  integration consists in the stacking of many metal
                  layers, one can consider surrounding a
                  security-sensitive circuit part by a wire cage.
                  After exploring and comparing different cage
                  construction strategies (and reporting preliminary
                  implementation results on silicon), we introduce a
                  "hardware canary". The canary is a spatially
                  distributed chain of functions F i positioned at the
                  vertices of a 3D cage surrounding a protected
                  circuit. A correct answer (F n  ∘ … ∘ F 1)(m) to a
                  challenge m attests the canary's integrity.},
  doi = {10.1007/978-3-642-33027-8_1},
  pdf = {pdf/briais20123d.pdf}
}

This file was generated by bibtex2html 1.99.