Level: M2

Contact: Pablo Arrighi

Read the complete description of the internship topic in PDF.

Level: M2

Contact: Philippe Schnoebelen

The logic of subsequences is the logic of the structure {$(X^*;\leq_*,..)$} where the universe {$X^*$} contains all finite sequences over some base set {$X$}, and where {$\leq_*$} is the subsequence relation (as in Higman's Lemma).

For example, this logic allows writing constraints like {$$ \tag{$\phi$} {aa}\leq_* x \land {bb}\leq_* x \land {ab}\not\leq_* x $$} where {$a,b$} are letters and {$x$} is a variable standing for an unknown word. Over {$X=\{a,b\}$}, the two-letter alphabet, the solution set of the above constraint is the language {$L_\phi={bbb}^*{aaa}^*$}.

The logic allows more complex formulae, like

\begin{equation*} \tag{$\psi$} \forall x,y: \exists z: \bigl( x\leq_* z\land y\leq_* z \land \forall u: x\leq_* u\land y\leq_* u\implies z\leq_* u \bigr) \end{equation*} that states that {$(X^*,\leq_*)$} is an upper semilattice. Whether {$\psi$} is true or false depends on {$X$}.

The goal of this Master Internship is to develop the computational theory of the logic of subsequences, especially by identifying decidable fragments of the logic and assessing their algorithmic complexity.

Read more...

Level: M1,M2

Contact: Burkhart Wolff, Safouan Taha

Summary. The theory of Communicating Sequential Processes going back to Hoare and Roscoe is still today one of the reference theories for concurrent specification and computing. This theory has been presented in Isabelle/HOL based on the denotational semantics of the Failure/Divergence Model of CSP; the resulting theory is called HOL-CSP. The "Plain Old Telephone Service" is a standard medium-size example for architectural modeling of a concurrent system. The goal of this internship is a formal analysis of deadlock and life lock properties of this protocol via interactive proof in Isabelle/HOL and Isabelle/HOL-CSP. Read more...

Level: M2

Contact: Philippe Dague <philippe.dague [at] universite-paris-saclay [dot] fr>, Lina Ye <lina.ye [at] centralesupelec [dot] fr>

Location: Laboratoire Méthodes Formelles, Université Paris-Saclay

Keywords: Timed Automata, Hybrid Automata, Diagnosability, Approximations, CEGAR, SMT, PINN

Read more...

Level: M2

Contact: Serge Haddad

Context. With the development of machine learning and its daily applications, gaining confidence in the systems produced by such techniques has become a critical issue. A first problem consists in formalizing what is expected from the systems. Such requirements may be either generic or specific to the task to be achieved. For instance, adversarial robustness is a generic property [1]. It measures howmuch information is needed by an attacker to “falsify” the answer of a classifying system. On the other hand, assume the system proposes actions to be performed in the presence of an intruder, a specific property would be that there is no actionto be proposed when no intruder is detected.

In the internship, we will focus on neural networks since this is the most widely used and moreover it presents similar features to hybrid systems letting the possibility to adapt efficient techniques from this domain. Let us illustrate an example of specification formula:

{$ \forall \mathbf{x}, y \, \mathrm{Pre}(x) \wedge \mathrm{InOut}( x, y) \implies \mathrm{Post}(y )$}

where {$x$} (resp.{$y$}) is the input (resp. output) vector of the system, {$Pre$} is a precondition on the inputs and {$Post$} is a postcondition on the outputs. Thus checking the negation of a formula consists in solving some existential first-ordertheory [3].

The design of verification for neural networks is a challenging issue sincethe number of neurons generally is between few hundreds and millions (see [2]for a comparative study for piecewise linear neural networks). The techniquesare either sound and complete [6] or can proceed via astraction [5] thus rising the issue of incompleteness and how to tackle with it. There are now softwareframework dedicated to the verification of deep neural networks [4].

Goals. Thus the goals of this internship are twofold:

• Specifying a language or a logic that can express the main properties ex-pected to be satisfied by neural networks;
• Identifying specificities of formula related to these properties in order to de-sign new exact and/or approximate algorithms for verifying these properties.

References

1. Bastani, O., Ioannou, Y., Lampropoulos, L., Vytiniotis, D., Nori, A.V.,Criminisi, A.: Measuring neural net robustness with constraints. In: Lee,D.D., Sugiyama, M., von Luxburg, U., Guyon, I., Garnett, R. (eds.)Advances in Neural Information Processing Systems 29: Annual Confer-ence on Neural Information Processing Systems 2016, December 5-10,2016, Barcelona, Spain. pp. 2613–2621 (2016),http://papers.nips.cc/paper/6339-measuring-neural-net-robustness-with-constraints
2. Bunel, R., Turkaslan, I., Torr, P.H.S., Kohli, P., Kumar, M.P.: Piecewise linearneural network verification: A comparative study. CoRRabs/1711.00455(2017),http://arxiv.org/abs/1711.00455
3. Katz, G., Barrett, C.W., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: Anefficient SMT solver for verifying deep neural networks. In: Majumdar, R., Kuncak,V. (eds.) Computer Aided Verification - 29th International Conference, CAV 2017,Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I. Lecture Notes in Com-puter Science, vol. 10426, pp. 97–117. Springer (2017). https://doi.org/10.1007/978-3-319-63387-95,https://doi.org/10.1007/978-3-319-63387-9_5
4. Katz, G., Huang, D.A., Ibeling, D., Julian, K., Lazarus, C., Lim, R., Shah, P.,Thakoor, S., Wu, H., Zeljic, A., Dill, D.L., Kochenderfer, M.J., Barrett, C.W.:The marabou framework for verification and analysis of deep neural networks.In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st InternationalConference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I. Lecture Notes in Computer Science, vol. 11561, pp. 443–452. Springer(2019). https://doi.org/10.1007/978-3-030-25540-426,https://doi.org/10.1007/978-3-030-25540-4_26
5. Mirman, M., Gehr, T., Vechev, M.T.: Differentiable abstract interpretation for provably robust neural networks. In: Dy, J.G., Krause, A. (eds.) Proceedingsof the 35th International Conference on Machine Learning, ICML 2018, Stockholm, Sweden, July 10-15, 2018. Proceedings of Machine Learn-ing Research, vol. 80, pp. 3575–3583. PMLR (2018),http://proceedings.mlr.press/v80/mirman18b.html
6. Tjeng, V., Tedrake, R.: Verifying neural networks with mixed integer programming. CoRRabs/1711.07356(2017),http://arxiv.org/abs/1711.07356

Contact: Stefan Schwoon, Stefan Haar

Supervisory control of partially observable Petri nets has been studied int he literature mostly under a sequential and centralized perspective. With new application challenges from systems biology, it is time to to create a frameworkfor supervisory control of partially observable Petri nets, under the constraints of concurrency of the supervised processes (which are intrinsically non-sequential)and decentralization of observation and intervention.

The objectives targeted by the control must include reachability objectives in safe Petri nets; ideally, the results exceed this domain, to include reprogrammingof long-term behaviors of models arising in cell regulation. In this setting, thestakes are to steer the cell fate into a desired attractor or phenotype, whilestaying clear of fatal pathways (cancerous mutation, etc.)

The strengths of the well-known unfolding technique for safe Petri nets are expected to be instrumental in this work. The controller’s knowledge is a decentralized and asynchronous observation coming from a distributed set of observers. The tasks include:

• establish the semantics of supervisory control under these circumstances;
• determine an adequate game theoretic setting, and
• develop efficient techniques for synthezing controllers.

Level: M2

Contact: Laurent Doyen

Keywords: automata theory, probability, algorithms.

Read more...

Contact: Burkhart Wolff

Description du stage en pdf.

Contexte

Au sein de l’Institut de Recherche Technologique SystemX, situé au cœur du campus scientifique d’excellence mondiale de Paris-Saclay, vous prendrez une part active au développement d’un centre de recherche technologique de niveau international dans le domaine de l’ingénierie numérique des systèmes. Adossé aux meilleurs organismes de recherche français du domaine et constitué par des équipes mixtes d’industriels et d’académiques, ce centre a pour mission de générer de nouvelles connaissances et solutions technologiques en s’appuyant sur les percées de l’ingénierie numérique et de diffuser ses compétences dans tous les secteurs économiques.

Vous serez encadré par un ingénieur chercheur SystemX du domaine Sûreté de Fonctionnement, et vous aurez des échanges avec des chercheurs du Laboratoire Méthodes Formelles (LMF), notamment B. Wolff et S. Taha.

Vous travaillerez au sein du projet de recherche SystemX 3SA – Simulation pour la Sécurité des systèmes du véhicule Autonome – dont les partenaires industriels sont Apsys, AVsimulation, Expleo, Stellantis, Oktal-SE, Renault, SECTOR Group, Valeo et les partenaires académiques le CEA (Commissariat à l’Energie Atomique), le LNE (Laboratoire national de métrologie et d'essais) et le LMF (Laboratoire Méthodes Formelles).

Le poste est basé à l’IRT SystemX – 2, Boulevard Thomas Gobert 91120 Palaiseau.

Durée et date de démarrage

Read more...

Niveau: M2, Postdoc

Contact: Burkhart Wolff

Lire la description du stage en pdf.

Contexte

Au sein de l’Institut de Recherche Technologique SystemX, situé au cœur du campus scientifique d’excellence mondiale de Paris-Saclay, vous prendrez une part active au développement d’un centre de recherche technologique de niveau international dans le domaine de l’ingénierie numérique des systèmes. Adossé aux meilleurs organismes de recherche français du domaine et constitué par des équipes mixtes d’industriels et d’académiques, ce centre a pour mission de générer de nouvelles connaissances et solutions technologiques en s’appuyant sur les percées de l’ingénierie numérique et de diffuser ses compétences dans tous les secteurs économiques.

Vous serez encadré par un ingénieur chercheur SystemX du domaine Sûreté de Fonctionnement, et vous aurez des échanges avec des chercheurs du Laboratoire Méthodes Formelles (LMF), notamment B. Wolff et S. Taha.

Vous travaillerez au sein du projet de recherche SystemX 3SA – Simulation pour la Sécurité des systèmes du véhicule Autonome – dont les partenaires industriels sont Apsys, AVsimulation, Expleo, Stellantis, Oktal-SE, Renault, SECTOR Group, Valeo et les partenaires académiques le CEA (Commissariat à l’Energie Atomique), le LNE (Laboratoire national de métrologie et d'essais) et le LMF (Laboratoire Méthodes Formelles).

Le poste est basé à l’IRT SystemX – 2, Boulevard Thomas Gobert 91120 Palaiseau.

Durée et date de démarrage

Read more...

Modeling and analysis of cyber-physical systems is a challenge for formal methods and an active area of research. Initially developed for the analysis of the safety properties of autonomous vehicles (see [1]), the HOL-Cyberphy framework, based on the Isabelle/HOL proof assistant, has been generalized to model multi-agent cyber-physical systems. . The objective of this internship is to study this framework, notably based on the use of an Isabelle theory of Communicating Sequential Processes (see [2]), and to adapt it to the modeling of cyber-multi-agent systems. communicating physics, in order to analyze and prove their proper functioning properties. We can particularly draw inspiration from the work of André Platzer in this area (see [3]).

Missions:

1. Constitute a state of the art on the formal modeling of communicating cyber-physical multi-agent systems;
2. Take charge of the Isabelle HOL-CyberPhy framework, by creating some models of single and multi-agent cyber-physical systems;
3. Design a generic model of communicating cyber-physical multi-agent systems based on case studies to be identified, and propose an adaptation of the HOL-CyberPhy framework accordingly.

Bibliographic references on the subject:

• [1] Paolo Crisafulli, Safouan Taha, Burkhart Wolff. Modeling and Proving Safety in Autonomous Cars Scenarios in HOL-CSP. Research Report 1, University Paris-Saclay; IRT SystemX, Palaiseau. 2021, pp.81. URL:
• [2] Taha S., Ye L., Wolff B.: HOL-CSP Version 2.0. Archive of Formal Proofs (2019).
• [3] Brieger, Marvin & Mitsch, Stefan & Platzer, André. (2023). Dynamic Logic of Communicating Hybrid Programs

The internship may lead to recruitment for a thesis, on the subject described here