Seminar (2020-2021)

The following talks were given at the Épicure seminar during the academic year 2020-2021:

12/02/21: Vincent Rébiscoul, “Analyses Statiques pour Sémantiques Squelettiques”
05/02/21: Yann Herklotz (Imperial College, UK), “Formal Verification of High-Level Synthesis” abstract
High-level synthesis (HLS), which refers to the automatic compilation of software into hardware, is rapidly gaining popularity. In a world increasingly reliant on application-specific hardware accelerators, HLS promises hardware designs of comparable performance and energy efficiency to those coded by hand in a hardware description language like Verilog, while maintaining the convenience and the rich ecosystem of software development. However, current HLS tools cannot always guarantee that the hardware designs they produce are equivalent to the software they were given, thus undermining any reasoning conducted at the software level. Worse, there is mounting evidence that existing HLS tools are quite unreliable, sometimes generating wrong hardware or crashing when given valid inputs. To address this problem, we present the first HLS tool that is mechanically verified to preserve the behaviour of its input software. Our tool, called Vericert, extends the CompCert verified C compiler with a new hardware-oriented intermediate language and a Verilog back end, and has been proven correct in Coq. Vericert supports all C constructs except for case statements, function pointers, recursive function calls, integers larger than 32 bits, floats, and global variables. An evaluation on the PolyBench/C benchmark suite indicates that Vericert generates hardware that is around an order of magnitude slower and larger than hardware generated by an existing, optimising (but unverified) HLS tool.
29/01/21: Emmanuel Fleury
18/12/20: Aurèle Barrière, “Formally Verified Speculation and Deoptimization in a JIT Compiler” abstract
Just-in-time compilers for dynamic languages routinely generate code under assumptions that may be invalidated at run-time, this allows for specialization of program code to the common case in order to avoid unnecessary overheads due to uncommon cases. This form of software speculation requires support for deoptimization when some of the assumptions fail to hold. We present a model just-in-time compiler with an intermediate representation that explicits the synchronization points used for deoptimization and the assumptions made by the compiler’s speculation. We also present several common compiler optimizations that can leverage speculation to generate improved code. The optimizations are proved correct with the help of a proof assistant. While our work stops short of proving native code generation, we demonstrate how one could use the verified optimization to obtain significant speed ups in an end-to-end setting.
07/12/20: Solène Mirliaz, “Provable Cost Analysis of Cryptographic Code”
27/11/20: Adam Khayam, “JSkel – A JavaScript Formalization in Skeletal Semantics” Slides
13/11/20: Santiago Bautista, “Numeric domains meet algebraic types” Slides abstract
We report on the design and formalization of a novel abstract domain, called numeric path relations (NPRs), that combines numeric relational domains with algebraic data types. This domain expresses relations between algebraic values that can contain scalar data. The construction of the domain is parameterized by the choice of a relational domain on scalar values. The construction employs projection paths on algebraic values, and in particular projections on variant cases, whose sound treatment is subtle due to mutual exclusiveness.
23/10/20: Timothée Haudebourg, “Regular Language Type Inference with Term Rewriting” Slides abstract
This paper defines a new type system applied to the fully automatic verification of safety properties on higher-order tree-processing functional programs. We use term rewriting systems to model the program and its semantics and tree automata to model algebraic data types. We define the regular abstract interpretation of the input term rewriting system where the abstract domain is a set of regular languages. From the regular abstract interpretation we derive a type system where each type is a regular language. We define an inference procedure for this type system which allows us check the validity of safety properties. The inference mechanism is built on an invariant learning procedure based on the tree automata completion algorithm. This invariant learning procedure is regularly-complete and complete in refutation, meaning that if it is possible to give a regular type to a term then we will eventually find it, and if there is no possible type (regular or not) then we will eventually find a counter-example.
16/10/20: Simon Castellan, “Causality: A monad for truly concurrent computation” Slides abstract
Causal models have always had difficulty to gain widespread use to model concurrent languages due to their difficulty both to define the semantics, and then to implement it. Recently, a methodology based on event structures called concurrent games made it possible to define the semantics for a wide variety of concurrent languages. However this semantics is abstract and untractable. Moreover, defining the model of a new language requires familiarity with the intricacies of the model. In this talk, I will present my efforts towards implementing causal and interactive semantics based on event structures. This implementation relies on a monad that supports effects for concurrency, which allows to write interpreter for concurrent languages in a straightforward way and automatically extract an event structure semantics out of it, without having to manipulate explicitly event structures.
09/10/20: Delphine Demange, “Intermittent Computing with Peripherals, Formally Verified” Website abstract
Transiently-powered systems featuring non-volatile memory as well as external peripherals enable the development of new low-power sensor applications. However, as programmers, we are ill-equipped to reason about systems where power failures are the norm rather than the exception. A first challenge consists in being able to capture all the volatile state of the application – external peripherals included – to ensure progress. A second, more fundamental, challenge consists in specifying how power failures may interact with peripheral operations. In this work, we propose a formal specification of intermittent computing with peripherals, an axiomatic model of interrupt-based checkpointing as well as its proof of correctness, machine-checked in the Coq proof assistant. We also illustrate our model with several systems proposed in the literature. This is joint work with Gautier Berthou, Pierre-Évariste Dagand, Rémi Oudin, and Tanguy Risset.
29/09/20: Guillaume Ambal, “Formal Transformations of Operational Semantics” Slides abstract
Skeletal semantics is a recent framework developed to formalize languages, from λ-calculus to JavaScript. Languages can be defined in a range of format, including the intuitive big-step (Natural Semantics), or the more detailed small-step (Structural Operational Semantics). In this talk, I will present a new fully-automatic generic transformation to derive a small-step semantics from a big-step one. We also generate a Coq proof of equivalence as a bonus.
29/09/20: Benoît Montagu, “Stable Relations and Abstract Interpretation of Higher-Order Programs” abstract
We present a novel denotational semantics for the untyped call-by-value λ-calculus, where terms are interpreted as stable relations, i.e. as binary relations between substitutions and values, enjoying a monotonicity property. The denotation captures the input-output behaviour of higher-order programs, and is proved sound and complete with respect to the operational semantics. The definition also admits a presentation as a program logic. Following the principles of abstract interpretation, we use our denotational semantics as a collecting semantics to derive a modular relational analysis for higher-order programs. The analysis infers equalities between the arguments of a program and its result — a form of frame condition for functional programs.
18/09/20: Thomas Rubiano, “WebAssembly : sémantique et sécurité”