VeriDis seminar

Thursday May 14th 2024 (1 PM): Antoine Lejay

Location: Room B013 (BOB)

Title: Apollon : un projet d’humanités numériques

Abstract:

Nous présenterons un projet d’humanités numériques visant à étudier l’ouvrage La Politique d’Aristote par des moyens numériques, afin de constituer un lexique des idées. En particulier, nous nous intéresserons au problème du format des textes, et notamment des difficultés liées aux textes antiques, aux technique de plongement des mots et leurs limitations, ainsi aux questions que nous pouvons nous poser sur la détection de relations et de raisonnement.

Ce projet est porté par Antoine Lejay (Inria), Lionel Lenotre (UHA), Maria-Teresa Schettino (UHA).

Thursday March 21th 2024 (2 PM): Martin Vassor

Location: zoom TBA

Title: Introduction aux types-session, et quelques questions autour de la fiabilité

Abstract:

Les types-session sont une famille de systèmes de types comportementaux servant à caractériser des protocoles de communications dans le cadre de systèmes concurrents par passage de messages. Le but de cette présentation est de présenter cette famille de systèmes de types, puis de voir brièvement comment ils peuvent être utilisés pour:

1. prévenir statiquement certaines classes d’erreurs (e.g. absence de deadlock)

2. détecter, à l’execution des comportements non-voulu (e.g. contenu de messages incohérents)

3. participer à la gestion des erreurs (e.g. reprise sur panne, extinction contrôlée du protocole)

Tuesday March 19th 2024 (1 PM): Philippe de Groote (Université de Lorraine 🇫🇷, Sémagramme group)

Location: room A006

Title: Sémantique des dépendances

Abstract:

Cet exposé jettera les bases d’une théorie permettant de dériver des représentations sémantiques d’énoncés en langue naturelle à partir de leurs analyses en dépendances.

Thursday March 14th 2024 (1 PM): Julie Cailler

Location: https://cnrs.zoom.us/j/98230475220?pwd=UWNENlJPMjl1VzBPU0dCZ2ROa09Zdz09

Titre: Conception d’un prouveur automatique basé sur les tableaux analytiques et production de preuves vérifiables

Abstract:

La déduction automatique est l’utilisation de programmes informatique afin d’automatiquement prouver des théorèmes mathématiques. Elle trouve son intérêt dans la détection de bogues au sein de systèmes critiques ou encore dans l’aide à la démonstration de preuves mathématiques. Cet exposé se concentre sur la présentation de Goéland, un prouveur de théorèmes automatique concurrent, et sur les principaux défis qu’il rencontre. Ces défis incluent l’implémentation d’une procédure de recherche de preuves équitable basée sur la méthode des tableaux en logique du premier ordre, la prise en compte du raisonnement au sein des certaines théories (l’égalité, la théorie des ensembles, etc), ainsi que la génération de preuves vérifiables par des outils externes (Coq, Lambdapi).

Tuesday March 12th 2024 (1 PM): Jawher Jerray

Location: room A006

Titre: Model-based High-level Integration of Heterogeneous Components for co-simulation

Abstract:

Because of their complexity, embedded systems are designed with sub-systems or components taken in charge by different development teams or entities and with different modeling frameworks and simulation tools, depending on the characteristics of each component. Unfortunately, this diversity of tools and semantics makes the integration of these heterogeneous components difficult. Thus, to evaluate their integration before their hardware or software is available, one solution would be to merge them into a common modeling framework. Yet, such a holistic environment supporting many computation and computation semantics seems hard to settle. Another solution we investigate is to generically link their respective simulation environments in order to keep the strength and semantics of each component environment. We present a method to simulate heterogeneous components of embedded systems in real-time. These components can be described at any abstraction level. Our main contribution is a generic glue that can analyze in real-time the state of different simulation environments and accordingly enforce the correct communication semantics between components.

Tuesday March 5th 2024 (1 PM): Claude Stolze

Location: room B013 (Bob)

Title: Composable Partial Multiparty Session Types

Abstract:

We introduce partial sessions and partial (multiparty) session types, in order to deal with open systems, i.e., systems with missing components. Partial sessions can be composed, and the type of the resulting system is derived from those of its components without knowing any suitable global type nor the types of missing parts. We apply these types to a process calculus, for which we prove subject reduction and progress, so that well-typed systems never violate the prescribed constraints. Therefore, partial session types support the development of systems by incremental assembling of components.

Monday February 19th 2024 (1 PM): Laetitia Laversa (LIPN 🇫🇷, LoVe group)

Location: room B013 (Bob)

Title: Communicating automata and k-synchronizability

Abstract:

Distributed systems are ubiquitous and their implementation is complex and error-prone. In order to check for errors, they can be modeled as systems of communicating automata, where each automaton represents the behavior of an element of the system. In general, verification problems are undecidable in such a model. The use of (under or over) approximations is necessary. This talk presents k-synchronizable systems, which are a subclass of systems of communicating automata, and some results on them.

Tuesday February 13th 2024 (1 PM): Steve Kremer (Université de Lorraine 🇫🇷, PESTO group)

Location: room B013 (Bob)

Title: DY Fuzzing: Formal Dolev-Yao Models Meet Cryptographic Protocol Fuzz Testing

Abstract:

Critical and widely used cryptographic protocols have repeatedly been found to contain flaws in their design and their implementation. A prominent class of such vulnerabilities is logical attacks, e.g. attacks that exploit flawed protocol logic. Automated formal verification methods, based on the Dolev-Yao (DY) attacker, formally define and excel at finding such flaws, but operate only on abstract specification models. Fully automated verification of existing protocol implementations is today still out of reach. This leaves open whether such implementations are secure. Unfortunately, this blind spot hides numerous attacks, such as recent logical attacks on widely used TLS implementations introduced by implementation bugs.

We propose a novel and effective technique that we call DY model-guided fuzzing, which precludes logical attacks against protocol implementations. The main idea is to consider as possible test cases the set of abstract DY executions of the DY attacker, and use a novel mutation-based fuzzer to explore this set. The DY fuzzer concretizes each abstract execution to test it on the program under test. This approach enables reasoning at a more structural and security-related level of messages represented as formal terms (e.g. decrypt a message and re-encrypt it with a different key) as opposed to random bit-level modifications that are much less likely to produce relevant logical adversarial behaviors. We implement a full-fledged and modular DY protocol fuzzer and demonstrate its effectiveness by fuzzing three popular TLS implementations, resulting in the discovery of several novel vulnerabilities.

Thursday January 25th 2024 (1 PM): Thomas Bagrel (Université de Lorraine 🇫🇷, VeriDis group)

Location: room B013 (Bob)

Title: Destination-passing style programming: a Haskell implementation

Abstract (from the associated article): 

Destination-passing style programming introduces destinations, which represent the address of a write-once memory cell. Those destinations can be passed as function parameters, and thus enable the caller of a function to keep control over memory management: the body of the called function will just be responsible of filling that memory cell. This is especially useful in functional programming languages, in which the body of a function is typically responsible for allocation of the result value.

Programming with destination in Haskell is an interesting way to improve performance of critical parts of some programs, without sacrificing memory guarantees. Indeed, thanks to a linearly-typed API I present, a write-once memory cell cannot be left uninitialized before being read, and is still disposed of by the garbage collector when it is not in use anymore, eliminating the risk of uninitialized read, memory leak, or double-free errors that can arise when memory is managed manually.

In this article, I present an implementation of destinations for Haskell, which relies on so-called compact regions. I demonstrate, in particular, a simple parser example for which the destination-based version uses 35% less memory and time than its naive counterpart for large inputs.

Tuesday January 23rd 2024 (1 PM): Thomas Lambert (Université de Lorraine 🇫🇷, COAST group)

Location: room B013 (Bob)

Title: Prise de décision dans un monde (informatique) incertain

Abstract: 

Avec la complexification des systèmes informatiques et les échelles de plus en plus élevées sur lesquelles sont effectuées les calculs parallèles ou distribués, il apparait irréaliste d’espérer avoir une connaissance exacte des problèmes traitées et de l’ensemble de leurs paramètres. Dès lors, lorsqu’on traite de problèmes d’ordonnancement et d’optimisation en général, comment peut-on prendre une décision et comment peut-on évaluer la qualité d’un algorithme ? Cette présentation essaye, au travers quelques exemples, d’illustrer un peu ces problèmes et de présenter certaines réponses, incluant le modèle d’algorithme “offline”, la notion d’alpha-compétitivité et l’utilité de lancer des boules dans des urnes pour voir ce qui se passe.

Tuesday December 12th 2023 (1 PM): Guilhem Gamard (Université de Lorraine 🇫🇷, Mocqua group)

Location: room B013 (Bob)

Title: The quest for the Domino Problem

Abstract: 

In the 1960s, Hao Wang was trying to use computers to perform automated checking of logic formulae of a certain kind (AEA formulae). He reduced this task to an “amusing combinatorial problem” which he
endeavored to study:

“Assume we are given a finite set of square plates of the same size with edges colored, each in a different manner. Suppose further there are infinitely many copies of each plate (plate type). We are not permitted to rotate or rotate a plate. The question is to find an effective procedure by which we can decide, for each given set of plates, whether we can cover up the whole plane […] with copies of plates subject to the restriction that adjoining edges must have the same color.”

Wang initially conjectured this “Domino problem” was decidable; his student, Robert Berger, proved that it is not. The study of the Domino problem turned out to have a surprising number of ramifications and connections, notably with symbolic dynamics, computability theory, cellular automata, combinatorics, and geometry.

In this talk we’ll outline the theory of Wang tiles, see why it was reasonable to conjecture decidability of the Domino problem, and one proof (among many) of undecidability.

No background in tiling theory is necessary to follow.

Tuesday December 5th 2023 (1 PM): Gidon Ernst (LMU Munich 🇩🇪)

Location: room B013 (Bob)

Title: Automating software verification with respect to strong specifications

Abstract:

Proving functional correctness of software with respect to specifications of application-specific requirements requires one to define these specifications in the first place, to come up with coupling relations that connect the concrete state space of the implementation to its abstract counterpart, and to prove that this correspondence is maintained by the computation of the system.

In this talk I will sketch ideas how to automate this process. In the main technical part of the talk I will present an approach that quickly and fully automatically discovers (distributive) lemmas typically needed for the core part of the proofs. The approach, called LemmaCalc, leverages well-known transformations, originally conceived for the optimization of functional programs (such as fusion and accumulator removal), to that purpose.

Friday October 27th 2023 (10 AM): Rosalie Defourné (Université de Lorraine 🇫🇷)

Location: room A008

Title: Encoding TLA+’s Set Theory for Automated Theorem Provers

Abstract: 

TLA+ est un langage de spécification combinant la logique temporelle des actions et la théorie des ensembles non typée. L’assistant de preuve TLAPS traite les obligations de preuve de TLA+ et les fait résoudre par des prouveurs automatiques externes. Cette thèse a permis l’élaboration de deux nouveaux encodages de TLA+ : le premier vers la logique d’ordre supérieur (HOL) afin de mieux prendre en charge certaines preuves par induction, le second vers la logique des solveurs SMT. Ce dernier encodage étend des travaux précédents avec des heuristiques d’instantiation (triggers) permettant à SMT de raisonner efficacement sur la théorie des ensembles de TLA+. Ces deux encodages ont été implémentés dans TLAPS, et le prouveur Zipperposition a été intégré comme nouveau backend d’ordre supérieur. Le nouvel encodage SMT est intéressant car son implémentation est plus légère, mais il n’entraîne pas une perte d’efficacité pour autant.

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

Abstract: 

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

Abstract: 

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 [1] à 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.
[1] 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

Abstract: 

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

Abstract:

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

Abstract:  

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

Title: Carcara: An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format

Abstract:

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 🇫🇷)

Location: B013

Title: Towards an Automatic Proof of the Bakery Algorithm (joint work with Aman Goel and Karem Sakallah)

Abstract:

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)

Location: B013

Title: Testing specified program systems by finite state machine

Abstract:

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.)

Location: online

Title: Formalizing Algorithms for Real Quantifier Elimination

Abstract:

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)

Location: B013

Title: Decentralised Runtime Verification for Timed Properties

Abstract:

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 🇮🇪)

Location: virtual

Title: Cyclone: A New Specification Language for Verifying Graph-based Structures

Abstract:

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 🇧🇭)

Location: Bob

Title: Proof by Induction and Computer Security Applications

Abstract:

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 🇧🇪)

Location: Bob

Title: An Alternative (Multi-timed) Semantics for Modelling the Behaviour of Distributed Timed Systems

Abstract:

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 🇺🇸)

Location: virtual

Title: Monitoring of scattered uncertain logs using uncertain linear dynamical systems

Abstract:

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.

Joint work with Étienne André, to be presented at FORTE 2022.

Tuesday 31st May 2022 (1pm): Louis Penet de Monterno (École Polytechnique 🇫🇷)

Location: Bob (B013)

Title: Self-Stabilizing Clock Synchronization in Dynamic Networks

Abstract:

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 🇫🇷)

Location: Bob

Title: Exemplifying parametric timed specifications over signals with bounded behavior

Abstract:

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

Abstract:

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 🇩🇪)

Location: online

Title: Signature-based Algorithms for Computing Groebner Bases

Abstract:

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 🇩🇪)

Location: Bob

Title: Structured Fuzzing: Make Fuzzing Great Again?

Abstract:

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 🇫🇷)

Location: A006

Title: Certified Abstract Machines for Skeletal Semantics

Abstract:

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 🇫🇷)

Location: Bob

Title: Non-Deterministic Abstract Machines

Abstract:

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.

Tuesday 19th October 2021 (1pm): Hans-Jörg Schurr (Université de Lorraine 🇫🇷)

Location: LORIA (Salle Bob)

Title: What’s new in proofs from SMT solvers?

Abstract:

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

Abstract:

SMT solvers have been extended to deal with higher-order problems just a few years ago [1]. 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 [2], 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.

[1] Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, Clark W. Barrett: Extending SMT Solvers to Higher-Order Logic. CADE 2019: 35-54
[2] 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

Abstract:

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 🇫🇷)

Location: virtual

Title: IMITATOR 3: Synthesis of timing parameters beyond decidability

Abstract:

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 🇫🇷)

Location: virtual

Title: A Benchmarks Library for Extended Parametric Timed Automata [slides]

Abstract:

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 🇫🇷)

Location: virtual

Title: Reasoning about the TLA+ operators ENABLED and … within TLAPS

Abstract:

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

Location: virtual

Title: Verification of Distributed Systems Composed of Mobile Agents

Abstract:

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 🇫🇷)

Location: virtual

Title: Correct-by-construction design of hybrid systems based on refinement and proof

Abstract:

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 🇦🇹)

Location: virtual

Title: Design, Verification and Synthesis of Hybrid Systems [slides]

Abstract:

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. 

Friday 5th March 2021 (1pm): Simon Robillard (IMT Atlantique 🇫🇷)

Location: virtual

Title: Automated Planning for Distributed System Reconfigurations With a SMT Solver

Abstract:

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 🇫🇷)

Location: virtual

Title: On the formal verification of safety-critical systems: challenges, approaches and perspectives [slides]

Abstract:

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 🇩🇰)

Location: virtual

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 🇫🇷)

Location: virtual

Title: An Agda tutorial : language and development environment

Abstract:

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 🇺🇸)

Location: virtual

Title: Robust Intelligent Systems [slides]

Abstract:

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 🇫🇷)

Location: virtual

Title: Generation of bounded invariants via stroboscopic set-valued maps: Application to the stability analysis of parametric time-periodic systems [slides]

Abstract:

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 🇩🇪)

Location: virtual

Title: On Information Control in Probabilistic Systems: a closer look on Opacity and Diagnosis [slides]

Abstract:

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 🇫🇷)

Location: virtual

Title: From Big-Step to Small-Step Skeletal Semantics

Abstract:

Skeletal semantics is a recent framework developed to formalize languages, from λ-calculus to JavaScript. Languages can be defined in a range of formats, 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.

Friday 13th November 2020 (1pm): Mathieu Montin (Université de Lorraine 🇫🇷)

Location: virtual

Title: A formal framework for heterogeneous systems semantics

Abstract:

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 🇫🇷)

Location: virtual

Title: Defeating Opaque Predicate using Binary Analysis and Machine Learning

Abstract:

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 🇫🇷)

Location: virtual

Title: Modeling and formal verification of a communicating autonomous vehicle system [slides]

Abstract:

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 🇫🇷)

Location: B011

Title: Parametric Timed Model Checking for Guaranteeing Timed Opacity

Abstract:

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 🇫🇷)

Location: B011

Title: Auxiliary Variables Revisited

Abstract:

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 🇫🇷)

Location: virtual

Title: TBA

Abstract:

TBA