Oded Maler

Research Director


Contact information

Research interests:  Theory of Automata, Monitoring, Verification and Synthesis of Timed and Hybrid Systems, Machine Learning, Systems Biology.

Short Cucurriculum Vitae
"In the beginning
God created the heaven and the earth. And the earth was without form, and void; and darkness was upon the face of the deep. And the Spirit of God moved upon the face of the waters."
Oded Maler was born in 21.2.57 in Haifa, Israel. He obtained his B.A. in Computer Science from the Technion, Haifa in 1979 and his M.Sc. in Management Science from the University of Tel-Aviv at In 1984. In 1989 he finished his Ph.D. thesis (Finite Automata: Infinite Behavior, Learnability and Decomposition), under the liberal supervision of A. Pnueli in the department of Applied Mathematics and Computer Science, Weizmann Institute, Rehovot. After two years of post-doc at IRISA, Rennes, he moved to Grenoble at 1992 and obtained a research position (CR1) at the CNRS (French National Center of Scientific Research) in 1994. He has been promoted to "research director" (DR2) in 2001 and (DR1) in 2011. And he lives more or less happily ever after.

Warm topics

·  Funded PhD Position: Data Mining of Dynamic Behaviors using Signal Temporal Logic NewNew

·  Thesis defense, Dogan Ulus, Pattern Matching with Time: Theory and Applications 15/01/2018, 14:00 slides New

·  HSCC, Monitoring and Testing of Cyber-Physical Systems (MT-CPS) Porto, April 2018 New

·  Frontiers in Analog CAD (FAC) Vienna, May 16-17, 2018 New

·  Computational Methods in Systems Biology (CMSB) Brno, September 12-14, 2018 New

·  FORMATS, Beijing, September 4-6, 2018 New

·  Thesis defense, Irini-Eleftheria Mens, Learning Regular Languages over Large Alphabets slides

·  Timed and Hybrid Systems research at Verimag 2009-2014 Slides

·  Dynamic Systems Biology (slides, December 2013), video, September 2013 part 1 part 2

·  SpaceEx: The State-space Explorer

·  My Habilitation (a kind of scientific autobiography summarizing my research from 1987 to 2000)

·  Continuous Systems Verification 2010 Slides Video

·  Research on Analog Circuit Verification at Verimag, Toward AMS verification (slides)

·  At Least Now  Poems (in Hebrew) 1978.

·  Publications Google scholar DBLP Research Gate CV (long)

Recent Work

·  A. Bakhirkin, T. Ferrere, D. Nickovic, O. Maler, E. Asarin Online Timed Pattern Matching using Automata, FORMATS 2018 NewNew

·  E. Bartocci, J. Deshmukh, A. Donzé, G. Fainekos, O. Maler, D. Nickovic, S. Sankaranarayanan, Specification-based Monitoring of Cyber-Physical Systems, Lectures on Runtime Verification 2018 New

·  D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, D. Ulus, AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic, TACAS 2018 SlidesNew

·  A. Bakhirkin, T. Ferrere, O. Maler, Efficient Parametric Identification for STL, HSCC 2018 Slides New

·  O. Maler, D. Ulus, Specifying Timed Patterns using Temporal Logic, HSCC 2018 Slides New

·  O. Maler, Learning Monotone Partitions of Partially-Ordered Domains (Work in Progress), 2017 Slides

·  A. Bakhirkin, T. Ferrere, O. Maler, D. Ulus, On the Quantitative Semantics of Signal Regular Expressions over Real-Valued Signals, FORMATS 2017 Slides

·  E. Asarin, O. Maler, D. Nickovic, D. Ulus, Combining the Temporal and Epistemic Dimensions for MTL Monitoring, FORMATS 2017 Slides

·  O. Maler, I.E. Mens, A Generic Algorithm for Learning Symbolic Automata from Membership Queries, Models, Algorithms, Logics and Tools 2017

Selected Publications

Hybrid Systems: General

·  O. Maler, Some Thoughts on Runtime Verification, RV 2016 Slides

·  O. Maler, The Unmet Challenge of Timed Systems, From Programs to Systems, 2014 Slides

·  O. Maler, On Under-Determined Dynamical Systems, EMSOFT 2011, Slides

·  O. Maler, Amir Pnueli and the Dawn of Hybrid Systems, HSCC 2010, Good slides

·  O. Maler, On Optimal and Reasonable Control in the Presence of Adversaries, IFAC Annual Reviews in Control 2007 Slides French version

·  O. Maler, Analog Circuit Verification: a State of an Art, FAC 2005

·  O. Maler, Control from Computer Science, IFAC Annual Reviews in Control 2003 Slides

·  O. Maler, Guest Editorial: Verification of Hybrid Systems, European Journal of Control 2001

·  O. Maler, A Unified Approach for Studying Discrete and Continuous Dynamical Systems, CDC 1998

·  O. Maler, Hybrid Systems and Real-World Computations, unpublished 1992

Monitoring, Signal Temporal Logic, Timed Regular Expressions

·  O. Maler, Some Thoughts on Runtime Verification, RV 2016 Slides

·  D. Ulus, T. Ferrere, E. Asarin, O. Maler, Online Timed Pattern Matching using Derivatives, TACAS 2016 Slides

·  T. Ferrere, O. Maler, D. Nickovic, Trace Diagnostics using Temporal Implicants, ATVA 2015 Slides

·  T. Ferrere, O. Maler, D. Nickovic, D. Ulus, Measuring with Timed Patterns, CAV 2015 Slides

·  D. Ulus, T. Ferrere, E. Asarin, O. Maler, Timed Pattern Matching, FORMATS 2014 Slides

·  A Donze, T. Ferrere, O. Maler, Efficient Robust Monitoring for STL, CAV 2013 Slides

·  O. Maler, D. Nickovic, Monitoring Properties of Analog and Mixed-Signal Designs, STTT 2013

·  A. Donze, O. Maler, E. Bartocci, D. Nickovic, R. Grosu, S. Smolka, On Temporal Logic and Signal Processing, ATVA 2012

·  E. Asarin, A. Donze, O. Maler, D. Nickovic, Parametric Identification of Temporal Properties, RV 2011 Slides

·  A. Donze, O. Maler, Robust Satisfaction of Temporal Logic over Real-Valued Signals, FORMATS 2010

·  O. Maler, D. Nickovic, A. Pnueli, Checking Temporal Properties of Discrete, Timed and Continuous Behaviors, Pillars of Computer Science, 2008

·  D. Nickovic, O. Maler, AMT: a Property-based Monitoring Tool for Analog Systems, FORMATS 2007 Slides

·  O. Maler, D. Nickovic, Monitoring Temporal Properties of Continuous Signals, FORMATS/FTRTFT 2004

·  E. Asarin, O. Maler, P. CaspiTimed Regular Expressions, The Journal of the ACM, 2002 

·  E. Asarin, O. Maler, P. CaspiA Kleene Theorem for Timed Automata, LICS 1997

Hybrid Systems: Reachability, Synthesis, Exploration

·  J. Deshmukh, X. Jin, J. Kapinski, O. Maler, Stochastic Local Search for Falsification of Hybrid Systems, ATVA 2015 Slides

·  O. Maler, Algorithmic Verification of Continuous and Hybrid Systems, Infinity 2013 Slides

·  T. Dang, C. Le Guernic, O. Maler, Computing Reachable States for Nonlinear Biological Models, TCS 2011 Slides

·  E. Asarin, T. Dang, O. Maler, R. Testylier, Using Redundant Constraints for Refinement, ATVA 2010

·  O. Maler, G. Batt, Approximating Continuous Systems by Timed Automata, FMSB 2008

·  A. Donze, O. Maler,  Systematic Simulation using Sensitivity Analysis, HSCC 2007 Slides

·  A. Girard, C. Le Guernic, O. Maler, Efficient Computation of Reachable Sets of Linear Time-Invariant Systems with Inputs, HSCC 2006 Slides

·  G. Frehse, O. Maler, Modeling and Analysis of Switched Buffer Networks using Hybrid Automata, unpublished 2006

·  B. Krogh, J. Kapinski, O.Maler, O. Stursberg, On Systematic Simulation of Open Continuous Systems, HSCC 2003

·  E. Asarin, O. Bournez, T. Dang, O. Maler, A. Pnueli, Effective Synthesis of Switching Controllers for Linear Systems, Proc. of the IEEE 2000

·  E. Asarin, O. Bournez, T. Dang, O. Maler, Reachability Analysis of Piecewise-Linear Dynamical Systems, HSCC 2000

·  T. Dang, O. Maler, Reachability Analysis via Face Lifting, HSCC 1998

·  E. Asarin, O. Maler, A. Pnueli, Reachability Analysis of Dynamical Systems having Piecewise-Constant Derivatives, TCS 1995 Slides

·  O. Maler, Z. Manna A. Pnueli, From Timed to Hybrid Systems, Real-Time: Theory in Practice, LNCS 600, Springer 1992

Timed Systems: Scehduling, Real-Time, Multi-core, Schdeuling under Uncertainty

·  J.-F. Kempf, O. Lebeltel, O. Maler, Formal and Informal Methods for Multi-Core Design Space Exploration, QAPL 2014 Slides

·  P. Tendulkar, P. Poplavko, O. Maler, Symmetry Breaking for Multi-Criteria Mapping and Scheduling on Multicores, FORMATS 2013, Slides

·  J.-F. Kempf, M. Bozga, O. Maler, As Soon as Probable: Optimal Scheduling under Stochastic Uncertainty, TACAS 2013 Slides

·  J.-F. Kempf, M. Bozga, O. Maler, Performance Evaluation of Schedulers in a Probabilistic Setting, FORMATS 2011 Slides

·  J. Legriel, O. Maler, Meeting Deadlines Cheaply, ECRTS 2011

·  O. Maler, K. Larsen, B. Krogh, On Zone-Based Analysis of Duration Probabilistic Automata, Infinity 2010 Slides

·  A. Degorre, O. Maler, On Scheduling Policies for Streams of Structured Jobs, FORMATS 2008

·  P. Caspi, O. Maler, From Control Loops to Real-Time Programs, Handbook of Networked and Embedded Control Systems 2005 Slides

·  Y. Abdeddaïm, E. Asarin, O. Maler, Scheduling with Timed Automata, Theoretical Computer Science 2006

·  Y. Abdeddaïm, O. Maler, Preemptive Job-Shop Scheduling using Stopwatch Automata TACAS 2002

·  B. Krogh, O. Maler, M. Mahfoudh, On Control with Bounded Computational Resources FTRTFT 2002

·  E. Asarin, O. Maler, As Soon as Possible: Time Optimal Control for Timed Automata, HSCC 1999

Timed Systems: General, Synthesis, Timing Analysis, Theory, SMT

·  R. Ben Salah, M. Bozga, O. Maler, Compositional Timing Analysis, EMSOFT 2009. Informal version Slides

·  O. Maler, D. Nickovic, A. Pnueli,  On Synthesizing Controllers from Bounded-Response Properties, CAV 2007 Slides

·  O. Maler, D. Nickovic, A. Pnueli, From MITL to Timed Automata, FORMATS 2006

·  S. Cotton, O. Maler, Fast and Flexible Difference Logic Propagation for  DPLL(T), SAT 2006 Slides

·  R. Ben Salah, M. Bozga, O. Maler, On Interleaving in Timed Automata, CONCUR 2006

·  O. Maler, D. Nickovic, A. Pnueli, Real Time Temporal Logic: Past, Present, Future, FORMATS 2005 Slides

·  O. Maler, A. Pnueli, On Recognizable Timed Languages, FOSSACS 2004 Slides

·  E. Asarin, O. Maler, P. CaspiTimed Regular Expressions, The Journal of the ACM, 2002 

·  E. Asarin, O. Maler, A. Pnueli, On Discretization of Delays in Timed Automata and Digital Circuits, CONCUR 1998

·  O. Maler, A. Pnueli, Timing Analysis of Asynchronous Circuits using Timed Automata, CHARME 1995. (see also)

·  E. Asarin, O. Maler, A. Pnueli, Symbolic Controller Synthesis for Discrete and Timed Systems, Hybrid Systems II 1995. See also [MPS95] and [AMPS98]

Theoretical Computer Science: Automata, Learning, Probabilities, Polyhedra, Optimization

·  O. Maler, A. Srivastav, Double Archive Pareto Local Search, SSCI 2016

·  J. Lanik, O. Maler, On Switching Aware Synthesis for Combinational Circuits, HVC 2015 Slides

·  O. Maler, I.E. Mens, Learning Regular Languages over Large Ordered Alphabets, LMCS 2015 Slides

·  S. Cotton, J. Legriel, O. Maler, On Universal Search Strategies for Multi-Criteria Optimization Using Weighted Sums, CEC 2011

·  J. Legriel, C. Le Guernic, S. Cotton, O. Maler, Approximating the Pareto Front of Multi-Criteria Optimization Problems, TACAS 2010

·  O. Maler, On the Krohn-Rhodes Cascaded Decomposition Theorem, Time for Verification, Essays in Memory of Amir Pnueli, 2010

·  Y. Kesten, O. Maler, M. Marcus, A. Pnueli, E. Shahar, Symbolic Model Checking with Rich Assertional Languages, Theoretical Computer Science 2001

·  O. Bournez, O. Maler, On the Representation of Timed Polyhedra, ICALP 2000

·  O. Bournez, O. Maler, A. Pnueli, Orthogonal Polyhedra: Representation and Computation, HSCC 1999

·  M. Bozga, O. Maler, On the Representation of Probabilities over Structured Domains, CAV 1999 Slides

·  E. Asarin, O. Maler, Achilles and the Tortoise Climbing Up the Arithmetical Hierarchy, J. of Computers and Systems Science 1998

·  A. Bouajjani, J. Esparza, O. Maler, Reachability Analysis of Pushdown Automata: Application to Model-Checking, CONCUR 1997

·  O. Maler, L. Staiger, On Syntactic Congruences for Omega-Languages, Theoretical Computer Science 1997

·  O. Maler, A Decomposition Theorem for Probabilistic Transition Systems, Theoretical Computer Science 1995

·  O. Maler, A. Pnueli, On the Learnability of Infinitary Regular Sets, Information and computation 1995 Slides

·  B. Delyon, O. Maler, On the Effects of Noise and Speed on Computations, Theoretical Computer Science 1994

·  O. Maler, A. Pnueli, On the Cascaded Decomposition of Automata, its Complexity and Application to Logic, unpublished 1988-1994

Biological Applications

·  O. Maler, Á. Halász, T. Dang, C. Piazza (Eds.), Hybrid Systems Biology, 2016 Preface

·  O. Maler, A. Halasz, O. Lebeltel, O. Maler, Exploring Synthetic Mass Action Models, Hybrid systems Biology, Springer, 2015 Slides

·  E. Pourcelot, N. Mobilia, A. Donze, F. Louis, O. Maler, P. Mossuz, E. Fanchon, JM Moulis, Cellular Iron Regulation in Animals: Need and Use of Suitable Models, 2014

·  S. Stoma, A. Donze, F. Bertaux, O. Maler, G. Batt, STL-based analysis of TRAIL-induced apoptosis challenges the notion of type I/type II cell line classification, PLoS Comp. Biology 2013

·  A. Donze, E. Fanchon, L.M. Gattepaille, O. Maler, Ph.Tracqui, Robustness Analysis and Behavior Discrimination in Enzymatic Reaction Networks, PLoS One 2011

·  G. Batt, R. Ben Salah, O. Maler, On Timed Models of Gene Networks, FORMATS 2007 Slides


·  O. Maler, Why should we Develop Artificial Worms and How?, unpublished 1990

·  M. Ben-Bassat, O. Maler, A Framework for Control Strategies in Uncertain Inference Networks, UAI 1985

PhD Students

·  Thao Dang, Verification and Synthesis of Hybrid Systems (with E. Asarin), October 2000. Research director CNRS Verimag, Grenoble

·  Yasmina Abdeddaïm, Scheduling with Timed Automata (with E. Asarin), November 2002. Associate professor (MdC), ESIEE, Paris

·  Moez Mahfoudh, On Satisfiability Checking for Difference Logic (with E. Asarin and P. Niebert), May 2003. CTO, Aprelium, Tunis

·  Abdelkarim Kerbaa, Conditional Scheduling Strategies using Timed Automata (with M. Bozga), October 2006

·  Alexandre Donze, Trajectory-Based Verification and Controller Synthesis for Continuous and Hybrid Systems (with T. Dang), June 2007. CTO, Decyphir, Grenoble/Berkeley

·  Ramzi Ben Salah, On Timing Analysis of Large Systems (with M. Bozga), October 2007. Software Engineer, Societe Generale.

·  Dejan Nickovic, Checking Timed and Hybrid Properties, October 2008. Senior researcher, AIT Austria, Vienna

·  Scott Cotton, On some Problems in Satisfiability Solving, June 2009. BB research, Grenoble

·  Colas Le Guernic, Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics (with A. Girard), October 2009 slides. Researcher, DGA, Rennes

·  Aldric Degorre, On some Quantitative Aspects of Formal Languages (with E. Asarin), October 2009. Associate professor (MdC), IRIF, Paris

·  Julien Legriel, Multi-Criteria Optimization and its Application to Multi-Processor Embedded Systems, October 2011 slides. R&D staff engineer, Synopsys, Grenoble

·  Selma Saidi, Optimizing DMA Data Transfers for Embedded Multi-Cores, October 2012 slides. Research engineer, Hamburg University of Technology

·  Jean-Francois Kempf, On Computer-Aided Design-Space Exploration for Multi-Cores (with M. Bozga), October 2012 slides. Senior software engineer, MathWorks, Natick, USA

·  Pranav Tendulkar, Mapping and Scheduling on Multi-core Processors using SMT Solvers (with P. Poplavko), October 2014 slides. Senior embedded software engineer, Intel, Munich

·  Jan Lanik, Power Reduction in Digital Circuits (with F. Rahim), June 2016 slides. Software engineer, OneSpin Solutions, Munich

·  Thomas Ferrere, Assertion and Measurements for Mixed-Signal Simulation, October 2016 slides. Post-doc, IST Austria, Vienna

·  Abhinav Srivastav, On Theoretical and Practical Aspects of Trade-offs in Resource Allocation Problems (with D. Trystram), February 2017 slides. Post-doc, PSL University, Paris

·  Irini-Eleftheria Mens, Learning Regular Languages over Large Alphabets, October 2017 slides New

·  Dogan Ulus, Pattern Matching with Time: Theory and Applications, January 2018 slides New


·  EDA MISTRAL, Mixed Signal Trace Assertion Language

·  ANR EQINOCS, Entropy in Computational Models

·  ANR CADMIDIA, Cadmium and Diabetes


·  Stream Explorer: Deploying Data-Flow Streaming Application on Multi-Cores

Master Students

·  Matthieu Moy, Specification of Timed Behaviors (in French) 2002

·  Abdelkarim Kerbaa, Task Graph Scheduling with Timed Automata 2002

·  Alexandre Donze, Studying a Model of a Hybrid Controller (in French) 2003

·  Ramzi Ben Salah, Circuit Timing Analysis using Timed Automata (in French) 2003

·  Olfa Ben Sik Ali, Simulation of Open Continuous Systems (in French) 2003

·  Scott Cotton, Satisfiability Checking with Difference Constraints, 2005

·  Colas Le Guernic, Efficient Computation of Reachable Sets for Uncertain Linear Systems (in French) 2005

Old Stuff

·  Hybrid Systems Biology (HSB) Vienna, 2014, Madrid, 2015, Grenoble, 2016

·  Workshop: Entropy and information in computational systems (EQINOCS), Paris, May 9-11, 2016

·  Workshop on Monitoring and Testing of Cyber-Physical System (MT-CPS), Vienna 2016, Pittsburgh, 2017

·  BIOSS (Systems Biology), Paris, 23/11/15

·  Paul Caspi: 1944-2012

·  Second Workshop: Toward Systems Biology, Grenoble 30/5-1/6/2011 slides

·  Discrete and Hybrid Methods in Systems Biology, On the Potential Roles of Informatics in Biology (slides, June 2012)

·  Workshop: Frontiers in Analog CAD (FAC) Salt Lake City 2011, Berkeley 2012, Grenoble 2014, Austin 2015, Frankfurt, 2017

·  Workshop: Formal Verification of Analog circuits Edinburgh 2005, Proceedings, Princeton 2008, Grenoble 2009

·  Fighting the Clock Explosion Slides

·  Workshop: Formal and Informal Methods for Correctness and Performance, Marrakech, 2013

·  CAV 2009, Grenoble Proceedings 

·  On some Potential Research Contributions to the Multicore Enterprise (slides)

·  Workshop: Toward Systems Biology, Grenoble 8-10/10/2007

·  Between Control and Software: Workshop in the honor of Paul Caspi, Grenoble 28/9/2007

·  Workshop: Topics in Computation and Control , Santa Barbara 27-28/3/2006

·  The workshop Hybrid Sytems: Computation and Control (HSCC03) Prague, April 2003. Some copies of the proceedings are available at an attractive price here.

·  Workshop on the Theory and Practice of Timed Systems (Grenoble 2002) 

· EU projects: PROSYD property-based system design 2007, CC control and computation 2005, AMETIST on timed systems 2005, VHS verification of hybrid systems 2001 

·  HART'97 Workshop (a workshop on hybrid systems, Grenoble)