CV: English - Francais
jacques-henri.jourdan [at] cnrs [dot] fr
Mail address
LMF - Laboratoire Méthodes Formelles, Bât. 650Univerité Paris-Saclay
91405 Orsay Cedex
France
Physical address
LMF - Bât. 650, bureau 2731, 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 Verification 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{pottier2024thunks,
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/pottier2024thunks.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.