Logo IRISA      logo Inria

Le séminaire en bref

Le séminaire 68NQRT est un séminaire commun de l'IRISA et d'Inria Rennes. Il a lieu le jeudi à 14 heures par défaut dans la salle Markov. Les thèmes du séminaire recouvrent des thèmes étudiés dans les départements « réseaux, télécommunication et services » et « langage et génie logiciel » de l'IRISA, ou des thèmes « Algorithmique, programmation, logiciels et architectures » et  « Réseaux, systèmes et services, calcul distribué » d'Inria. On y trouve des exposés introductifs, avancés ou prospectifs dans les thèmes du génie logiciel, de l'informatique théorique, des mathématiques discrètes et de l'intelligence artificielle.

D'après Mathematical Subject Classification:
68 Computer Science
N Software
Q Theory of computing
R Discrete mathematics in relation to computer science
T Artificial intelligence

Prochain Exposé

Jeudi 23 juin, 14h00 en salle Markov

Pierre-Evariste Dagand (LIP6)

Verifying Clock-Directed Modular Code Generation for Lustre

The correct compilation of block diagram languages like Lustre, SCADE, and the discrete subset of Simulink is important since they are used to program critical embedded control software. This talk addresses the compilation pass that transforms synchronous dataflow programs into imperative ones. The challenge is to move from a synchronous dataflow semantics, where programs manipulate streams of values, to an imperative one, where they perform stateful computations. We specify and verify in the Coq interactive theorem prover a code generator that handles the key aspects of Lustre, namely sampling, nodes and delays. Our solution introduces a novel intermediate model that combines features of the dataflow and imperative models.
This talk describes joint work with Timothy Bourke, Marc Pouzet, and Lionel Rieg.

Exposés des semaines suivantes

Jeudi 7 juillet, 14h00 en salle Sicile

Maximilien Colange (LSV)

Symbolic Optimal Reachability in Weighted Timed Automata

Weighted timed automata have been defined in the early 2000’s for modelling resource-consumption or -allocation problems in real-time systems. Optimal reachability is decidable in weighted timed automata, and a symbolic forward algorithm has been developed to solve that problem. This algorithm uses so-called priced zones, an extension of standard zones with cost functions. In order to ensure termination, the algorithm requires clocks to be bounded. For unpriced timed automata, much work has been done to develop sound abstractions adapted to the forward exploration of timed automata, ensuring termination of the model-checking algorithm without bounding the clocks. In this talk, we take advantage of recent developments on abstractions for timed automata, and propose an algorithm allowing for symbolic analysis of all weighted timed automata, without requiring bounded clocks.
Joint work with Patricia Bouyer and Nicolas Markey.