AA/Seminar

Seminar "Automata and Applications"

The seminar of the research group Automata and Applications is held every 2-3 weeks, usually online. It is open to the public.

The languages of the seminar are French and English. Talks may be given, and questions asked, in any of the two languages.

If you want to participate in the seminar, or if you want to propose a talk, send an email to the organizer.

Upcoming Talks

• Monday 20 March 14:00: Vincent Botbol: Static analysis of Michelson smart-contracts using abstract interpretation
  • In this talk, we briefly introduce the Toss blockchain and Michelson, its statically typed stacked-based smart-contract language. Then, we present a static analysis for Michelson smart-contracts using abstract interpretation. Our tool automatically infers (numerical) invariants allowing us to verify numerical safety properties along with more blockchain-specific functional properties, e.g., validating user authentication patterns, analyzing the evolution of contract's storage, determining an upper-bound gas usage of a smart-contract,... This ongoing work is integrated as an addition to the MOPSA platform which already provides abstract interpretation-based analysis of C and Python programs.

Previous Seminars

• Thursday 2 February 10:00: Uli Fahrenberg: A Generic Approach to Quantitative Verification
  • This talk is concerned with quantitative verification, that is, the verification of quantitative properties of quantitative systems. These systems are found in numerous applications, and their quantitative verification is important, but also rather challenging. In particular, given that most systems found in applications are rather big, compositionality and incrementality of verification methods are essential. In order to ensure robustness of verification, we replace the Boolean yes-no answers of standard verification with distances. Depending on the application context, many different types of distances are being employed in quantitative verification. Consequently, there is a need for a general theory of system distances which abstracts away from the concrete distances and develops quantitative verification at a level independent of the distance. It is our view that in a theory of quantitative verification, the quantitative aspects should be treated just as much as input to a verification problem as the qualitative aspects are. In this work we develop such a general theory of quantitative verification. We assume as input a distance between traces, or executions, and then employ the theory of games with quantitative objectives to define distances between quantitative systems. Different versions of the quantitative bisimulation game give rise to different types of distances, viz.~bisimulation distance, simulation distance, trace equivalence distance, etc., enabling us to construct a quantitative generalization of van Glabbeek's linear-time--branching-time spectrum. We also extend our general theory of quantitative verification to a theory of quantitative specifications. For this we use modal transition systems, and we develop the quantitative properties of the usual operators for behavioral specification theories.
  • Online at https://meet.jit.si/seminar-AA

• Tuesday 13 December 10:00: Vijay Ganesh: SAT Solver + Computer Algebra Attack on the Minimum Kochen-Specker Problem (conjoint with LIP6)
  • One of the most fundamental results in the foundations of quantum mechanics is the Kochen--Specker (KS) theorem, a `no-go' theorem which states that contextuality is an essential feature of any hidden-variable theory. The theorem hinges on the existence of a mathematical object called a KS vector system. Although the existence of a KS vector system was first established by Kochen and Specker, the problem of the minimum size of such a system has stubbornly remained open for over 50 years. In this paper, we present a new method based on a combination of a SAT solver and a computer algebra system (CAS) to address this problem. We improve the lower bound on the minimum number of vectors in a KS system from 22 to 23 and improve the efficiency of the search by a factor of over 1000 when compared to the most recent computational methods. Finding a minimum KS system would simplify experimental tests of the KS theorem and have direct applications in quantum information processing, specifically in the security of quantum cryptographic protocols based on complementarity, zero-error classical communication, and dimension witnessing.

• Monday 21 November 11:00: Souheib Baarir: Contributions to Boolean satisfiability solving and its application to the analysis of discrete systems
  • Despite its NP-Completeness, propositional (Boolean) satisfiability (SAT) covers a broad spectrum of applications. Nowadays, it is an active research area finding its applications in many contexts: planning decision, cryptology, computational biology, hardware and software analysis, etc. Hence, the development of approaches that could handle increasingly challenging SAT problems has become a focus. During these last 8 years, SAT solving has been the main subject of my research work, and in this talk I will present some of the main results we obtained in the field.

• Wednesday 26 October 15:00: Gaëtan Staquet: Learning Realtime One-Counter Automata
  • We present a new learning algorithm for realtime one-counter automata. Our algorithm uses membership and equivalence queries as in Angluin's L* algorithm, as well as counter value queries and partial equivalence queries. In a partial equivalence query, we ask the teacher whether the language of a given finite-state automaton coincides with a counter-bounded subset of the target language. We evaluate an implementation of our algorithm on a number of random benchmarks and on a use case regarding efficient JSON-stream validation.
  • Recording: https://peertube.lre.epita.fr/w/toVh61JXaxNUdxBViUpRvD

• Wednesday 26 October 13:30: Guillermo Perez: The Geometry of Reachability in Continuous Vector Addition Systems with States
  • We study the geometry of reachability sets of continuous vector addition systems with states (VASS). In particular we establish that they are almost Minkowski sums of convex cones and zonotopes generated by the vectors labelling the transitions of the VASS. We use the latter to prove that short so-called linear path schemes suffice as witnesses of reachability in continuous VASS of fixed dimension. Then, we give new polynomial-time algorithms for the reachability problem for linear path schemes. Finally, we also establish that enriching the model with zero tests makes the reachability problem intractable already for linear path schemes of dimension two.
  • Recording: https://peertube.lre.epita.fr/w/nQVdcT73vYzBfgQqZDwKJ4

• Friday 14 October 14:00: Sarah Berkemer: Compositional properties of alignments
  • Alignments, i.e., position-wise comparisons of two or more strings or ordered lists are of utmost practical importance in computational biology and a host of other fields, including historical linguistics and emerging areas of research in the Digital Humanities. The problem is well-known to be computationally hard as soon as the number of input strings is not bounded. Due to its practical importance, a huge number of heuristics have been devised, which have proved very successful in a wide range of applications. Alignments nevertheless have received hardly any attention as formal, mathematical structures. Here, we focus on the compositional aspects of alignments, which underlie most algorithmic approaches to computing alignments. We also show that the concepts naturally generalize to finite partially ordered sets and partial maps between them that in some sense preserve the partial orders. As a consequence of this discussion we observe that alignments of even more general structure, in particular graphs, are essentially characterized by the fact that the restriction of alignments to a row must coincide with the corresponding input graphs. Pairwise alignments of graphs are therefore determined completely by common induced subgraphs. In this setting alignments of alignments are well-defined, and alignments can be decomposed recursively into subalignments. This provides a general framework within which different classes of alignment algorithms can be explored for objects very different from sequences and other totally ordered data structures.

• Friday 30 September 14:00: Florian Renkin: Transformations d’ω-automates pour la synthèse de systèmes réactifs
  • La synthèse vise à produire un système correct à partir de spécifications. Une approche pour résoudre ce problème consiste à traduire la spécification en un jeu de parité dont la stratégie gagnante encode le système. Dans cet exposé nous verrons deux méthodes permettant de produire des automates de parité. La première s’appuie sur l’amélioration et la combinaison de procédures nouvelles ou existantes. La seconde est un algorithme de Casares et al. apportant une garantie d’optimalité du résultat. Dans un deuxième temps, nous verrons comment nous réduisons le système obtenu. Deux types de réductions seront abordées. La première permet d’obtenir un résultat optimal mais pas la seconde qui privilégie le temps de traitement.

• Friday 9 September 14:00: Alexandre Duret-Lutz: À l'arrache : Spot
  • Présentation informelle de Spot, bibliothèque C++ de manipulation d'ω-automates et de formules de logique temporelle linéaire, fournissant des bindings Python et plusieurs outils.