Monday September 25th 2023 (1pm): Dylan Marinho (Université de Lorraine 🇫🇷)
Location: room A008
Title: Theoretical and algorithmic contributions to the analysis of safety and security properties in timed systems under uncertainty
Real-time systems can be used in a wide range of applications, such as transport, telecommunications and industry. However, accidents can happen, and it is necessary to have confidence in these systems in order to avoid them. It is therefore necessary to formally prove that their behavior will comply with a specification. This specification can be of two kinds: with safety properties, showing that the system will always behave as expected, and security properties, showing that it will be resistant to certain attacks. For this, the formalism of timed automata (TAs) is fairly common.
Thursday September 5th 2023 (1pm): Ghilain Bergeron (Université de Lorraine 🇫🇷)
Location: room B013 (Bob)
Title: Formalisation d’un framework de splitting en Isabelle/HOL
Les calculs de démonstration de théorèmes par saturation (comme la résolution ou la superposition) sont des techniques utilisées dans de nombreux démonstrateurs de théorèmes. Cependant, ceux-ci ont notamment comme inconvénient de générer de très longues preuves et de devoir traiter un nombre grandissant de clauses (ralentissant ainsi le procédé). Le splitting est une technique qui augmente un calcul par saturation. Il permet de mitiger la baisse de performances en cassant certaines clauses en de plus petites clauses indépendantes. Cela réduit le nombre de clauses à traiter dans chaque branche ainsi que leurs tailles. Mon travail a été de formaliser le splitting tel que défini dans le splitting framework  à l’aide de l’assistant de preuve Isabelle/HOL. J’ai ainsi vérifié certaines propriétés importantes du splitting telles que la complétude réfutationnelle et j’ai travaillé sur une instance du splitting construite sur le calcul de résolution, ce qui m’a ammené à m’intéresser à la formalisation de la compacité de la logique du premier ordre.
 Gabriel Ebner, Jasmin Blanchette, and Sophie Tourret. A unifying splitting framework. In Platzer, A., Sutcliffe, G. (eds.) 28th International Conference on Automated Deduction (CADE-28), LNCS 12699, pp. 344–360, Springer, 2021. https://matryoshka-project.github.io/pubs/splitting_paper.pdf
Thursday July 13th 2023 (1pm): Isaline Plaid (ENS de Lyon 🇫🇷)
Location: room B013 (Bob)
Title: Optimising Costs in Stochastic Diagnosis
Diagnosis of partially observable stochastic systems prone to faults was introduced in the late nineties. In this context, a system is represented by a stochastic model (such as a labelled Markov chain) where a fault might occur (a special unobservable event f). The goal of diagnosis is, through the observation of runs of the system, detect whether the fault occur. A large literatture exists around diagnosis, presenting multiple definitions of when a fault can be detected for instance. During this presentation, I will explain some of those notions as well as means to achieve diagnosis while reducing some costs for the users (such as the number of sensors needed to observe the system).
Monday June 26th 2023 (1pm): Sophie Tourret (Université de Lorraine 🇫🇷)
Location: room B013 (Bob)
Title: Verified Given Clause Procedures
Resolution and superpostion provers rely on the given clause procedure to saturate the clause set. Using Isabelle/HOL, we formally verify four variants of the procedure: the well-known Otter and DISCOUNT loops as well as the lesser-known iProver and Zipperposition loops. For each of the variants, we show that given a fair data structure to store the formulas that wait to be selected, the procedure guarantees saturation. Our formalization of the Zipperposition loop clarifies some fine points previously misunderstood in the literature.
Tuesday May 24th 2023 (1pm): Rosalie Defourné (Université de Lorraine 🇫🇷)
Location: room Alice
Title: Encoding TLA+ Proof Obligations Safely for SMT
The TLA+ Proof System (TLAPS) is an interactive proof assistant supported by automated provers, including SMT solvers. TLA+ is an expressive language based on unsorted set theory, which makes the task of encoding it efficiently challenging. An SMT encoding combining type inference with rewriting techniques was implemented, but it was recently shown to contain bugs. To better ensure the soundness of TLAPS, we reimplemented a simpler version of that encoding. This new version is entirely based on an SMT axiomatization of TLA+ with E-matching patterns, also known as triggers. Surprisingly, we found that a large set of TLA+ obligations could be handled by SMT with suitable triggers. The two encodings lead to similar results in terms of how many obligations they can solve, but our version is less likely to fail before the encoding gives a result.
Tuesday May 9th 2023 (1pm): Bruno Andreotti (Universidade Federal de Minas Gerais 🇧🇷)
Location: room Alice
Proofs from SMT solvers ensure correctness independently from implementation, which is often a requirement when solvers are used in safety-critical applications or proof assistants. Alethe is an established SMT proof format generated by the solvers veriT and cvc5, with reconstruction support in the proof assistants Isabelle/HOL and Coq. The format is close to SMT-LIB and allows both coarse- and fine-grained steps, facilitating proof production. However, it lacks a stand-alone checker, which harms its usability and hinders its adoption. Moreover, the coarse-grained steps can be too expensive to check and lead to verification failures. We present Carcara, an independent proof checker and elaborator for Alethe, implemented in Rust. It aims to
increase the adoption of the format by providing push-button proof-checking for Alethe proofs, focusing on efficiency and usability; and by providing elaboration for coarse-grained steps into fine-grained ones, increasing the potential success rate of checking Alethe proofs in performance-critical validators, such as proof assistants. We evaluate Carcara over a large set of Alethe proofs generated from SMT-LIB problems and show that it has good performance and its elaboration techniques can make proofs easier to check.
Tuesday 21st March 2023 (1pm): Stephan Merz (Université de Lorraine 🇫🇷)
Title: Towards an Automatic Proof of the Bakery Algorithm (joint work with Aman Goel and Karem Sakallah)
The Bakery algorithm is a landmark algorithm for ensuring mutual exclusion among N processes that communicate via shared variables. Starting from existing TLA+ specifications, we use the recently-developed IC3PO parameterized model checker to automatically compute inductive invariants for two versions of the algorithm. We compare the machine-generated invariants with human-written invariants that were used in an interactive correctness proof checked by the TLA+ Proof System. The similarity between these two sets of invariants suggests that automated invariant inference is becoming a viable alternative to labor-intensive human written proofs.
Tuesday 6th December 2022 (1pm): Marian Ileana (University of Pitesti, Romania)
Title: Testing specified program systems by finite state machine
Finite State Machine (FSM) are frequently used to model systems in various fields, such as the field of sequential circuits, some types of programs (in lexical analysis, pattern matching, etc.) and communication protocols. The need for system reliability pushes the research of the problem further for testing finite state machines to cover their correct functionality and to distinguish elements of their behavior.
The use of Finite State Machine to model software behavior is practical. I will describe several methods for deriving tests from the FSM. As a case study, I will show how to represent Web applications using FSM.
Friday 2nd December 2022 (4pm): Katherine Kosaian (Carnegie-Mellon University, U.S.A.)
Title: Formalizing Algorithms for Real Quantifier Elimination
Real arithmetic questions involving the “there exists” and “for all” quantifiers arise in various fields, including formalized mathematics, rigorous engineering domains, and life sciences. Although Tarski proved that real quantified statements can always be reduced to logically equivalent quantifier-free statements through quantifier elimination (QE), QE algorithms are notoriously complicated. This makes QE algorithms difficult to formally verify – formally verified algorithms require accompanying proofs of correctness (typically developed in theorem provers) that rely only on a set of trusted logical axioms –and so in practice, QE problems must be solved with unverified software. This is undesirable given the subtlety of QE algorithms and the safety-critical nature of their applications. In recent work, my collaborators and I found that some of the existing unverified QE tools are self-contradictory on (in total) 137 benchmarks, which underscores the need for more support for practical formally verified QE.
My proposed approach is twofold: First, verify a general-purpose multivariate quantifier elimination algorithm based on the Ben-Or, Kozen, and Reif (BKR) algorithm and its variant by Renegar – to fit in a potential “sweet spot” in between practicality of use and algorithmic complexity. Second, augment BKR with strong additional methods and preprocessing methods, including virtual substitution (an extremely practical QE method for QE problems that involve low-degree polynomials). This talk discusses progress towards this ambitious goal, which includes verifying, in the theorem prover Isabelle/HOL, linear and quadratic virtual substitution, univariate BKR, and a naive multivariate quantifier elimination algorithm that can serve as a stepping-stone to multivariate BKR (in joint work).
Tuesday 29th November 2022 (1pm): Victor Roussanaly (University of Lorraine, France)
Title: Decentralised Runtime Verification for Timed Properties
Ensuring the correctness of distributed cyber-physical systems can be done at runtime by monitoring properties over their behaviour. In a decentralised setting, such behaviour consists of multiple local traces, each offering an incomplete view of the system events to the local monitors, as opposed to the standard centralised setting with a unique global trace. While there exists methods to achieve this decentralised monitoring on partial observations, they usually require the assumptions of synchronous communications.
In this talk, we introduce several approach to monitor the behaviour of the system in a decentralised asynchronous system. In this context, timed properties tend to emerge due to the need to synchronise partial observations. This leads us to consider timed properties, focusing primarly on timed regular expressions for our benchmarks, although the methods introduced can be applied to other formalisms.
Tuesday 12th July 2022 (4pm): Hao Wu (Maynooth University, Ireland 🇮🇪)
Title: Cyclone: A New Specification Language for Verifying Graph-based Structures
In this talk, I will briefly introduce Cyclone a new specification language that can be used for verifying graph-based structures. Many interesting and challenging problems can be simply reduced to graphs. Graphs are simple and elegant structures and they can be abstractly used for representing many complex tasks such as verification and testing. In this seminar, I will informally present Cyclone that is a graph-based language and demonstrate some of its features through interesting problems. This is a joint work between Maynooth University and University of Lorraine under 2019 Ulysses scheme, which our initial idea is to design a framework for verifying and testing cyber physical systems. However, as the development continues, we felt that Cyclone could be extended to a much more general verification tool
Tuesday 12th July 2022 (11am): Adel Bouhoula (Arabian Gulf University de Bahreïn 🇧🇭)
Title: Proof by Induction and Computer Security Applications
In this talk, we will present an overview of proof by induction techniques and an introduction to our recent research studies regarding computer security applications such as the verification of security protocols, and the detection and resolution of anomalies in firewall configurations.
Friday 24th June 2022 (10am): James Ortiz (Université de Namur 🇧🇪)
Title: An Alternative (Multi-timed) Semantics for Modelling the Behaviour of Distributed Timed Systems
Distributed Timed Systems (DTS) can be characterized by several communicating components whose behaviour depends on many timing constraints, and such component can be located at several computers spread over a communication network. Distributed Timed Automata (DTA) and Timed Automata with In dependent Clocks (icTA) were introduced to model DTS. They are a variant of Timed Automata (TA) with local clocks that may not run at the same rate. Model checking is a popular technique for automatic formal verification of untimed as well as timed systems. Unfortunately, this technique suffers from the well-known explosion problem: it becomes increasingly difficult to explore exhaustively the whole state space as the system grows, and this problem is exacerbated with the presence of clocks. To handle this problem, many techniques have emerged in recent years, among which bisimulation is popular. Timed bisimulation has already been proven to be decidable for TA. In this talk, I will show our alternative semantics (Multi-timed Automata (MTA)), which is an extension of TA and icTA, whose execution traces can be modelled as sequences of pairs, where each pair contains an action and a tuple of timestamps. Thus, each action has its own tuple of the local time of occurrence for each component that belongs to the modelling DTS. Then, we have extended the theory of Timed Labelled Transition Systems (TLTS) to Multi-Timed Labelled Transition Systems (MLTS) and relate it through our alternative semantics for MTA. Also, we have revisited the notion of timed bisimulation on those automata, resulting in multi-timed bisimulation. We have proved its decidability and presented an EXPTIME algorithm for deciding whether two MTA are multi-timed bisimilar.
Tuesday 7th June 2022 (1.30pm): Bineet Ghosh (University of North Carolina at Chapel Hill 🇺🇸)
Monitoring the correctness of distributed cyber-physical systems is essential.
We address the analysis of the log of a black-box cyber-physical system.
Detecting possible safety violations can be hard when some samples are uncertain or missing.
In this work, the log is made of values known with some uncertainty; in addition, we make use of an over-approximated yet expressive model, given by a non-linear extension of dynamical systems.
Given an offline log, our approach is able to monitor the log against safety specifications with a limited number of false alarms.
As a second contribution, we show that our approach can be used online to minimize the number of sample triggers, with the aim at energetic efficiency.
We apply our approach to two benchmarks, an anesthesia model and an adaptive cruise controller.
Tuesday 31st May 2022 (1pm): Louis Penet de Monterno (École Polytechnique 🇫🇷)
Location: Bob (B013)
Title: Self-Stabilizing Clock Synchronization in Dynamic Networks
We consider the fundamental problem of clock synchronization in a synchronous multi-agent system.
Each agent holds a clock with an arbitrary initial value, and clocks must eventually indicate the same value.
Previous algorithms worked in static networks with drastic connectivity properties and assumed that global information is available. We present different solutions for time-varying topologies that require neither strong connectivity nor any global knowledge on the network.
First, we study the case of unbounded clocks, and propose a self-stabilizing MinMax algorithm
that works if, in each sufficiently long but bounded period of time, there is an agent, called a root,
that can send messages, possibly indirectly, to all other agents.
Such networks are highly dynamic in the sense that roots may change arbitrarily over time.
Moreover, the bound on the time required for achieving this rootedness property is unknown to the agents.
We then present a finite-state algorithm that synchronizes periodic clocks in dynamic networks that are
strongly connected over bounded periods of time.
Here also, the bound on the time for achieving strong connectivity exists, but is not supposed to be known.
Interestingly, it unifies several seemingly different algorithms proposed previously for static networks.
Next, we show that strong connectivity is actually not required: our algorithm still works when the network
is just rooted over bounded period of time with a set of roots that becomes stable.
Finally, we study the time and space complexities of our algorithms, and discuss how initial timing information
allows for much more efficient solutions.
Joint work with Bernadette Charron-Bost, submitted to DISC 2022.
Tuesday 24th May 2022 (1pm): Étienne André (Université de Lorraine 🇫🇷)
Title: Exemplifying parametric timed specifications over signals with bounded behavior
Specifying properties can be challenging work. Here, we propose an automated approach to exemplify properties given in the form of automata extended with timing constraints and timing parameters, and that can also encode constraints over real-valued signals.
That is, given such a property and given an admissible automaton for each signal, we output concrete runs exemplifying real (or impossible) runs for this property.
Specifically, our method takes as input a property, and a set of admissible behaviors, all given as a subclass of linear hybrid automata, namely timed automata extended with arbitrary clock rates and timing parameters.
Our method then generates concrete runs exemplifying the property.
Joint work with Masaki Waga, Ichiro Hasuo and Natsuki Urabe to be presented at Nasa Formal Methods 2022.
Tuesday 1st March 2022 (1pm): Johan Arcile (Université de Lorraine 🇫🇷)
Location: C005 Philippe Flajolet (salle du conseil)
Title: Extrapolations de zone dans les automates temporisés paramétrés
Les automates temporisés (TAs) sont un formalisme efficace pour modéliser et vérifier des systèmes à contraintes temporelles bien définies.
L’extrapolation de zone, l’une des diverses abstractions sur l’espace d’états de ces modèles, est au cœur de leur efficacité.
Alors que les TAs supposent des contraintes temporelles précises, les TAs paramétrés (PTAs) lèvent cette limite et permettent une meilleure expressivité, au prix de l’indécidabilité de nombreuses propriétés.
Je présenterai les problèmes que pose l’extension de l’extrapolation de zone aux PTAs, et comment y faire face.
Tuesday 22nd February 2022 (1pm): Alexander Demin (MPI-INF 🇩🇪)
Title: Signature-based Algorithms for Computing Groebner Bases
Groebner bases are the central tool of analyzing systems of polynomial equations. However, Groebner bases computations are often a bottleneck in a variety of algorithms used in Computer Algebra. Approaches for computing Groebner bases have evolved a great deal since the first one was proposed in 1965 by Bruno Buchberger. One of them, Faugère’s F5, an elaborate algorithm requiring close attention both in study and implementation, initiated the area of signature-based Groebner bases methods.
In this talk, I will give the algebraic ground for signature-based Groebner bases algorithms, and present an intuitive perception of the mechanism. Finally, I will discuss the general idea that allows exceptional performance of the signature-based approach.
Tuesday 14th December 2021 (1pm): Michaël Mera (CISPA 🇩🇪)
Title: Structured Fuzzing: Make Fuzzing Great Again?
In the past years fuzzing has been gaining traction in the security community. In this talk we’ll first explore the reasons behind the resurgence of this ancient testing technique but also the shortcomings preventing it to appeal to a wider circle of developers. To address these shortcomings, new techniques based on structured fuzzing are starting to emerge. We’ll discuss how these techniques leverage a given input model to (1) explore a program input space more efficiently, (2) give control over which parts of the program to test and (3) build higher level failure oracles. Finally, I’ll present our newest approach to automatically synthesize high quality input models from a program, significantly lowering the barrier of entry for integrating fuzzing in many different scenarios.
Tuesday 23th November 2021 (1pm): Guillaume Ambal (IRISA, Rennes 🇫🇷)
Title: Certified Abstract Machines for Skeletal Semantics
Skeletal semantics is a recent framework for the formalization of programming languages, and offers tools to manipulate them. To cover more use cases, we introduce two new meanings of skeletal semantics, in the form of non-deterministic and deterministic abstract machines. The work is formalized in Coq and extracted to OCaml. This results in a certified interpreter for any language defined in skeletal semantics
Tuesday 2nd November 2021 (1pm): Sergueï Lenglet (Université de Lorraine 🇫🇷)
Title: Non-Deterministic Abstract Machines
Abstract machines are a form of semantics closer to the implementation than the usual reduction semantics or Structural Operational Semantics. While abstract machines are well-studied for deterministic languages and can be derived from other semantics, they are usually ad-hoc and incomplete for non-deterministic languages. We propose a generic design of non-deterministic abstract machines which can be derived from an intermediate format called zipper semantics.
Location: LORIA (Salle Bob)
Title: What’s new in proofs from SMT solvers?
If an SMT solver determines that a given problem is unsatisfiable, it might generate a formal proof. Unfortunately, the current state of SMT-generated proofs is not satisfying: no two solvers use the same proof format, and the generated proofs are not widely used. In this talk I will present our recent effort to improve this situation. On the one hand, we developed a solid reconstructions of the proofs generated by veriT into Isabelle/HOL. This improved the success rate of the Sledgehammer proof-search tool. On the other hand, we are now in the process of defining a solver-independent proof format called Alethe.
Tuesday 21st September 2021 (1pm): Sophie Tourret (Inria 🇫🇷)
Location: LORIA (Salle A008)
Title: On what is wrong with higher-order SMT and what we are doing to fix it
SMT solvers have been extended to deal with higher-order problems just a few years ago . However, their performances are limited in this new domain, because only the ground SMT module has been extended.
This talk presents ongoing work about extending one of the most effective SMT instantiation technique, namely CCFV , to lambda-free HOL, as a first step to full HOL SMT instantiation. Surprisingly, moving to lambda-free HOL allows us to encode the problem as a propositional formula, such that its models correspond to instances we need. I will explain how this is done.
 Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, Clark W. Barrett: Extending SMT Solvers to Higher-Order Logic. CADE 2019: 35-54
 Haniel Barbosa, Pascal Fontaine, Andrew Reynolds: Congruence Closure with Free Variables. TACAS (2) 2017: 214-230
Friday 25th June 2021 (12.45pm): Sorin Stratulat (Université de Lorraine 🇫🇷)
Location: C005 / virtual
Title: Noetherian Induction for Computer-Assisted First-Order Reasoning
Noetherian induction is one of the most general induction principles used in formal reasoning. In the frame of the first-order reasoning, we propose a classification of its instances that can be split into term- and formula-based instances. We give an overview of the term- and formula-based Noetherian induction reasoning, and established relations between them. We show that every term-based Noetherian induction proof can be converted to a formula-based one. The question about the conversion in the other direction remains open. However, we identify certain classes of formula-based Noetherian induction proofs that can be translated into term-based ones. We establish connections between formula-based Noetherian reasoning and other kinds of first-order reasoning, as the cyclic induction reasoning for first-order logic with inductive definitions (FOLID) and saturation-based reasoning. Last but not least, we have devised methodologies for certifying formula-based Noetherian induction proofs and FOLID cyclic proofs using the Coq proof assistant.
This is an HDR defense rehearsal.
Friday 18th June 2021 (1pm): Étienne André (Université de Lorraine 🇫🇷)
Title: IMITATOR 3: Synthesis of timing parameters beyond decidability
Real-time systems are notoriously hard to verify due to nondeterminism, concurrency and timing constraints.
When timing constants are uncertain (in early the design phase, or due to slight variations of the timing bounds), timed model checking techniques are often not satisfactory. In contrast, parametric model checking synthesizes timing values ensuring correctness. IMITATOR takes as input an extension of parametric timed automata (PTAs), a powerful formalism to formally verify critical real-time systems. IMITATOR extends PTAs with stopwatches, multi-rate clocks, global rational-valued variables and a set of additional useful features. We describe here the features offered by IMITATOR 3, that moved along the years from a simple prototype dedicated to robustness analysis to a standalone parametric model checker for timed systems.
Paper accepted at CAV 2021.
Friday 11th June 2021 (1pm): Dylan Marinho (Université de Lorraine 🇫🇷)
Title: A Benchmarks Library for Extended Parametric Timed Automata [slides]
Parametric timed automata are a powerful formalism for reasoning on concurrent real-time systems with unknown or uncertain timing constants. In order to test the efficiency of new algorithms, a fair set of benchmarks is required. We present an extension of the IMITATOR benchmarks library, that accumulated over the years a number of case studies from academic and industrial contexts. We extend here the library with several dozens of new benchmarks; these benchmarks highlight several new features: liveness properties, extensions of (parametric) timed automata (including stopwatches or multi-rate clocks), and unsolvable toy benchmarks. These latter additions help to emphasize the limits of state-of-the-art parameter synthesis techniques, with the hope to develop new dedicated algorithms in the future.
Paper accepted at TAP 2021 with Étienne André and Jaco Van de Pol.
Friday 30th April 2021 (1pm): Ioannis Filippidis (Université de Lorraine 🇫🇷)
Title: Reasoning about the TLA+ operators ENABLED and … within TLAPS
TLA+ is a language for writing system specifications, and mathematics in general. The TLA+ proof system, TLAPS, is a program that checks proofs of theorems written in TLA+. ENABLED and … are TLA+ operators, and this presentation will describe the new reasoning capabilities of TLAPS for these operators. The main motivation for reasoning about the operator ENABLED is proving liveness properties of systems. A system’s specification usually includes weak fairness formulas, which are defined using ENABLED, and from the safety and fairness formulas that specify the system, the desired liveness properties can be proved. Liveness properties are useful because they can express that a system eventually responds to each input it receives, that an algorithm terminates, in the sense of reaching a state that can be regarded as having completed a computation, that a vehicle reaches its destination, and that an unstuck process progresses, among other properties. This presentation will summarize relevant notions from TLA+, including what it means to prove correctness of a system. The reasoning approaches that have been implemented will be described with examples that show how to use them. These approaches are a translation to quantification, automated expansion of defined operators to ensure soundness, and the application of axioms and proof rules about ENABLED. How basic TLA+ proofs are written will also be discussed.
Friday 26th March 2021 (1pm): Sébastien Bouchard
Title: Verification of Distributed Systems Composed of Mobile Agents
Mobile agents are theoretical entities able to perform computations, execute an algorithm, observe their environment, and move in it. The main tasks involving such agents considered in the literature are gathering and treasure hunt. The former one consists in bringing the mobile agents together, while the latter one consists in finding some idle target.
During the presentation, I will briefly introduce some of my contributions related to these tasks as an introduction for the project which motivates my application to your team, that is verifying such distributed systems. Then, I will present the first steps I have taken in this direction.
Friday 19th March 2021 (1pm): Guillaume Dupont (IRIT 🇫🇷)
Title: Correct-by-construction design of hybrid systems based on refinement and proof
Hybrid systems integrate simultaneously discrete behaviours (algorithms) and continuous behaviours (physical phenomena). Such systems being very adaptable and diverse, they started being quite common in our everyday life, from smart light bulbs to more complex products, including safety critical systems such as autonomous cars or airplanes.
Due to their hybrid nature, hybrid systems are especially hard to verify. Their discrete part may be handled using “traditional” formal methods, and their continuous part is the subject of control theory; but the integration of both these aspects at the same level in the designing and verifying process is still an important challenge of the domain.
In the context of our work, we propose a formal framework for the correct-by-construction design of hybrid systems. This framework is based on the Event-B formal method, and in particular its associated extension mechanism and refinement operation. It provides a number of reusable and generic formal design patterns, that may be used in order to design any hybrid system in an incremental way. This framework is also the support of a generic method for the formal design of hybrid systems, which we demonstrate the use of on various case studies.
Friday 12th March 2021 (1pm): Miriam García Soto (IST Austria 🇦🇹)
Title: Design, Verification and Synthesis of Hybrid Systems [slides]
We have witnessed an increasing interest and investment in safe autonomous systems such as self-driving vehicles, robots and medical devices. Critical aspects to be considered in the design of these complex systems are security, reliability and safety. For instance, a single design bug can wreak havoc across thousand of deployed devices. The prevention of such occurrences requires the use of a rigorous methodology to validate and verify pivotal properties in autonomous systems.
Current approaches to verify and validate software and systems rely mainly on testing and simulation. These solutions encounter in general two problems, they are not cost-efficient and do not provide a correctness certificate for the system performance. To design high-confidence systems, solid modelling formalisms along with verification and validate algorithms have been developed in the field of computer science. These techniques fall into the discipline known as “formal methods”, which has its foundations in rigorous mathematical modelling and analysis.
The broad goal of my research is to design and analyse real-world autonomous systems, by developing cost-efficient formal approaches which provide correctness certificates. Concretely, this talk will introduce some of the algorithmic techniques I have developed so far, such as (1) a Counterexample Guided Abstraction Refinement (CEGAR) approach for stability verification of hybrid systems, (2) a stabilizing controller synthesis of hybrid systems, and (3) techniques for the data-based synthesis of hybrid automata.
Friday 5th March 2021 (1pm): Simon Robillard (IMT Atlantique 🇫🇷)
Title: Automated Planning for Distributed System Reconfigurations With a SMT Solver
Large distributed systems with an emphasis on adaptability are now considered a necessity in many domains, yet reconfiguration of these systems is still largely carried out in an ad hoc fashion, a process that is both inefficient and error-prone. This presentation will discuss a SMT-based technique to solve the planification problem for the reconfiguration of distributed systems in a component-based model. Specifically, given some tasks to execute and a desired final state of the system, we will show how to compute a reconfiguration plan that guarantees satisfaction of inter-component dependencies and is also optimized for parallel execution.
Friday 5th February 2021 (1pm): Mohammed Foughali (Université Grenoble-Alpes 🇫🇷)
Title: On the formal verification of safety-critical systems: challenges, approaches and perspectives [slides]
Safety-critical applications, e.g. those stemming from robotic, autonomous and cyber-physical systems, must be formally verified against crucial behavioral and timed properties. Yet, the use of formal verification techniques in such context faces a number of challenges, such as the absence of formal foundations of robotic frameworks and the lack of scalability of exhaustive verification techniques. In this talk, I will explore the approaches I have been proposing for the last six years to tackle these challenges, based on a global vision that favors correctness, user-friendliness and scalability of formal methods vis-à-vis real-world robotic and autonomous systems deployed on embedded platforms. I will discuss a major part of my work where safety-critical specifications are automatically translated into strictly equivalent formal models on which model checking, but also scalable non exhaustive techniques such as statistical model checking and runtime verification, may be used by practitioners to gain a considerable amount of trust in their underlying applications. Further, I will present a couple of techniques that allow to take into account hardware and OS specificities in the verification process, such as the scheduling policy and the number of processor cores provided by the platform, and thus increase the meaningfulness of the verification results. I will conclude with possible future research directions within the broad objective of deploying trustable safety-critical systems through bridging the gap between the software engineering, robotics, formal methods and real-time systems communities.
Friday 22nd January 2021 (1pm): Nicolas Schnepf (Aalborg Universitet 🇩🇰)
Title: Vérification formelle de systèmes distribués et de leurs propriétés réseau
Abstract: La présentation couvre à la fois les travaux de thèse sur l’orchestration et la vérification de fonctions de sécurité et ceux de recherche post-doctorale sur le routage résiliant contraint par les capacités. En fin d’exposé, quelques défis et pistes de recherche future seront esquissés.
(talk in French)
Friday 8th January 2021 (1pm): Mathieu Montin (Université de Lorraine 🇫🇷)
Title: An Agda tutorial : language and development environment
Agda is a fully functionally, dependently typed language developed in the late 2000s by Ulf Norell in his PhD thesis. While the language was originally directed towards programming and treated dependent types as a mean to perfect this activity, it quickly became apparent that Agda could equally be used as a proof assistant by exploiting the well known Curry-Howard correspondence. Agda comes with several convenient features which makes programming and verifying using the language both powerful and satisfying, which this introduction aims at demonstrating. From the definition of basic data types to more advanced predicates, we will explore the possibilities of the language as well as the automation and help the tools around it provide through the programming effort.
Friday 18th December 2020 (1pm): Bineet Ghosh (University of North Carolina at Chapel Hill 🇺🇸)
Title: Robust Intelligent Systems [slides]
Formal analysis of dynamical systems, such as autonomous vehicles, drones, spacecrafts, medical devices etc., often assumes that the model is perfectly known. But in reality, this is seldom the case. A dynamical system model is dependent on a lot of parameters, for instance, consider the model of an adaptive cruise controller (ACC), the model is dependent on parameters like the mass of the car, acceleration of the lead vehicle etc. These parameters are measured by sensors, whose accuracy is not perfect, but gives a value with some error tolerance. Such examples are plenty in medical devices: an anesthesia delivery model is dependent on a lot of parameters, that are often measured empirically. Therefore, analysis assuming a perfectly known model is often useless in practice.
In a safety critical scenario, analysis without considering uncertainties can result in fatal mistakes. In my research, I have worked on several methods to perform safety analysis of such systems by computing reachable sets that accounts for uncertainties. I’m also currently working on offloading algorithms that automatically switch to safety verification methods with varying cost and accuracy based on the scenario, with formal guarantees. Also, implementing them in real embedded system platforms, considering the computation and energy availability constraints. In the rest of the talk I’ll briefly introduce the techniques that I have developed.
Friday 11th December 2020 (1pm): Jawher Jerray (Université Sorbonne Paris Nord 🇫🇷)
Title: Generation of bounded invariants via stroboscopic set-valued maps: Application to the stability analysis of parametric time-periodic systems [slides]
In this talk, we present a method that generates a bounded invariant of a differential system with a given set of initial conditions around a point x0.
This invariant has the form of a tube centered on the Euler approximate solution starting at x0, which has for radius an upper bound on the distance between the approximate solution and the exact ones.
The method consists in finding a real T>0 such that the /snapshot/ of the tube at time t=(i+1)T is included in the snapshot at t=iT, for some integer i.
A simple additional condition is also given to ensure that the solutions of the system can never converge to a point of equilibrium. In dimension 2, this ensures that all solutions converge towards a limit cycle.
The method is extended in case the dynamic system contains a parameter p, thus allowing the stability analysis of the system for a range of values of p.
We applied this method on a generic proof of the convergence of the Van der Pol system towards a limit cycle with a real parameter μ ∈ [0.2, 2.2].
Friday 4th December 2020 (1pm): Engel Lefaucheux (MPI Saarbrücken 🇩🇪)
Title: On Information Control in Probabilistic Systems: a closer look on Opacity and Diagnosis [slides]
The control of the information given by a system has recently seen increasing importance due to the omnipresence of communicating systems, the need for privacy, etc.
This control can be used in order to disclose to an observer an information of the system, or, oppositely, to hide one.
In this talk, I will consider the control of the information released by a system represented by a stochastic model such as a Markov chain.
Here, an external observer is interested in detecting a particular set of relevant paths of the system.
However, he can only observe those paths through an observation function which obfuscates the real behaviour of the system.
Exact disclosure of the information occurs when the observer can deduce from a finite
observation that the path is relevant, the approximate disclosure variant corresponding to the path being identified as relevant with high accuracy.
I will discuss the problems of diagnosability and opacity, which corresponds, in spirit, to the cases where one wants to disclose all the information or hide as much of it as possible with a focus on the approximate notion of disclosure.
Friday 27th November 2020 (1pm): Guillaume Ambal (Université de Rennes 1 🇫🇷)
Title: From Big-Step to Small-Step Skeletal Semantics
Friday 13th November 2020 (1pm): Mathieu Montin (Université de Lorraine 🇫🇷)
Cyber physical systems (CPS) are usually complex systems which are often critical,meaning their failure can have significant negative impacts on human lives. A key point in their development is the verification and validation (V & V) activities which are used to assess their correctness towards user requirements and the associated specifications. This process aims at avoiding failure cases, thus preventing any incident or accident. In order to conduct these V & V steps on such complex systems, separations of concerns of various nature are used. In that purpose, the system is modelled using heterogeneous models that have to be combined together. The nature of these separations of concerns can be as follows: horizontal, which corresponds to a structural decomposition of the system; vertical, which corresponds to the different steps leading from the abstract specification to the concrete implementation; and transversal, which consists in gathering together the parts that are thematically identical (function, performance, security, safety…). These parts are usually expressed using domain specific modelling languages (DSML), while the V & V activities are historically conducted using testing and proofreading, and more and more often, using formal methods, which is advocated in our approach. In all these cases, the V & V activities must take into account these separations in order to provide confidence in the global system from the confidence of its sub-parts bound to the separation in question. In other words, to ensure the correctness of the system, a behavioural semantics is needed which has to rely on the ad-hoc semantics of the subsystems. In order to define it, these semantics must be successfully combined in a single formalism. This thesis stems from the GEMOC project: a workbench that allows the definition of various languages along with their coordination properties, and target the formal modelling of the GEMOC core through the association of trace semantics to each preoccupation and the expression of constraints between them to encode the correct behaviour of the system. This thesis follows several other works conducted under the TOPCASED, OPEES, QUARTFT}, P and GEMOC projects, and provides four contributions in that global context: the first one proposes a methodology to give an operational semantics to executable models illustrated through two case studies: PetriNets and SimplePDL. The second one proposes a formal context on which refinement can be expressed to tackle vertical separation. The third one gives a denotational semantics to CCSL, which is the language that is currently used in the GEMOC projects to express behavioural properties between events from one or several models, possibly heterogeneous. Finally, the fourth one proposes an investigation on how to extend CCSL with the notion of refinement we proposed. All these contribution are mechanized in the AGDA proof assistant, and thus have been modelled and proven in a formal manner.
Friday 23rd October 2020 (1pm): Dylan Marinho (Université de Lorraine 🇫🇷)
Title: Defeating Opaque Predicate using Binary Analysis and Machine Learning
Program obfuscation, since it permits to prevent reverse engineering analysis while preserving a same behavior, is nowadays introduced as a method to protect a software, particularly for intellectual property matters. However, this tool is also used by malware designer in order to bypass investigations and be able to propagate itself.
Therefore, obfuscation is a scientific problem that occurs since that we try to analysis this kind of programs. De-obfuscation methods were introduced, but still remain insufficient. The main goal of this work was to introduce a method, combining binary analysis and machine learning, to detect an obfuscation by “opaque predicates”.
Friday 16th October 2020 (1pm): Johan Arcile (Université de Lorraine 🇫🇷)
Title: Modeling and formal verification of a communicating autonomous vehicle system [slides]
A system of autonomous vehicles consists of several agents individually making decisions in real time while exchanging information with other agents nearby.
The validation of formal logic properties in such systems is not possible through naive approaches, due to the large number of variables involved in their representation.
The two complementary works that will be presented have been developed to address this issue:
-The VerifCar software framework, dedicated to decision-making analysis of communicating autonomous vehicles, which uses the state-of-art tool Uppaal.
-The formalism of MAPTs and its dedicated exploration algorithms, allowing the use of heuristics that reduces the computation time needed to address reachability problems.
Friday 31st January 2020 (11am): Étienne André (Université de Lorraine 🇫🇷)
Title: Parametric Timed Model Checking for Guaranteeing Timed Opacity
Information leakage can have dramatic consequences on systems security. Among harmful information leaks, the timing information leakage is the ability for an attacker to deduce internal information depending on the system execution time.
We address the following problem: given a timed system, synthesize the execution times for which one cannot deduce whether the system performed some secret behavior. We solve this problem in the setting of timed automata (TAs). We first provide a general solution, and then extend the problem to parametric TAs, by synthesizing internal timings making the TA secure. We study decidability, devise algorithms, and show that our method can also apply to program analysis.
This is a joint work with Sun Jun (SMU, Singapore)
Friday 17th January 2020 (11am): Masaki Waga (和賀 正樹) (Tokyo 🇯🇵)
Friday 10th January 2020 (11am): Stephan Merz (Université de Lorraine 🇫🇷)
Title: Auxiliary Variables Revisited
When proving refinement between two specifications, refinement mappings are the standard technique for explaining how the lower-level specification implements the internal state components of the higher-level specification. However, it is well known that refinement mappings by themselves are incomplete, and it has been suggested to augment the lower-level specification by history and prophecy variables in order to obtain a more complete proof method. We introduce new rules for prophecy variables that both yield stronger completeness results and, we believe, are simpler to apply in practice. Our approach is based on two ideas: simple prophecy variables yield one-shot predictions over a finite time horizon, and several such variables can be combined into an array for making prophecies over entire executions.
(joint work with Leslie Lamport)
(Below is just a dummy template for future events.)
Tuesday 16th October 2022 (1pm): TBA (Université de Lorraine 🇫🇷)