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.
|mardi 24 janvier 2017||Rasmus Ibsen-Jensen
||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.|
Précédents exposés depuis janvier 2017
|mardi 10 janvier 2017||B 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
Diego Figueira, Gabriele Puppis