Exposés des semaines suivantes

Jeudi 9 janvier, 14h en salle Markov

Cezara Dragoi (INRIA - Antique)

Communication-Closed Asynchronous Protocols

The verification of asynchronous fault-tolerant distributed systems is challenging due to unboundedly many interleavings and network failures (e.g., processes crash or message loss). We propose a method that reduces the verification of asynchronous fault-tolerant protocols to the verification of round-based synchronous ones. Synchronous protocols are easier to verify due to fewer interleavings, bounded message buffers etc. We implemented our reduction method and applied it to several state machine replication and consensus algorithms. The resulting synchronous protocols are verified using existing deductive verification methods.

Lundi 13 janvier, 11h en salle Markov

Toby Murray (University of Melbourne)

Verifying that a compiler preserves concurrent value-dependent information-flow security.

It is common to prove by reasoning over source code that programs do not leak sensitive data. But doing so leaves a gap between reasoning and reality that can only be filled by accounting for the behaviour of the compiler. This task is complicated when programs enforce value-dependent information-flow security properties (in which classification of locations can vary depending on values in other locations) and complicated further when programs exploit shared-variable concurrency. Prior work has formally defined a notion of concurrency-aware refinement for preserving value-dependent security properties. However, that notion is considerably more complex than standard refinement definitions typically applied in the verification of semantics preservation by compilers. To date it remains unclear whether it can be applied to a realistic compiler, because there exist no general decomposition principles for separating it into smaller, more familiar, proof obligations. In this work, we provide such a decomposition principle, which we show can almost halve the complexity of proving secure refinement. Further, we demonstrate its applicability to secure compilation, by proving in Isabelle/HOL the preservation of value-dependent security by a proof-of-concept compiler from an imperative While language to a generic RISC-style assembly language, for programs with shared-memory concurrency mediated by locking primitives. Finally, we execute our compiler in Isabelle on a While language model of the Cross Domain Desktop Compositor, demonstrating to our knowledge the first use of a compiler verification result to carry an information-flow security property down to the assembly-level model of a non-trivial concurrent program. Joint work with Robert Sison.

Lundi 13 janvier, 14h en salle Markov

Francois Laroussinie

From Quantified CTL to QBF

QCTL extends the temporal logic CTL with quantifications over atomic propositions. This extension is known to be very expressive (it is as expressive as \MSO). In this work, we consider the structure semantics for the quantifications: the extra propositions label the Kripke structure (and not its execution tree). In this case, the model-checking problem is known to be PSPACE-complete. We propose a model-checking algorithm for QCTL based on a reduction to QBF. We consider several reduction strategies, and we compare them with a prototype (based on different QBF solvers) on several examples. [joint work with Akash Hossain. A preliminary version has been presented at TIME 2019]

Jeudi 16 janvier, 14h en salle Aurigny

Joao (Marques-Silva) (ANITI, Univ. Toulouse)

Automated Reasoning for Explainable AI

This talk provides an overview of our recent efforts on exploiting automating reasoning tools, including SAT, SMT and ILP solvers, for computing explanations of non-interpretable (black-box) ML models and for assessing heuristic explanation approaches. Concretely, the talk will detail the computation of rigorous explanations of black-box models. In addition, the talk will investigate the quality of widely used approaches for computing heuristic explanations. Moreover, the talk summarizes our recent effort on understanding the relationship between rigorous explanations and adversarial examples using duality.

Vendredi 31 janvier, 14h en salle Markov

Pierre Ohlmann

Controlling a random population

Bertrand et al. (2017) introduced a model of parameterised systems, where each agent is represented by a finite state system, and studied the following control problem: for any number of agents, does there exist a controller able to bring all agents to a target state? They showed that the problem is decidable and EXPTIME-complete in the adversarial setting, and posed as an open problem the stochastic setting, where the agent is represented by a Markov decision process. In this paper, we show that the stochastic control problem is decidable. Our solution makes significant uses of well quasi orders, of the max-flow min- cut theorem, and of the theory of regular cost functions.

Jeudi 6 février, 14h en salle Aurigny

Stéphane Le Roux

TBA

TBA

Vos propositions sont les bienvenues !