
@phdthesis{maiza_hardware_and_software_2023_tel-04741877,
	title = {Hardware and software analyses for precise and efficient timing analysis},
	abstract = {In hard real-time systems, encountered for example in the transportation, energy or medical domains, programs must not only provide a functionally correct result but also guarantee timing constraints. Our researches focus on timing models and analyses which aim to get precise bounds on execution time and delays. Generally, these models focus on a single hardware or software aspect. On the hardware side, our models and analyses focus on cache memories, memory bus arbitration and memory access ways in multi-core and many-core platforms. As part of software analysis, we took benefit from the infeasible path elimination during analysis: the idea is that the computation of the worst-case execution time should ignore paths that are not semantically possible. Additionally, we have shown that a better integration of software and hardware analyses leads to more precise bounds. In the context of multi-core timing systems, we have shown that timing analysis can benefit both from a better knowledge of software and hardware, and from the integration of timing analysis with the last step of implementation. We show how and where our work leads to changing the point of view on timing analysis in order to improve it. Finally, we expose the current state of the art and which gaps must still be filled to obtain a complete and efficient timing analysis.},
	author = {Maiza, C.},
	year = {2023},
	type = {HDR},
	eprinttype={HAL}, eprint = {tel-04741877},
	HAL_version = {v1},
}

@phdthesis{boulmé_formally_verified_defensive_2021_tel-03356701,
	title = {Formally Verified Defensive Programming (efficient Coq-verified computations from untrusted ML oracles)},
	abstract = {This document presents a lightweight approach – combining Coq and OCaml typecheckers – in order to formally verify higher-order imperative programs for partial correctness. In this approach, called FVDP (Formally Verified Defensive Programming), Coq-verified programs also contain some OCaml written functions, called oracles, which are untrusted: their implementation is simply ignored by the formal proof. Formal guarantees on the results of these oracles are obtained by combining dynamic tests in Coq with static properties deduced from OCaml types. Indeed, the simplest way to obtain a Coq-verified solver for a complex problem, often consists in combining an efficient OCaml oracle searching for "good" solutions with a verified defensive test able to ensure that the results found by the oracle have the expected properties. Hence, the solver benefits from the powerful imperative feature of OCaml, while hiding many complex details of its computation process to its formal proof: the theory of the defensive test is usually much simpler than the one of the oracle. The embedding of OCaml oracles into Coq is realized through a “may-return monad”, a structure that abstracts their side-effects by representing them as non-deterministic functions, and provided by the Impure library. This library also provides a very simple embedding of OCaml pointer equality, but powerful enough for defensive checks of some memoizing oracles (e.g. hash-consing of terms, memoized recursion). The document also shows how to deduce expressive invariants from the static OCaml type of polymorphic oracles, by adapting Wadler's “theorems for free” (based on Reynold's parametric polymorphism). This technique is exploited within a design pattern—for certificate producing oracles—called Polymorphic LCF Style (or Polymorphic Factory Style). Large Coq proofs on these higher-order impure defensive computations are decomposed thanks to data-refinement techniques in order to cleanly separate reasoning on pure data-structures and algorithms from reasonings on sequences of impure computations. Then, the latter are (semi)automated thanks to computations of weakest liberal preconditions. FVDP is detailed on several “realistic” applications: in optimizing compilation (instruction scheduling for CompCert), in static analysis (abstract domain of convex polyhedra of the VPL) and in automated deduction (Boolean SAT-solving and linear rational arithmetic). The document explains how FVDP, instantiated with a careful software design, both alleviates development times and running times of such formally verified applications.},
	author = {Boulmé, S.},
	year = {2021},
	type = {HDR},
	eprinttype={HAL}, eprint = {tel-03356701},
	HAL_version = {v1},
}

@phdthesis{devismes_versatility_and_efficiency_2020_tel-03080444,
	title = {Versatility and Efficiency in Self-Stabilizing Distributed Systems},
	author = {Devismes, S.},
	year = {2020},
	type = {HDR},
	eprinttype={HAL}, eprint = {tel-03080444},
	HAL_version = {v6},
}
