Séminaire de l'équipe Méthodes Formelles (MF)

Le séminaire MF a lieu salle 178 presque tous les mardis à 11H.

Pour proposer un séminaire, le calendrier vous aidera à choisir une date disponible.

Pour s'abonner ou se désabonner de la liste de diffusion.


Prochains exposés

DateOrateurTitre
mardi 10 octobre 2017Miguel Romero (Oxford University) TBD
TBD



Précédents exposés depuis janvier 2017

DateOrateurTitre
mardi 04 juillet 2017Stefan GRUNER (University of Pretoria, South Africa) SAT-based Bounded Model Checking for 3-Valued Abstractions - Part II
Continuation of his precedent talk.
mardi 27 juin 2017Stefan GRUNER (University of Pretoria, South Africa) SAT-based Bounded Model Checking for 3-Valued Abstractions
In this talk I will present joint work with Nils Timm (and students) from the University of Pretoria on how to make model-checking of concurrent systems more effective and more efficient. In the first part of the talk, which is based on our SBMF'16 paper, I show how bounded model-checking over a three-valued truth domain {T:true, F:false, U:unknown} can be translated into a classical Boolean satisfiability problem which can then be given to any classical SAT solver. In the second part of the talk, which is based on our recent FSEN'17 paper, I speak about efficiency-increasing heuristics which are based on the availability of structural knowledge about the original system to be model-checked. On the basis of such structural knowledge the SAT solver can be guided into 'promising' search paths, whereby the probability of unnecessarily exploring fruitless paths is considerably diminished. The SBMF'16 paper was acknowledged as the "2nd-best paper of the conference", and the FSEN'17 paper was nominated among the "top three papers of the conference".
mardi 13 juin 2017Emilia Descotte (UBA, Argentine) Axiomatizations for downward XPath on Data Trees
We give sound and complete axiomatizations for XPath with data tests by "equality" or "inequality", and containing the single "child" axis. This data-aware logic predicts over data trees, which are tree-like structures whose every node contains a label from a finite alphabet and a data value from an infinite domain. The language allows us to compare data values of two nodes but cannot access the data values themselves (i.e., there is no comparison by constants). Our axioms are in the style of equational logic, extending the axiomatization of data-oblivious XPath, by B. ten Cate, T. Litak and M. Marx. We axiomatize the full logic with tests by "equality" and "inequality", and also a simpler fragment with "equality" tests only. Our axiomatizations apply both to node expressions and path expressions. The proof of completeness relies on a novel normal form theorem for XPath with data tests.
mardi 30 mai 2017Victor Marsault (University of Liège) An efficient algorithm to decide the periodicity of b-recognisable sets using MSDF convention
Given an integer base b>1, a set of integers is represented in base b by a language over {0,1,...,b-1}. The set is said b-recognisable if its representation is a regular language. It is known that eventually periodic sets are b-recognisable in every base b, and Cobham's theorem imply the converse: no other set is b-recognisable in every base b. We are interested in deciding whether a b-recognisable set of integers (given as a finite automaton) is eventually periodic. Honkala showed in 1986 that this problem is decidable and recent developments give efficient decision algorithms. However, they only work when the integers are written with the least significant digit first. In this work, we consider here the natural order of digits (Most Significant Digit First) and give a quasi-linear algorithm to solve the problem in this case.
mardi 23 mai 2017Michael Raskin (LaBRI) A linear lower bound for incrementing a space-optimal integer representation in the bit-probe model
We present the first linear lower bound for the number of bits required to be accessed in the worst case to increment an integer in an arbitrary space-optimal binary representation. The best previously known lower bound was logarithmic. It is known that a logarithmic number of read bits in the worst case is enough to increment some of the integer representations that use one bit of redundancy, therefore we show an exponential gap between space-optimal and redundant counters. Our proof is based on considering the increment procedure for a space optimal counter as a permutation and calculating its parity. For every space optimal counter, the permutation must be odd, and implementing an odd permutation requires reading at least half the bits in the worst case. The combination of these two observations explains why the worst-case space-optimal problem is substantially different from both average-case approach with constant expected number of reads and almost space optimal representations with logarithmic number of reads in the worst case. https://arxiv.org/abs/1607.00242 ; ICALP 2017
mardi 16 mai 2017Igor Walukiewicz (LaBRI) Proving safety of concurrent programs
This talk will be based on the paper from POPL 2017: Thread Modularity at Many Levels: a pearl of compositional verification by Jochen Hoenicke, Rupak Majumdar, and Andreas Podelski In the paper the authors consider the problem of proving safety of (parametrized) concurrent programs. They do not propose new techniques but rather revisit some existing ones. I have found putting these techniques next to each other very interesting and thought provoking. Since the considered problem is a fundamental problem for verification, I think it is worth to see this work at the seminar. This will not be a survey talk. Technically the talk will be very easy, as the results are straightforward. The goal is to present a view point on the problem that I have got from reading the paper.
mardi 09 mai 2017Alain Finkel (LSV, ENS Cachan) WBTS: the new class of WSTS without WQO.
We present the ideal framework [FG09a,BFM14] which was recently used to obtain new deep results on Petri nets and extensions. If time, we will present the proof of the famous but unknown Erdös-Tarski theorem. We argue that the theory of ideals prompts a renewal of the theory of WSTS by providing a way to define a new class of monotonic systems, the so-called Well Behaved Transition Systems, which properly contains WSTS, and for which coverability is still decidable by a forward algorithm.
mardi 25 avril 2017Nathan Lhote (LaBRI) On Reversible Transducers
Deterministic two-way transducers define the robust class of regular functions which is, among other good properties, closed under composition. However, the best known algorithms for composing two-way transducers cause a double exponential blow-up in the size of the inputs. We introduce a class of transducers for which the composition has polynomial complexity. It is the class of reversible transducers, for which the computation steps can be reversed deterministically. While in the one-way setting this class is not very expressive, any two-way transducer can be made reversible through a single exponential blow-up. As a consequence, the composition of two-way transducers can be done with a single exponential blow-up in the number of states. A uniformization of a relation is a function with the same domain and which is included in the original relation. Our main result actually states that we can uniformize any non-deterministic two-way transducer by a reversible transducer with a single exponential blow-up, improving the known result by de Souza which has a quadruple exponential complexity. As a side result, our construction also gives a quadratic transformation from copyless streaming string transducers to two-way transducers, improving the exponential previous bound.
mardi 04 avril 2017Andrzej Murawski (University of Warwick) Automata theory and game semantics of higher-order computation
I will give a survey of various classes of automata that have been used to capture the game semantics of higher-order programs and, consequently, obtain decidability results for contextual equivalence.
mardi 28 mars 2017David Janin (LaBRI) Time domain (for time denotational semantics)
Directed complete partial orders (cpos) are used in denotational semantics for describing the way each value is incrementally computed, passing from a completely unknown value to a completely known value. Then, continuous functions between cpos propagate increase of knowledge on their inputs to increase of knowledge on their outputs. In this talk, we define the notion timed cpo by means of a cut function that tells what part of any value is known before any given instant. In the induced partial order, the increase of knowledge explicitly refers to the passage of time. It follows that continuous functions between timed cpos provide denotational semantics model candidates for timed IO-system acting over (higher-order) time evolving values, e.g. timed streams, but also bounded below values, partial inductive structures, timed functions, etc. Definitions, examples and (closure) properties of these timed cpos and their continuous functions are provided throughout.
mardi 21 mars 2017Laurent Bienvenu (LIRMM Montpellier) Learning probability measures
Suppose we have a probabilistic algorithm given as a black box and we have access to an output of this algorithm. There are two - related - questions one could ask. (1) Is it possible to make a plausible guess as to which algorithm is in the box? (2) Can we use the output of this algorithm as a random number generator by extracting `pure’ randomness from it? We will look at these questions from the point of view of computability and algorithmic learning theory. [Based on joint work with S. Figueira, B. Monin, and A. Shen]
mardi 14 mars 2017Gabriele Puppis (LaBRI) On the decomposition of finite-valued streaming string transducers
I will present some preliminary results towards a proof of a decomposition theorem for streaming string transducers (SSTs). Roughly, the conjectured decomposition theorem states that every SST that associates at most k outputs to each input can be effectively decomposed as a finite union of functional SSTs. Such a result would imply, among other things, the decidability of the equivalence problem for the considered class of transducers as well as a correspondence with the classical two-way transducers. I will present a proof of this decomposition theorem in the special case of SSTs with 1 register. The proof heavily relies on a combinatorial result by Kortelainen concerning word equations with iterated factors.
mardi 07 mars 2017Charles Grellois (University of Bologna) Verifying properties of functional programs: from the deterministic to the probabilistic case
In functional programs, also called higher-order programs, functions may take functions themselves as arguments. As a result, their model-checking relies in most approaches on semantic or type-theoretic tools. In this talk, I will explain how an analysis based on linear logic of a model-checking result of 2009 by Kobayashi and Ong led Melliès and I to the construction of a model for model-checking. This model is such that, when interpreting a term with recursion representing the tree of traces of a functional program, its denotation determines whether it satisfies a MSO property of interest. A related and similar model was obtained independently by Salvati and Walukiewicz. In the second part of the talk, I will discuss the verification of termination for functional programs with recursion and probabilistic choice. Dal Lago and I defined recently a type system which is such that typable programs terminate with probability 1. In other terms, their set of diverging executions is negligible. If time allows, I will sketch ideas towards an extension of the model-checking results of the deterministic case to quantitative logics and functional programs with recursion.
mardi 28 février 2017Emmanuel Fleury (LaBRI) Digital Currencies
Electronic money is a quite old problem in cryptology (Chaum, 1982) but recent discoveries lead to the birth of a new type of digital currency such as Bitcoins or Ethereum. Most of the new crypto-currencies are based on the concept of Blockchain which is used to maintain a trusted consensus in a distributed manner thanks to cryptographic primitives. This talk will summarize the main concepts and mechanisms used to ensure the security of Bitcoins and Blockchain.
mardi 14 février 2017Hugo Gimbert (LaBRI) Emptiness of nonzero automata is decidable
Zero automata are a probabilistic extension of parity automata on infinite trees. Bojanczyk has shown recently that the satisfiability of a certain probabilistic variant of MSO, called TMSO+zero reduces to the emptiness problem for zero automata. These automata perform random walks on the input (binary) tree: when the automaton is in a state q on a node labelled with a, it selects non-deterministically a transition (q,a,r_0,r_1) and moves with equal probability 1/2 either to the left node in state r_0 or to the right node in state r_1.. The acceptance condition of zero automata impose conditions not only on the parity of individual branches of the run but as well on some other properties of runs that should occur almost-surely or with positive probability. We introduce a variant of zero automata called nonzero automata and we show that i) for every zero automaton there is an equivalent nonzero automaton of quadratic size ii) the emptiness problem of nonzero automata is decidable, with complexity {sc np}. These results imply that TMSO+zero has decidable satisfiability. Joint work with Mikolaj Danger Bojanczyk and Edon Kelmendi
mardi 24 janvier 2017Rasmus Ibsen-Jensen (IST Austria) Faster algorithms for program analysis
The talk is based on joint work with Krishnendu Chatterjee, Amir Kafshdar Goharshady, Prateesh Goyal, and Andreas Pavlogiannis. The talk is about solving graph problems (focusing on graph problems that are often reduced to in program analysis) faster when the graphs are composed of control flow graphs of methods in programs. Using that control flow graphs of methods typically have constant tree-width we consider when the program either (i) has a single method, (ii) has many methods, or (iii) concurrent threads, each on a single method. For cases (ii) and (iii), we consider the Algebraic Path Problem (APP), which is a very general problem, with many interesting special cases, such as (1) reachability and shortest path (with positive and negative weights), (2) the IDE/IDFS frameworks of program analysis and (3) most probable path. Since APP has already been optimally solved for single methods/constant tree-width graphs, up to factors of log^* n (n is the number of states), in (i), if time permits, we will consider other weighted graph problems that has been reduced to in program analysis (but which are not special cases of APP), specifically finding the cycle with the least mean of weights (the minimum mean-payoff problem) and for a given start node v, finding the minimum number c and a path from v where all prefix sums of the weights of the path are greater than -c (the minimum initial credit problem). In all cases, we give simple algorithms which are faster than the state-of-the-art in theory and practice. The talk is based on my POPL papers from 2015 and 2016, and, if time permits, my CAV paper from 2015 (see e.g. my homepage at http://rasmus.ibsen-jensen.com for the papers). No prior specialised knowledge is necessary to follow the talk.
mardi 10 janvier 2017B Srivathsan (CMI Chennai) Why liveness for timed automata is hard, and what we can do about it
The liveness problem for timed automata asks if a given automaton has an infinite run visiting an accepting state infinitely often. In this talk, we will show that if P is not equal to NP, the liveness problem is "more difficult" than the reachability problem - more precisely, we will exhibit a family of automata for which reachability is in P whereas liveness is NP-hard. We will then present a new algorithm to solve the liveness problem, and compare it with existing solutions. Joint work with F. Herbreteau, T.T. Tran and I. Walukiewicz.



Archives des années précédentes




Responsables

Diego Figueira, Gabriele Puppis