Jacques-Henri Jourdan


CV: English - Francais


Email

jacques-henri.jourdan [at] normalesup [dot] org

My PGP public key

Address (MPI-SWS)

Jacques-Henri Jourdan
Max Plank Institute for Software Systems (MPI-SWS)
Campus E1 5
D-66123 Saarbrücken
Germany

publications.bib

@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}
}
@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}
}
@misc{jourdan2016statistically,
  author = {Jourdan, Jacques-Henri},
  title = {Statistically profiling memoy 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}
}
@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)}
}
@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}
}
@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}
}
@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}
}
@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{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}
}
@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}
}

This file was generated by bibtex2html 1.98.