Elles auront lien dans l’Amphithéâtre du Bâtiment Sophie Germain de l’Université Paris Diderot. Voir les informations locales pour obtenir l’accès.
JEUDI 16 JUIN#
13:00–13:15Accueil13:15–13:30Mots de bienvenue13:30–15:45Session thématique : Analyse statique et vérification de programmes
(Responsable: Delphine Demange)
- Delphine Demange, Mechanized Verification of SSA-based Compilers Techniques [abstract]Modern optimizing compilers rely on the Static Single Assignment (SSA) form to make optimizations fast and simpler to implement. In this talk, I will recall the basics of SSA, and discuss the challenges that it raises in the context of verified compilation. Then, I will report on the results obtained so far within the CompCertSSA project, which extends the CompCert compiler with an SSA middle-end.
- Jacques-Henri Jourdan, Verasco, un analyseur statique formellement vérifié pour C [abstract]Cet exposé présentera la conception et la preuve de correction de Verasco, un analyseur statique formellement vérifié pour une grande partie du langage C99, développé avec l’assistant de preuve Coq. Verasco tente d’établir l’absence d’erreur à l’exécution des programmes analysés. Il est conçu selon une architecture modulaire qui permet une combinaison extensible de nombreux domaines abstraits, relationnels ou non. Verasco a un domaine abstrait pour la mémoire, un domaine abstrait symbolique d’égalités arithmétiques, un domaine abstrait d’intervalles, un domaine abstrait de congruences arithmétiques et un domaine d’octogones. Verasco réutilise le front-end de CompCert, si bien que Verasco ne garantie pas seulement la correction de son analyse, mais aussi le fait que ces garanties sont conservées jusqu’au code compilé.
- David Monniaux, Proving array-manipulating programs without arrays [abstract]Proving automatically the correctness of programs operating over arrays or mutable maps is difficult. We present an approach that abstract away arrays so as to get a purely scalar problem. The correctness of that problem entails the correctness of the original program. This approach is sufficient for automatically proving the full functional correctness of classical sorting algorithms (e.g. selection sort). Joint work with Laure Gonnord.
- Frédéric Dabrowski, DRMA communications in the BSP model [abstract]We propose a formal semantics of DRMA communication facilities supported by most implementations of the BSP model. This specification abstracts away from the details of the local computations and considers only the communication requests they produce. We propose a validity criterion over communication requests which is independent of any underlying programming language. By proving that valid requests lead to successfull communication phases, we provide a suitable notion of correctness for BSP programs. We expect these results will be useful for future work on BSP programs verification.
15:45–16:15Pause café16:15–17:15Exposés courts
- Victor Magron, Formal Verification of Roundoff Error Bounds using Semidefinite Programming [abstract]Roundoff errors cannot be avoided when implementing numerical programs with finite precision. This problem becomes challenging when the program does not employ solely linear operations as non-linearities are inherent to many computational problems in real-world applications. To ensure safety of such non-linear programs, there is an obvious need for methods which output certificates that can be validated inside a proof assistant.We present a framework to provide upper and lower bounds of absolute roundoff errors. This framework is based on optimization techniques employing robust semidefinite programming (SDP) and sparse sums of squares certificates, which can be formally checked inside the Coq theorem prover.Our tool covers a wide range of nonlinear programs, including polynomials and transcendental operations as well as conditional statements. We illustrate the efficiency and precision of this tool on non-trivial programs coming from biology, optimization and space control.
- Jean-Christophe Léchenet, Cut Branches Before Looking for Bugs: Sound Verification on Relaxed Slices [abstract]Program slicing can be used to reduce a given initial program to a smaller one (a slice) which preserves the behavior of the initial program with respect to a chosen criterion. Verification and Validation of software can become easier on slices, but require particular care in presence of errors or non-termination in order to avoid unsound results or a poor level of reduction in slices. This article proposes a theoretical foundation for conducting Verification and Validation activities activities on a slice instead of the initial program. We introduce the notion of relaxed slicing that remains efficient even in presence of errors or non-termination, and establish an appropriate soundness property. It allows us to give a precise interpretation of verification results (absence or presence of errors) obtained for a slice in terms of the initial program. Our results have been proved in Coq.The talk will be given by the first author. It is based on the paper published at ETAPS/FASE 2016 [1]. The Coq formalization is available at http://perso.ecp.fr/~lechenetjc/slicing/.1. Léchenet, J., Kosmatov, N., Gall, P.L.: Cut branches before looking for bugs: Sound verification on relaxed slices. In: FASE’16 (Part of ETAPS’16). pp. 179–196 (2016)
- Engel Lefaucheux, Diagnosis in Infinite-State Probabilistic Systems [abstract]In a recent work, we introduced four variants of diagnosability FA, IA, FF, IF) in (finite) probabilistic systems (pLTS) depending whether one considers (1) finite or infinite runs and (2) faulty or all runs. We studied their relationship and established that the corresponding decision problems are PSPACE-complete. A key ingredient of the decision procedures was a characterisation of diagnosability by the fact that a random run almost surely lies in an open set whose specification only depends on the qualitative behaviour of the pLTS. Here we investigate similar issues for infinite pLTS. We first show that this characterisation still holds for FFdiag-diagnosability but with a Gδ set instead of an open set and also for IF and IA-diagnosability when pLTS are finitely branching. We also prove that surprisingly FA-diagnosability cannot be characterised in this way even in the finitely branching case. Then we apply our characterisations for a partially observable probabilistic extension of visibly pushdown automata (POpVPA), yielding EXPSPACE procedures for solving diagnosability problems. In addition, we establish some computational lower bounds and show that slight extensions of POpVPA lead to undecidability.
17:30–18h30Business meeting
VENDREDI 17 JUIN#
9:00–10:30Session thématique : Systèmes paramétrés
(Responsable: Arnaud Sangnier)
- Arnaud Sangnier, Parameterized verification of Networks with (selective) broadcast [abstract]We study decision problems for parameterized verification of a formal model of networks with broadcast communication in which the number of participants as the communication topoloby are paramters. The configuration of such a model can be represented thanks to graphs where nodes are labelled with states of individual processes. Adjacent nodes represent single-hop neighbors. Processes are finite state automata that communicate via broadcast messages. Reception of a broadcast is restricted to single-hop neighbors. We show that for such a model simple reachability questions are undecidable, but that decidability can be regained by either restricting the set of topologies or by allowing some processes not to receive the emitted messages. Finally, we consider verification problem under local strategies, where we assume that each process in the network behaves the same according to its past.
- Aiswarya Cyriac, Formal methods for the verification of distributed algorithms [abstract]We propose automata-theoretic approach for the verification of distributed algorithms in which processes can store, send and compare process-identifiers (pids). Examples include leader election algorithms and distributed sorting algorithms. We introduce a logic to specify correctness of such distributed algorithms. This logic is inspired by data logics, and can reason about processes and pids. The model checking problem is undecidable in general; we will see some ideas to regain decidability for distributed algorithms over ring topologies. Based on joint work with Benedikt Bollig and Paul Gastin.
10:30–11:00Pause café11:00–12:20Exposés courts
- Simon Halfon, Algorithmics of Well Quasi-Orderings [abstract]In this talk, I will present a generic representation of upward and downward closed subsets of the « natural » Well Quasi-Orderings, as well as algorithms for manipulating these sets (union, intersection, complement, …). This provides a toolbox to handle the WQOs frequently encountered e.g. in Verification. Joint work with Jean Goubault-Larrecq, Prateek Karandikar, Kumar Narayan and Philippe Schnoebelen.
- Nicolas Basset, Uniform Sampling for Timed Automata with Application to Language Inclusion Measurement [abstract]In this talk, I will present Monte Carlo model checking techniques to evaluate quantitative properties of timed languages. Our approach is based on uniform random sampling of behaviours, the uniformity being defined with respect to volume measure of timed languages previously studied by Asarin, Degorre and I. We implement our algorithms using tools PRISM, SageMath and COSMOS, and demonstrate their usefulness on statistical timed language inclusion measurement in terms of volume.
- Bruno Karelovic, Perfect-information Stochastic Priority Games [abstract]We present in this work an alternative solution to perfect-information stochastic parity games. Instead of use the elegant framework of $\mu$-calculus, which hides completely the algorithmic aspect, we solve it by induction on the number of absorbing states.
- Amina Doumane, Towards Completeness via Proof Search in the Linear Time mu-calculus [abstract]Modal mu-calculus is one of the central languages of logic and verification, whose study involves notoriously complex objects: automata over infinite structures on the model-theoretical side; infinite proofs and proofs by (co)induction on the proof-theoretical side. Nevertheless, axiomatizations have been given for both linear and branching time mu-calculi, with quite involved completeness arguments. We come back to this central problem, considering it from a proof search viewpoint, and provide some new completeness arguments in the linear time mu-calculus. Our results only deal with restricted classes of formulas that closely correspond to (non-alternating) ω-automata but, compared to earlier proofs, our completeness arguments are direct and constructive. We first consider a natural circular proof system based on sequent calculus, and show that it is complete for inclusions of parity automata expressed as formulas, making use of Safra’s construction directly in proof search. We then consider the corresponding finitary proof system, featuring (co)induction rules, and provide a partial translation result from circular to finitary proofs. This yields completeness of the finitary proof system for inclusions of sufficiently deterministic parity automata, and finally for arbitrary Büchi automata.
12:20–14:00Pause déjeuner14:00–16:15Session thématique : SAT/SMT
(Responsable: Pascal Fontaine)
- Gilles Audemard, Au coeur de SMT, les démonstrateurs SAT. [abstract]Dans cette présentation nous présentons les démonstrateurs SAT qui sont au coeur des démonstrateurs SMT. Nous commençons par une présentation succincte des ingrédients essentiels de ces solveurs. Ensuite, nous présentons l’utilisation incrémentale des démonstrateurs SAT, c’est à dire l’appel multiple de solveurs sur des instances proches les unes des autres. Nous introduisons quelques exemples d’utilisation incrémentale de SAT. Nous terminons par plusieurs pistes de recherche permettant d’espérer améliorer les moteurs SAT dans le cadre SMT.
- Pascal Fontaine, Une introduction à SMT [abstract]Les solveurs Satisfaisabilité Modulo Théories (SMT) permettent de décider la satisfaisabilité de grandes formules écrites dans des langages décidables, plus expressifs que la logique propositionnelle. Nous verrons l’architecture SMT, et comment elle s’articule autour d’un solveur SAT. En particulier, nous verrons par l’exemple comment on peut élever l’expressivité d’un solveur SAT vers des langages plus riches, et comment, à partir de procédures de décision pour différents langages, on peut construire une procédure de décision sur la combinaison des langages.Enfin, nous présenterons quelques solveurs SMT disponibles, la communauté SMT et les différentes initiatives, notamment le standard SMT-lib qui définit un langage d’entrée accepté par la majorité des solveurs SMT.
- Nicolas Peltier, Procédures de preuve par instanciation pour les problèmes SMT [abstract]