VeriDis seminar

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. 

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

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 2021 (1pm): TBA (Université de Lorraine 🇫🇷)

Location: virtual

Title: TBA

Abstract:

TBA

 

 

 

Comments are closed.