Workshop on Infinite Systems
and Verification of Quantitative Properties

Programme and Slides

Wednesday 5

• 10:30-11:30 Giorgio Delzanno (Genova U.) : Verification of multithreaded programs
• 11:45-12:45 Bernard Boigelot (Liège U.) : Hybrid Acceleration using Real Vector Automata
• 14:00-15:00 Philippe Schnoebelen (LSV, Cachan): The Verification of Lossy Channel Systems
• 15:15-16:15 Tomas Vojnar (LIAFA, Paris): Verification of Parameterized Systems of Processes with FIFO-based Resource Management
• 16:30-17:30 Silvio Ranise and David Deharbe (LORIA, Nancy) Validity Checking with If-then-else Expressions Modulo Rich First-Order Theories

Thursday 6

•  9:00-10:00 Joost-Pieter Katoen (Twente U.) : Performance analysis by model checking (see also the bibliography)
• 10:15-11:15 Denis Lugiez (Marseille) : Multitree automata
• 11:30-12:30 Blaise Genest (LIAFA, Paris): Projection of HMSCs
• 14:00-15:00 Eugene Asarin (Verimag, Grenoble) : Theory of Timed Languages
• 15:15-16:15 Oded Maler (Verimag, Grenoble) : A New Theory of Scheduling based on Timed Automata
• 16:30-17:30 Pierre-Yves Schobbens (FUNDP, Namur) Real-time ATL

Friday 7

•  9:00-10:00 Mooly Sagiv (Tel-Aviv U.) : Shape analysis
• 10:15-11:15 Eric Goubault (CEA, Saclay) : Static analysis of floating-point computations by abstract interpretation - current status and problems
• 11:30-12:30 Wendelin Serwe (IRISA, Rennes) : Abstracting Call-Stacks for Interprocedural Verification of Imperative Programs
• 13:45-14:45 Ahmed Bouajjani (LIAFA, Paris) : Regular Model Checking - verification of parametrized and dynamic systems
• 15:00-16:00 Tayssir Touili (LIAFA, Paris): Reachability analysis of Process Rewrite Systems: Application to the verification of multithreaded recursive programs