PROOF-PAD: An Interactive Proof Generating System Using Natural Deduction. - Thomas A. Henzinger; Hubert Hofbauer (ÖGAI, 1985)

An interleaving model for real-time. - Thomas A. Henzinger; Zohar Manna; Amir Pnueli (Jerusalem Conference on Information Technology, 1990)

Half-Order Modal Logic: How to Prove Real-Time Properties. - Thomas A. Henzinger (PODC, 1990)

Temporal Proof Methodologies for Real-time Systems. - Thomas A. Henzinger; Zohar Manna; Amir Pnueli (POPL, 1991)

Logics and Models of Real Time: A Survey. - Rajeev Alur; Thomas A. Henzinger (REX Workshop, 1991)

Timed Transition Systems. - Thomas A. Henzinger; Zohar Manna; Amir Pnueli (REX Workshop, 1991)

The temporal specification and verification of real-time systems. - Thomas A. Henzinger (1991)

Back to the Future: Towards a Theory of Timed Regular Languages - Rajeev Alur; Thomas A. Henzinger (FOCS, 1992)

Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems. - Rajeev Alur; Costas Courcoubetis; Thomas A. Henzinger; Pei-Hsin Ho (Hybrid Systems, 1992)

Towards Refining Temporal Specifications into Hybrid Systems. - Thomas A. Henzinger; Zohar Manna; Amir Pnueli (Hybrid Systems, 1992)

What Good Are Digital Clocks? - Thomas A. Henzinger; Zohar Manna; Amir Pnueli (ICALP, 1992)

Sooner is Safer Than Later. - Thomas A. Henzinger (Inf. Process. Lett., 1992)

Parametric real-time reasoning. - Rajeev Alur; Thomas A. Henzinger; Moshe Y. Vardi (STOC, 1993)

Verifying Temporal Properties of Systems . By Julian Charles Bradfield. (Birkhauser, 1992 viii+113pp . ISBN 0-8176-3625-0 . $49.50). - Thomas A. Henzinger (SIGACT News, 1993)

Real-Time Logics: Complexity and Expressiveness - Rajeev Alur; Thomas A. Henzinger (Inf. Comput., 1993)

A Determinizable Class of Timed Automata. - Rajeev Alur; Limor Fix; Thomas A. Henzinger (CAV, 1994)

The Observational Power of Clocks. - Rajeev Alur; Costas Courcoubetis; Thomas A. Henzinger (CONCUR, 1994)

Verification Methods for the Divergent Runs of Clock Systems. - Thomas A. Henzinger; Peter W. Kopke (FTRTFT, 1994)

Prooving Safety Properties of Hybrid Systems. - Arjun Kapur; Thomas A. Henzinger; Zohar Manna; Amir Pnueli (FTRTFT, 1994)

A Note on Abstract Interpretation Strategies for Hybrid Automata. - Thomas A. Henzinger; Pei-Hsin Ho (Hybrid Systems, 1994)

HYTECH: The Cornell HYbrid TECHnology Tool. - Thomas A. Henzinger; Pei-Hsin Ho (Hybrid Systems, 1994)

A Really Temporal Logic. - Rajeev Alur; Thomas A. Henzinger (J. ACM, 1994)

Symbolic Model Checking for Real-Time Systems - Thomas A. Henzinger; Xavier Nicollin; Joseph Sifakis; Sergio Yovine (Inf. Comput., 1994)

Temporal Proof Methodologies for Timed Transition Systems - Thomas A. Henzinger; Zohar Manna; Amir Pnueli (Inf. Comput., 1994)

Local Liveness for Compositional Modeling of Fair Reactive Systems. - Rajeev Alur; Thomas A. Henzinger (CAV, 1995)

Algorithmic Analysis of Nonlinear Hybrid Systems. - Thomas A. Henzinger; Pei-Hsin Ho (CAV, 1995)

Using HyTech to Synthesize Control Parameters for a Steam Boiler. - Thomas A. Henzinger; Howard Wong-Toi (Formal Methods for Industrial Applications, 1995)

Computing Simulations on Finite and Infinite Graphs. - Monika Rauch Henzinger; Thomas A. Henzinger; Peter W. Kopke (FOCS, 1995)

Linear Phase-Portrait Approximations for Nonlinear Hybrid Systems. - Thomas A. Henzinger; Howard Wong-Toi (Hybrid Systems, 1995)

Hybrid Automata with Finite Bisimulatioins. - Thomas A. Henzinger (ICALP, 1995)

The Expressive Power of Clocks. - Thomas A. Henzinger; Peter W. Kopke; Howard Wong-Toi (ICALP, 1995)

HyTech: The Next Generation. - Thomas A. Henzinger; Pei-Hsin Ho; Howard Wong-Toi (RTSS, 1995)

A User Guide to HyTech. - Thomas A. Henzinger; Pei-Hsin Ho; Howard Wong-Toi (TACAS, 1995)

The Algorithmic Analysis of Hybrid Systems. - Rajeev Alur; Costas Courcoubetis; Nicolas Halbwachs; Thomas A. Henzinger; Pei-Hsin Ho; Xavier Nicollin; Alfredo Olivero; Joseph Sifakis; Sergio Yovine (Theor. Comput. Sci., 1995)

State Equivalences for Rectangular Hybrid Automata. - Thomas A. Henzinger; Peter W. Kopke (CONCUR, 1996)

A Space-Efficient On-the-fly Algorithm for Real-Time Model Checking. - Thomas A. Henzinger; Orna Kupferman; Moshe Y. Vardi (CONCUR, 1996)

The Theory of Hybrid Automata. - Thomas A. Henzinger (LICS, 1996)

Some Myths About Formal Verification. - Thomas A. Henzinger (ACM Comput. Surv., 1996)

The Benefits of Relaxing Punctuality. - Rajeev Alur; Tomás Feder; Thomas A. Henzinger (J. ACM, 1996)

Automatic Symbolic Verification of Embedded Systems. - Rajeev Alur; Thomas A. Henzinger; Pei-Hsin Ho (IEEE Trans. Software Eng., 1996)

Modularity for Timed and Hybrid Systems. - Rajeev Alur; Thomas A. Henzinger (CONCUR, 1997)

Robust Timed Automata. - Vineet Gupta 001; Thomas A. Henzinger; Radha Jagadeesan (HART, 1997)

From Quantity to Quality. - Thomas A. Henzinger; Orna Kupferman (HART, 1997)

Computing Accumulated Delays in Real-time Systems. - Rajeev Alur; Costas Courcoubetis; Thomas A. Henzinger (Formal Methods Syst. Des., 1997)

Real-Time System = Discrete System + Clock Variables. - Rajeev Alur; Thomas A. Henzinger (Int. J. Softw. Tools Technol. Transf., 1997)

HYTECH: A Model Checker for Hybrid Systems. - Thomas A. Henzinger; Pei-Hsin Ho; Howard Wong-Toi (Int. J. Softw. Tools Technol. Transf., 1997)

MOCHA: Modularity in Model Checking. - Rajeev Alur; Thomas A. Henzinger; Freddy Y. C. Mang; Shaz Qadeer; Sriram K. Rajamani; Serdar Tasiran (CAV, 1998)

From Pre-historic to Post-modern Symbolic Model Checking. - Thomas A. Henzinger; Orna Kupferman; Shaz Qadeer (CAV, 1998)

You Assume, We Guarantee: Methodology and Case Studies. - Thomas A. Henzinger; Shaz Qadeer; Sriram K. Rajamani (CAV, 1998)

Alternating Refinement Relations. - Rajeev Alur; Thomas A. Henzinger; Orna Kupferman; Moshe Y. Vardi (CONCUR, 1998)

It's About Time: Real-Time Logics Reviewed. - Thomas A. Henzinger (CONCUR, 1998)

An Algorithm for the Approximative Analysis of Rectangular Automata. - Jörg Preußig; Stefan Kowalewski; Howard Wong-Toi; Thomas A. Henzinger (FTRTFT, 1998)

Reachability Verification for Hybrid Automata. - Thomas A. Henzinger; Vlad Rusu (HSCC, 1998)

Model Checking Game Properties of Multi-agent Systems (Abstract). - Thomas A. Henzinger (ICALP, 1998)

The Regular Real-Time Languages. - Thomas A. Henzinger; Jean-François Raskin; Pierre-Yves Schobbens (ICALP, 1998)

Computer-aided Verification of Embedded Systems. - Thomas A. Henzinger (IFIP Congress: Fundamentals - Foundations of Computer Science, 1998)

Symbolic Exploration of transition Hierarchies. - Rajeev Alur; Thomas A. Henzinger; Sriram K. Rajamani (TACAS, 1998)

What's Decidable about Hybrid Automata? - Thomas A. Henzinger; Peter W. Kopke; Anuj Puri; Pravin Varaiya (J. Comput. Syst. Sci., 1998)

Algorithmic analysis of nonlinear hybrid systems. - Thomas A. Henzinger; Pei-Hsin Ho; Howard Wong-Toi (IEEE Trans. Autom. Control., 1998)

Finitary Fairness. - Rajeev Alur; Thomas A. Henzinger (ACM Trans. Program. Lang. Syst., 1998)

Assume-Guarantee Refinement Between Different Time Scales. - Thomas A. Henzinger; Shaz Qadeer; Sriram K. Rajamani (CAV, 1999)

Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems. - Thomas A. Henzinger; Shaz Qadeer; Sriram K. Rajamani (CAV, 1999)

Automating Modular Verification. - Rajeev Alur; Luca de Alfaro; Thomas A. Henzinger; Freddy Y. C. Mang (CONCUR, 1999)

Rectangular Hybrid Games. - Thomas A. Henzinger; Benjamin Horowitz; Rupak Majumdar (CONCUR, 1999)

Formal specification and verification of a dataflow processor array. - Thomas A. Henzinger; Xiaojun Liu; Shaz Qadeer; Sriram K. Rajamani (ICCAD, 1999)

Introduction. - Rajeev Alur; Thomas A. Henzinger (Formal Methods Syst. Des., 1999)

Reactive Modules. - Rajeev Alur; Thomas A. Henzinger (Formal Methods Syst. Des., 1999)

Event-Clock Automata: A Determinizable Class of Timed Automata. - Rajeev Alur; Limor Fix; Thomas A. Henzinger (Theor. Comput. Sci., 1999)

Discrete-Time Control for Rectangular Hybrid Automata. - Thomas A. Henzinger; Peter W. Kopke (Theor. Comput. Sci., 1999)

Detecting Errors Before Reaching Them. - Luca de Alfaro; Thomas A. Henzinger; Freddy Y. C. Mang (CAV, 2000)

The Control of Synchronous Systems. - Luca de Alfaro; Thomas A. Henzinger; Freddy Y. C. Mang (CONCUR, 2000)

Beyond HYTECH: Hybrid Systems Analysis Using Interval Numerical Methods. - Thomas A. Henzinger; Benjamin Horowitz; Rupak Majumdar; Howard Wong-Toi (HSCC, 2000)

Robust Undecidability of Timed and Hybrid Systems. - Thomas A. Henzinger; Jean-François Raskin (HSCC, 2000)

Decomposing Refinement Proofs Using Assume-Guarantee Reasoning. - Thomas A. Henzinger; Shaz Qadeer; Sriram K. Rajamani (ICCAD, 2000)

Masaccio: A Formal Model for Embedded Components. - Thomas A. Henzinger (IFIP TCS, 2000)

Concurrent Omega-Regular Games. - Luca de Alfaro; Thomas A. Henzinger (LICS, 2000)

Abstract Interpretation of Game Properties. - Thomas A. Henzinger; Rupak Majumdar; Freddy Y. C. Mang; Jean-François Raskin (SAS, 2000)

A Classification of Symbolic Transition Systems. - Thomas A. Henzinger; Rupak Majumdar (STACS, 2000)

Symbolic Model Checking for Rectangular Hybrid Systems. - Thomas A. Henzinger; Rupak Majumdar (TACAS, 2000)

Fair Bisimulation. - Thomas A. Henzinger; Sriram K. Rajamani (TACAS, 2000)

Exploiting Design Structure in Model Checking. - Thomas A. Henzinger (MTCS, 2000)

Discrete abstractions of hybrid systems. - Rajeev Alur; Thomas A. Henzinger; Gerardo Lafferriere; George J. Pappas (Proc. IEEE, 2000)

New directions in computer-aided verification. - Thomas A. Henzinger (ACM SIGSOFT Softw. Eng. Notes, 2000)

Some lessons from the HYTECH experience. - Thomas A. Henzinger; Jörg Preußig; Howard Wong-Toi (CDC, 2001)

Compositional Methods for Probabilistic Systems. - Luca de Alfaro; Thomas A. Henzinger; Ranjit Jhala (CONCUR, 2001)

Symbolic Algorithms for Infinite-State Games. - Luca de Alfaro; Thomas A. Henzinger; Rupak Majumdar (CONCUR, 2001)

The Control of Synchronous Systems, Part II. - Luca de Alfaro; Thomas A. Henzinger; Freddy Y. C. Mang (CONCUR, 2001)

Interface Theories for Component-Based Design. - Luca de Alfaro; Thomas A. Henzinger (EMSOFT, 2001)

Assume-Guarantee Reasoning for Hierarchical Hybrid Systems. - Thomas A. Henzinger; Marius Minea; Vinayak S. Prabhu (HSCC, 2001)

Hybrid Systems Applications: An Oxymoron? - Alberto L. Sangiovanni-Vincentelli; Thomas A. Henzinger; Bruce H. Krogh; Oded Maler; Manfred Morari; Costas C. Pantelides; George J. Pappas; Tunc Simsec; Janos Sztipanovits; Stavros Tripakis (HSCC, 2001)

JMOCHA: A Model Checking Tool that Exploits Design Structure. - Rajeev Alur; Luca de Alfaro; Radu Grosu; Thomas A. Henzinger; M. Kang; Christoph M. Kirsch; Rupak Majumdar; Freddy Y. C. Mang; Bow-Yaw Wang (ICSE, 2001)

From Verification to Control: Dynamic Programs for Omega-Regular Objectives. - Luca de Alfaro; Thomas A. Henzinger; Rupak Majumdar (LICS, 2001)

Embedded Control Systems Development with Giotto. - Thomas A. Henzinger; Benjamin Horowitz; Christoph Meyer Kirsch (OM@PLDI, 2001)

Interface automata. - Luca de Alfaro; Thomas A. Henzinger (ESEC / SIGSOFT FSE, 2001)

MCWEB: A Model-Checking Tool for Web Site Debugging. - Luca de Alfaro; Thomas A. Henzinger; Freddy Y. C. Mang (WWW Posters, 2001)

Partial-Order Reduction in Symbolic State-Space Exploration. - Rajeev Alur; Robert K. Brayton; Thomas A. Henzinger; Shaz Qadeer; Sriram K. Rajamani (Formal Methods Syst. Des., 2001)

Interface Compatibility Checking for Software Modules. - Arindam Chakrabarti; Luca de Alfaro; Thomas A. Henzinger; Marcin Jurdzinski; Freddy Y. C. Mang (CAV, 2002)

Synchronous and Bidirectional Component Interfaces. - Arindam Chakrabarti; Luca de Alfaro; Thomas A. Henzinger; Freddy Y. C. Mang (CAV, 2002)

The Symbolic Approach to Hybrid Systems. - Thomas A. Henzinger (CAV, 2002)

Temporal-Safety Proofs for Systems Code. - Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar; George C. Necula; Grégoire Sutre; Westley Weimer (CAV, 2002)

Trading Probability for Fairness. - Marcin Jurdzinski; Orna Kupferman; Thomas A. Henzinger (CSL, 2002)

Timed Interfaces. - Luca de Alfaro; Thomas A. Henzinger; Mariëlle Stoelinga (EMSOFT, 2002)

Time-Safety Checking for Embedded Programs. - Thomas A. Henzinger; Christoph M. Kirsch; Rupak Majumdar; Slobodan Matic (EMSOFT, 2002)

A Giotto-Based Helicopter Control System. - Christoph M. Kirsch; Marco A. A. Sanvido; Thomas A. Henzinger; Wolfgang Pree (EMSOFT, 2002)

A Comparison of Control Problems for Timed and Hybrid Systems. - Franck Cassez; Thomas A. Henzinger; Jean-François Raskin (HSCC, 2002)

From Models to Code: The Missing Link in Embedded Software. - Thomas A. Henzinger (HSCC, 2002)

Synthesis of Uninitialized Systems. - Thomas A. Henzinger; Sriram C. Krishnan; Orna Kupferman; Freddy Y. C. Mang (ICALP, 2002)

Convertibility verification and converter synthesis: two faces of the same coin. - Roberto Passerone; Luca de Alfaro; Thomas A. Henzinger; Alberto L. Sangiovanni-Vincentelli (ICCAD, 2002)

Lazy abstraction. - Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar; Grégoire Sutre (POPL, 2002)

Fair Simulation. - Thomas A. Henzinger; Orna Kupferman; Sriram K. Rajamani (Inf. Comput., 2002)

Alternating-time temporal logic. - Rajeev Alur; Thomas A. Henzinger; Orna Kupferman (J. ACM, 2002)

Axioms for real-time logics. - Pierre-Yves Schobbens; Jean-François Raskin; Thomas A. Henzinger (Theor. Comput. Sci., 2002)

An assume-guarantee rule for checking simulation. - Thomas A. Henzinger; Shaz Qadeer; Sriram K. Rajamani; Serdar Tasiran (ACM Trans. Program. Lang. Syst., 2002)

Model Checking: From Hardware to Software. - Thomas A. Henzinger (APLAS, 2003)

Extreme Model Checking. - Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar; Marco A. A. Sanvido (Verification: Theory and Practice, 2003)

Thread-Modular Abstraction Refinement. - Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar; Shaz Qadeer (CAV, 2003)

The Element of Surprise in Timed Games. - Luca de Alfaro; Marco Faella; Thomas A. Henzinger; Rupak Majumdar; Mariëlle Stoelinga (CONCUR, 2003)

Simple Stochastic Parity Games. - Krishnendu Chatterjee; Marcin Jurdzinski; Thomas A. Henzinger (CSL, 2003)

Resource Interfaces. - Arindam Chakrabarti; Luca de Alfaro; Thomas A. Henzinger; Mariëlle Stoelinga (EMSOFT, 2003)

Schedule-Carrying Code. - Thomas A. Henzinger; Christoph M. Kirsch; Slobodan Matic (EMSOFT, 2003)

Discounting the Future in Systems Theory. - Luca de Alfaro; Thomas A. Henzinger; Rupak Majumdar (ICALP, 2003)

Counterexample-Guided Control. - Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar (ICALP, 2003)

Software Verification with BLAST. - Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar; Grégoire Sutre (SPIN, 2003)

On the Universal and Existential Fragments of the µ-Calculus. - Thomas A. Henzinger; Orna Kupferman; Rupak Majumdar (TACAS, 2003)

Automata for Specifying Component Interfaces. - Thomas A. Henzinger (CIAA, 2003)

From Pre-Historic to Post-Modern Symbolic Model Checking. - Thomas A. Henzinger; Orna Kupferman; Shaz Qadeer (Formal Methods Syst. Des., 2003)

Giotto: a time-triggered language for embedded programming. - Thomas A. Henzinger; Benjamin Horowitz; Christoph M. Kirsch (Proc. IEEE, 2003)

Embedded Software: Better Models, Better Code. - Thomas A. Henzinger (ICATPN, 2004)

Rich Interfaces for Software Modules. - Thomas A. Henzinger (ECOOP, 2004)

A typed assembly language for real-time programs. - Thomas A. Henzinger; Christoph M. Kirsch (EMSOFT, 2004)

Event-Driven Programming with Logical Execution Times. - Arkadeb Ghosal; Thomas A. Henzinger; Christoph M. Kirsch; Marco A. A. Sanvido (HSCC, 2004)

Generating Tests from Counterexamples. - Dirk Beyer 001; Adam Chlipala; Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar (ICSE, 2004)

An Eclipse Plug-in for Model Checking. - Dirk Beyer 001; Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar (IWPC, 2004)

Invited talk: the blast query language for software verification. - Dirk Beyer 001; Adam Chlipala; Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar (PEPM, 2004)

Race checking by context inference. - Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar (PLDI, 2004)

Trading Memory for Randomness. - Krishnendu Chatterjee; Luca de Alfaro; Thomas A. Henzinger (QEST, 2004)

The Blast Query Language for Software Verification.. - Dirk Beyer 001; Adam Chlipala; Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar (SAS, 2004)

Quantitative stochastic parity games. - Krishnendu Chatterjee; Marcin Jurdzinski; Thomas A. Henzinger (SODA, 2004)

Stack size analysis for interrupt-driven programs. - Krishnendu Chatterjee; Di Ma; Rupak Majumdar; Tian Zhao 002; Thomas A. Henzinger; Jens Palsberg (Inf. Comput., 2004)

Verifying Quantitative Properties Using Bound Functions. - Arindam Chakrabarti; Krishnendu Chatterjee; Thomas A. Henzinger; Orna Kupferman; Rupak Majumdar (CHARME, 2005)

Checking Memory Safety with Blast. - Dirk Beyer 001; Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar (FASE, 2005)

Automatic Rectangular Refinement of Affine Hybrid Systems. - Laurent Doyen 001; Thomas A. Henzinger; Jean-François Raskin (FORMATS, 2005)

Quantifying Similarities Between Timed Systems. - Thomas A. Henzinger; Rupak Majumdar; Vinayak S. Prabhu (FORMATS, 2005)

Semiperfect-Information Games. - Krishnendu Chatterjee; Thomas A. Henzinger (FSTTCS, 2005)

The Complexity of Stochastic Rabin and Streett Games'. - Krishnendu Chatterjee; Luca de Alfaro; Thomas A. Henzinger (ICALP, 2005)

Composable code generation for distributed giotto. - Thomas A. Henzinger; Christoph M. Kirsch; Slobodan Matic (LCTES, 2005)

Mean-Payoff Parity Games. - Krishnendu Chatterjee; Thomas A. Henzinger; Marcin Jurdzinski (LICS, 2005)

Trading End-to-End Latency for Composability. - Slobodan Matic; Thomas A. Henzinger (RTSS, 2005)

Permissive interfaces. - Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar (ESEC/SIGSOFT FSE, 2005)

The BLAST Software Verification System. - Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar (SPIN, 2005)

Games in system design and verification. - Thomas A. Henzinger (TARK, 2005)

Counterexample-guided Planning. - Krishnendu Chatterjee; Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar (UAI, 2005)

A programmable microkernel for real-time systems. - Christoph M. Kirsch; Marco A. A. Sanvido; Thomas A. Henzinger (VEE, 2005)

Web service interfaces. - Dirk Beyer 001; Arindam Chakrabarti; Thomas A. Henzinger (WWW, 2005)

Model checking discounted temporal properties. - Luca de Alfaro; Marco Faella; Thomas A. Henzinger; Rupak Majumdar; Mariëlle Stoelinga (Theor. Comput. Sci., 2005)

A classification of symbolic transition systems. - Thomas A. Henzinger; Rupak Majumdar; Jean-François Raskin (ACM Trans. Comput. Log., 2005)

Abstract Counterexample-Based Refinement for Powerset Domains. - Roman Manevich; John Field; Thomas A. Henzinger; G. Ramalingam; Mooly Sagiv (Program Analysis and Compilation, 2006)

Lazy Shape Analysis. - Dirk Beyer 001; Thomas A. Henzinger; Grégory Théoduloz (CAV, 2006)

Antichains: A New Algorithm for Checking Universality of Finite Automata. - Martin De Wulf; Laurent Doyen 001; Thomas A. Henzinger; Jean-François Raskin (CAV, 2006)

Strategy Improvement for Stochastic Rabin and Streett Games. - Krishnendu Chatterjee; Thomas A. Henzinger (CONCUR, 2006)

Algorithms for Omega-Regular Games with Imperfect Information, . - Krishnendu Chatterjee; Laurent Doyen 001; Thomas A. Henzinger; Jean-François Raskin (CSL, 2006)

Solving Games Without Determinization. - Thomas A. Henzinger; Nir Piterman (CSL, 2006)

A hierarchical coordination language for interacting real-time tasks. - Arkadeb Ghosal; Alberto L. Sangiovanni-Vincentelli; Christoph M. Kirsch; Thomas A. Henzinger; Daniel T. Iercan (EMSOFT, 2006)

The Embedded Systems Design Challenge. - Thomas A. Henzinger; Joseph Sifakis (FM, 2006)

Timed Alternating-Time Temporal Logic. - Thomas A. Henzinger; Vinayak S. Prabhu (FORMATS, 2006)

Compositional Quantitative Reasoning. - Krishnendu Chatterjee; Luca de Alfaro; Marco Faella; Thomas A. Henzinger; Rupak Majumdar; Mariëlle Stoelinga (QEST, 2006)

Strategy Improvement for Concurrent Reachability Games. - Krishnendu Chatterjee; Luca de Alfaro; Thomas A. Henzinger (QEST, 2006)

An Interface Algebra for Real-Time Components. - Thomas A. Henzinger; Slobodan Matic (IEEE Real Time Technology and Applications Symposium, 2006)

SYNERGY: a new algorithm for property checking. - Bhargav S. Gulavani; Thomas A. Henzinger; Yamini Kannan; Aditya V. Nori; Sriram K. Rajamani (SIGSOFT FSE, 2006)

The complexity of quantitative concurrent parity games. - Krishnendu Chatterjee; Luca de Alfaro; Thomas A. Henzinger (SODA, 2006)

Strategy Improvement and Randomized Subexponential Algorithms for Stochastic Parity Games. - Krishnendu Chatterjee; Thomas A. Henzinger (STACS, 2006)

Markov Decision Processes with Multiple Objectives. - Krishnendu Chatterjee; Rupak Majumdar; Thomas A. Henzinger (STACS, 2006)

Finitary Winning in omega-Regular Games. - Krishnendu Chatterjee; Thomas A. Henzinger (TACAS, 2006)

Executable biology. - Jasmin Fisher; Thomas A. Henzinger (WSC, 2006)

Games with secure equilibria. - Krishnendu Chatterjee; Thomas A. Henzinger; Marcin Jurdzinski (Theor. Comput. Sci., 2006)

On the universal and existential fragments of the mu-calculus. - Thomas A. Henzinger; Orna Kupferman; Rupak Majumdar (Theor. Comput. Sci., 2006)

Algorithms for Interface Synthesis. - Dirk Beyer 001; Thomas A. Henzinger; Vasu Singh (CAV, 2007)

Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis. - Dirk Beyer 001; Thomas A. Henzinger; Grégory Théoduloz (CAV, 2007)

Quantitative Generalizations of Languages. - Thomas A. Henzinger (Developments in Language Theory, 2007)

Generalized Parity Games. - Krishnendu Chatterjee; Thomas A. Henzinger; Nir Piterman (FoSSaCS, 2007)

Minimum-Time Reachability in Timed Games. - Thomas Brihaye; Thomas A. Henzinger; Vinayak S. Prabhu; Jean-François Raskin (ICALP, 2007)

An Application ofWeb-Service Interfaces. - Dirk Beyer 001; Arindam Chakrabarti; Thomas A. Henzinger; Sanjit A. Seshia (ICWS, 2007)

Probabilistic Systems with LimSup and LimInf Objectives. - Krishnendu Chatterjee; Thomas A. Henzinger (ILC, 2007)

Path invariants. - Dirk Beyer 001; Thomas A. Henzinger; Rupak Majumdar; Andrey Rybalchenko (PLDI, 2007)

Games, Time, and Probability: Graph Models for System Design and Analysis. - Thomas A. Henzinger (SOFSEM (1), 2007)

Assume-Guarantee Synthesis. - Krishnendu Chatterjee; Thomas A. Henzinger (TACAS, 2007)

Invariant Synthesis for Combined Theories. - Dirk Beyer 001; Thomas A. Henzinger; Rupak Majumdar; Andrey Rybalchenko (VMCAI, 2007)

Qualitative networks: a symbolic approach to analyze biological signaling networks. - Marc A. Schaub; Thomas A. Henzinger; Jasmin Fisher (BMC Syst. Biol., 2007)

The Discipline of Embedded Systems Design. - Thomas A. Henzinger; Joseph Sifakis (Computer, 2007)

Algorithms for Omega-Regular Games with Imperfect Information. - Jean-François Raskin; Krishnendu Chatterjee; Laurent Doyen 001; Thomas A. Henzinger (Log. Methods Comput. Sci., 2007)

Predictive Modeling of Signaling Crosstalk during C. elegans Vulval Development. - Jasmin Fisher; Nir Piterman; Alex Hajnal; Thomas A. Henzinger (PLoS Comput. Biol., 2007)

The software model checker Blast. - Dirk Beyer 001; Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar (Int. J. Softw. Tools Technol. Transf., 2007)

Concurrent reachability games. - Luca de Alfaro; Thomas A. Henzinger; Orna Kupferman (Theor. Comput. Sci., 2007)

The embedded machine: Predictable, portable real-time code. - Thomas A. Henzinger; Christoph M. Kirsch (ACM Trans. Program. Lang. Syst., 2007)

Strategy Construction for Parity Games with Imperfect Information. - Dietmar Berwanger; Krishnendu Chatterjee; Laurent Doyen 001; Thomas A. Henzinger; Sangram Raje (CONCUR, 2008)

Environment Assumptions for Synthesis. - Krishnendu Chatterjee; Thomas A. Henzinger; Barbara Jobstmann (CONCUR, 2008)

Completeness and Nondeterminism in Model Checking Transactional Memories. - Rachid Guerraoui; Thomas A. Henzinger; Vasu Singh (CONCUR, 2008)

Logical Reliability of Interacting Real-Time Tasks. - Krishnendu Chatterjee; Arkadeb Ghosal; Thomas A. Henzinger; Daniel T. Iercan; Christoph M. Kirsch; Claudio Pinello; Alberto L. Sangiovanni-Vincentelli (DATE, 2008)

Interface theories with component reuse. - Laurent Doyen 001; Thomas A. Henzinger; Barbara Jobstmann; Tatjana Petrov (EMSOFT, 2008)

Bounded Asynchrony: Concurrency for Modeling Cell-Cell Interactions. - Jasmin Fisher; Thomas A. Henzinger; Maria Mateescu; Nir Piterman (FMSB, 2008)

Model-Checking omega-Regular Properties of Interval Markov Chains. - Krishnendu Chatterjee; Koushik Sen; Thomas A. Henzinger (FoSSaCS, 2008)

Trading Infinite Memory for Uniform Randomness in Timed Games. - Krishnendu Chatterjee; Thomas A. Henzinger; Vinayak S. Prabhu (HSCC, 2008)

Controller Synthesis with Budget Constraints. - Krishnendu Chatterjee; Rupak Majumdar; Thomas A. Henzinger (HSCC, 2008)

Program Analysis with Dynamic Precision Adjustment. - Dirk Beyer 001; Thomas A. Henzinger; Grégory Théoduloz (ASE, 2008)

Valigator: A Verification Tool with Bound and Invariant Generation. - Thomas A. Henzinger; Thibaud Hottelier; Laura Kovács (LPAR, 2008)

Model checking transactional memories. - Rachid Guerraoui; Thomas A. Henzinger; Barbara Jobstmann; Vasu Singh (PLDI, 2008)

Proving non-termination. - Ashutosh Gupta 001; Thomas A. Henzinger; Rupak Majumdar; Andrey Rybalchenko; Ru-Gang Xu (POPL, 2008)

Value Iteration. - Krishnendu Chatterjee; Thomas A. Henzinger (25 Years of Model Checking, 2008)

Permissiveness in Transactional Memories. - Rachid Guerraoui; Thomas A. Henzinger; Vasu Singh (DISC, 2008)

Strategy Improvement for Concurrent Safety Games - Krishnendu Chatterjee; Luca de Alfaro; Thomas A. Henzinger (CoRR, 2008)

Algorithms for Büchi Games - Krishnendu Chatterjee; Thomas A. Henzinger; Nir Piterman (CoRR, 2008)

Equivalence of Labeled Markov Chains. - Laurent Doyen 001; Thomas A. Henzinger; Jean-François Raskin (Int. J. Found. Comput. Sci., 2008)

Stochastic limit-average games are in EXPTIME. - Krishnendu Chatterjee; Rupak Majumdar; Thomas A. Henzinger (Int. J. Game Theory, 2008)

Reduction of stochastic parity to stochastic mean-payoff games. - Krishnendu Chatterjee; Thomas A. Henzinger (Inf. Process. Lett., 2008)

Better Quality in Synthesis through Quantitative Objectives. - Roderick Bloem; Krishnendu Chatterjee; Thomas A. Henzinger; Barbara Jobstmann (CAV, 2009)

Software Transactional Memory on Relaxed Memory Models. - Rachid Guerraoui; Thomas A. Henzinger; Vasu Singh (CAV, 2009)

Sliding Window Abstraction for Infinite Markov Chains. - Thomas A. Henzinger; Maria Mateescu; Verena Wolf (CAV, 2009)

Probabilistic Weighted Automata. - Krishnendu Chatterjee; Laurent Doyen 001; Thomas A. Henzinger (CONCUR, 2009)

On relational interfaces. - Stavros Tripakis; Ben Lickly; Thomas A. Henzinger; Edward A. Lee (EMSOFT, 2009)

Alternating Weighted Automata. - Krishnendu Chatterjee; Laurent Doyen 001; Thomas A. Henzinger (FCT, 2009)

Synthesizing robust systems. - Roderick Bloem; Karin Greimel; Thomas A. Henzinger; Barbara Jobstmann (FMCAD, 2009)

A Survey of Stochastic Games with Limsup and Liminf Objectives. - Krishnendu Chatterjee; Laurent Doyen 001; Thomas A. Henzinger (ICALP (2), 2009)

Stochastic Games with Finitary Objectives. - Krishnendu Chatterjee; Thomas A. Henzinger; Florian Horn 001 (MFCS, 2009)

Distributed, Modular HTL. - Thomas A. Henzinger; Christoph M. Kirsch; Eduardo R. B. Marques; Ana Sokolova (RTSS, 2009)

Termination criteria for solving concurrent safety and reachability games. - Krishnendu Chatterjee; Luca de Alfaro; Thomas A. Henzinger (SODA, 2009)

Alpaga: A Tool for Solving Parity Games with Imperfect Information. - Dietmar Berwanger; Krishnendu Chatterjee; Martin De Wulf; Laurent Doyen 001; Thomas A. Henzinger (TACAS, 2009)

The 2008 CAV Award citation. - Randal E. Bryant; Orna Grumberg; Thomas A. Henzinger; Moshe Y. Vardi (Formal Methods Syst. Des., 2009)

Finitary winning in omega-regular games. - Krishnendu Chatterjee; Thomas A. Henzinger; Florian Horn 001 (ACM Trans. Comput. Log., 2009)

FlexPRICE: Flexible Provisioning of Resources in a Cloud Environment. - Thomas A. Henzinger; Anmol V. Singh; Vasu Singh; Thomas Wies; Damien Zufferey (IEEE CLOUD, 2010)

Robustness of Sequential Circuits. - Laurent Doyen 001; Thomas A. Henzinger; Axel Legay; Dejan Nickovic (ACSD, 2010)

Probabilistic Automata on Infinite Words: Decidability and Undecidability Results. - Krishnendu Chatterjee; Thomas A. Henzinger (ATVA, 2010)

Quantitative Simulation Games. - Pavol Cerný; Thomas A. Henzinger; Arjun Radhakrishna (Essays in Memory of Amir Pnueli, 2010)

Robustness in the Presence of Liveness. - Roderick Bloem; Krishnendu Chatterjee; Karin Greimel; Thomas A. Henzinger; Barbara Jobstmann (CAV, 2010)

Gist: A Solver for Probabilistic Games. - Krishnendu Chatterjee; Thomas A. Henzinger; Barbara Jobstmann; Arjun Radhakrishna (CAV, 2010)

Hybrid numerical solution of the chemical master equation. - Thomas A. Henzinger; Linar Mikeev; Maria Mateescu; Verena Wolf (CMSB, 2010)

Mean-Payoff Automaton Expressions. - Krishnendu Chatterjee; Laurent Doyen 001; Herbert Edelsbrunner; Thomas A. Henzinger; Philippe Rannou (CONCUR, 2010)

A marketplace for cloud resources. - Thomas A. Henzinger; Anmol V. Singh; Vasu Singh; Thomas Wies; Damien Zufferey (EMSOFT, 2010)

Shape Refinement through Explicit Heap Analysis. - Dirk Beyer 001; Thomas A. Henzinger; Grégory Théoduloz; Damien Zufferey (FASE, 2010)

Forward Analysis of Depth-Bounded Processes. - Thomas Wies; Damien Zufferey; Thomas A. Henzinger (FoSSaCS, 2010)

Generalized Mean-payoff and Energy Games. - Krishnendu Chatterjee; Laurent Doyen 001; Thomas A. Henzinger; Jean-François Raskin (FSTTCS, 2010)

ABC: Algebraic Bound Computation for Loops. - Régis Blanc; Thomas A. Henzinger; Thibaud Hottelier; Laura Kovács (LPAR (Dakar), 2010)

Aligators for Arrays (Tool Paper). - Thomas A. Henzinger; Thibaud Hottelier; Laura Kovács; Andrey Rybalchenko (LPAR (Yogyakarta), 2010)

Qualitative Analysis of Partially-Observable Markov Decision Processes. - Krishnendu Chatterjee; Laurent Doyen 001; Thomas A. Henzinger (MFCS, 2010)

From Boolean to quantitative notions of correctness. - Thomas A. Henzinger (POPL, 2010)

SABRE: A Tool for Stochastic Analysis of Biochemical Reaction Networks. - Frédéric Didier; Thomas A. Henzinger; Maria Mateescu; Verena Wolf (QEST, 2010)

Transactions in the jungle. - Rachid Guerraoui; Thomas A. Henzinger; Michal Kapalka; Vasu Singh (SPAA, 2010)

Invariant and Type Inference for Matrices. - Thomas A. Henzinger; Thibaud Hottelier; Laura Kovács; Andrei Voronkov (VMCAI, 2010)

Solving the chemical master equation using sliding windows. - Verena Wolf; Rushil Goel; Maria Mateescu; Thomas A. Henzinger (BMC Syst. Biol., 2010)

Synthesis of AMBA AHB from Formal Specification - Yashdeep Godhal; Krishnendu Chatterjee; Thomas A. Henzinger (CoRR, 2010)

Expressiveness and Closure Properties for Quantitative Languages - Krishnendu Chatterjee; Laurent Doyen 001; Thomas A. Henzinger (Log. Methods Comput. Sci., 2010)

Model checking transactional memories. - Rachid Guerraoui; Thomas A. Henzinger; Vasu Singh (Distributed Comput., 2010)

Strategy construction for parity games with imperfect information. - Dietmar Berwanger; Krishnendu Chatterjee; Martin De Wulf; Laurent Doyen 001; Thomas A. Henzinger (Inf. Comput., 2010)

Strategy logic. - Krishnendu Chatterjee; Thomas A. Henzinger; Nir Piterman (Inf. Comput., 2010)

Quantitative languages. - Krishnendu Chatterjee; Laurent Doyen 001; Thomas A. Henzinger (ACM Trans. Comput. Log., 2010)

Quantitative Synthesis for Concurrent Programs. - Pavol Cerný; Krishnendu Chatterjee; Thomas A. Henzinger; Arjun Radhakrishna; Rohit Singh 002 (CAV, 2011)

Propagation models for computing biochemical reaction networks. - Thomas A. Henzinger; Maria Mateescu (CMSB, 2011)

Dynamic Reactive Modules. - Jasmin Fisher; Thomas A. Henzinger; Dejan Nickovic; Nir Piterman; Anmol V. Singh; Moshe Y. Vardi (CONCUR, 2011)

The Complexity of Quantitative Information Flow Problems. - Pavol Cerný; Krishnendu Chatterjee; Thomas A. Henzinger (CSF, 2011)

Determinizing Discounted-Sum Automata. - Udi Boker; Thomas A. Henzinger (CSL, 2011)

From boolean to quantitative synthesis. - Pavol Cerný; Thomas A. Henzinger (EMSOFT, 2011)

Scheduling large jobs by abstraction refinement. - Thomas A. Henzinger; Vasu Singh; Thomas Wies; Damien Zufferey (EuroSys, 2011)

Static Scheduling in Clouds. - Thomas A. Henzinger; Anmol V. Singh; Vasu Singh; Thomas Wies; Damien Zufferey (HotCloud, 2011)

The Complexity of Request-Response Games. - Krishnendu Chatterjee; Thomas A. Henzinger; Florian Horn 001 (LATA, 2011)

Quantitative Evaluation of BFT Protocols. - Raluca Halalai; Thomas A. Henzinger; Vasu Singh (QEST, 2011)

Specification-centered robustness. - Roderick Bloem; Krishnendu Chatterjee; Karin Greimel; Thomas A. Henzinger; Barbara Jobstmann (SIES, 2011)

QUASY: Quantitative Synthesis Tool. - Krishnendu Chatterjee; Thomas A. Henzinger; Barbara Jobstmann; Rohit Singh 002 (TACAS, 2011)

Biology as reactivity. - Jasmin Fisher; David Harel; Thomas A. Henzinger (Commun. ACM, 2011)

Timed Parity Games: Complexity and Robustness - Krishnendu Chatterjee; Thomas A. Henzinger; Vinayak S. Prabhu (Log. Methods Comput. Sci., 2011)

The Decidability Frontier for Probabilistic Automata on Infinite Words - Krishnendu Chatterjee; Thomas A. Henzinger; Mathieu Tracol (CoRR, 2011)

Conditional Model Checking - Dirk Beyer 001; Thomas A. Henzinger; M. Erkan Keremoglu; Philipp Wendler (CoRR, 2011)

Verification of STM on relaxed memory models. - Rachid Guerraoui; Thomas A. Henzinger; Vasu Singh (Formal Methods Syst. Des., 2011)

Formalisms for Specifying Markovian Population Models. - Thomas A. Henzinger; Barbara Jobstmann; Verena Wolf (Int. J. Found. Comput. Sci., 2011)

Approximation of event probabilities in noisy cellular processes. - Frédéric Didier; Thomas A. Henzinger; Maria Mateescu; Verena Wolf (Theor. Comput. Sci., 2011)

Qualitative concurrent parity games. - Krishnendu Chatterjee; Luca de Alfaro; Thomas A. Henzinger (ACM Trans. Comput. Log., 2011)

A Theory of Synchronous Relational Interfaces. - Stavros Tripakis; Ben Lickly; Thomas A. Henzinger; Edward A. Lee (ACM Trans. Program. Lang. Syst., 2011)

Delayed Continuous-Time Markov Chains for Genetic Regulatory Circuits. - Calin C. Guet; Ashutosh Gupta 001; Thomas A. Henzinger; Maria Mateescu; Ali Sezgin (CAV, 2012)

Synthesis from incompatible specifications. - Pavol Cerný; Sivakanth Gopi; Thomas A. Henzinger; Arjun Radhakrishna; Nishant Totla (EMSOFT, 2012)

Finite automata with time-delay blocks. - Krishnendu Chatterjee; Thomas A. Henzinger; Vinayak S. Prabhu (EMSOFT, 2012)

Synchronous Interface Theories and Time Triggered Scheduling. - Benoît Delahaye; Uli Fahrenberg; Thomas A. Henzinger; Axel Legay; Dejan Nickovic (FMOODS/FORTE, 2012)

Approximate Determinization of Quantitative Automata. - Udi Boker; Thomas A. Henzinger (FSTTCS, 2012)

Quantitative Reactive Models. - Thomas A. Henzinger (MoDELS, 2012)

Independent Implementability of Viewpoints. - Thomas A. Henzinger; Dejan Nickovic (Monterey Workshop, 2012)

Conditional model checking: a technique to pass information between verifiers. - Dirk Beyer 001; Thomas A. Henzinger; M. Erkan Keremoglu; Philipp Wendler (SIGSOFT FSE, 2012)

Ideal Abstractions for Well-Structured Transition Systems. - Damien Zufferey; Thomas Wies; Thomas A. Henzinger (VMCAI, 2012)

Keynote on "the propagation approach for computing biochemical reaction networks". - Thomas A. Henzinger (WSC, 2012)

Strategy Improvement for Concurrent Reachability and Safety Games - Krishnendu Chatterjee; Luca de Alfaro; Thomas A. Henzinger (CoRR, 2012)

Finite Automata with Time-Delay Blocks (Extended Version) - Krishnendu Chatterjee; Thomas A. Henzinger; Vinayak S. Prabhu (CoRR, 2012)

2011 CAV award announcement. - Moshe Y. Vardi; Thomas A. Henzinger; Rajeev Alur; Marta Z. Kwiatkowska (Formal Methods Syst. Des., 2012)

A survey of stochastic ω-regular games. - Krishnendu Chatterjee; Thomas A. Henzinger (J. Comput. Syst. Sci., 2012)

Separate compilation of hierarchical real-time programs into linear-bounded Embedded Machine code. - Arkadeb Ghosal; Daniel T. Iercan; Christoph M. Kirsch; Thomas A. Henzinger; Alberto L. Sangiovanni-Vincentelli (Sci. Comput. Program., 2012)

Simulation distances. - Pavol Cerný; Thomas A. Henzinger; Arjun Radhakrishna (Theor. Comput. Sci., 2012)

Lumpability abstractions of rule-based systems. - Jérôme Feret; Thomas A. Henzinger; Heinz Koeppl; Tatjana Petrov (Theor. Comput. Sci., 2012)

Efficient Synthesis for Concurrency by Semantics-Preserving Transformations. - Pavol Cerný; Thomas A. Henzinger; Arjun Radhakrishna; Leonid Ryzhyk; Thorsten Tarrach (CAV, 2013)

Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates. - Cezara Dragoi; Ashutosh Gupta 001; Thomas A. Henzinger (CAV, 2013)

Distributed queues in shared memory: multicore performance and scalability through quantitative relaxation. - Andreas Haas; Michael Lippautz; Thomas A. Henzinger; Hannes Payer; Ana Sokolova; Christoph M. Kirsch; Ali Sezgin (Conf. Computing Frontiers, 2013)

From Model Checking to Model Measuring. - Thomas A. Henzinger; Jan Otop (CONCUR, 2013)

Aspect-Oriented Linearizability Proofs. - Thomas A. Henzinger; Ali Sezgin; Viktor Vafeiadis (CONCUR, 2013)

The Ackermann Award 2013. - Anuj Dawar; Thomas A. Henzinger; Damian Niwinski (CSL, 2013)

Distributed synthesis for LTL fragments. - Krishnendu Chatterjee; Thomas A. Henzinger; Jan Otop; Andreas Pavlogiannis (FMCAD, 2013)

Quantitative Fitness Measures for Embedded Systems. - Thomas A. Henzinger (PECCS, 2013)

Quantitative abstraction refinement. - Pavol Cerný; Thomas A. Henzinger; Arjun Radhakrishna (POPL, 2013)

Quantitative relaxation of concurrent data structures. - Thomas A. Henzinger; Christoph M. Kirsch; Hannes Payer; Ali Sezgin; Ana Sokolova (POPL, 2013)

A survey of partial-observation stochastic parity games. - Krishnendu Chatterjee; Laurent Doyen 001; Thomas A. Henzinger (Formal Methods Syst. Des., 2013)

Quantitative reactive modeling and verification. - Thomas A. Henzinger (Comput. Sci. Res. Dev., 2013)

Strategy improvement for concurrent reachability and turn-based stochastic safety games. - Krishnendu Chatterjee; Luca de Alfaro; Thomas A. Henzinger (J. Comput. Syst. Sci., 2013)

Synthesis of AMBA AHB from formal specification: a case study. - Yashdeep Godhal; Krishnendu Chatterjee; Thomas A. Henzinger (Int. J. Softw. Tools Technol. Transf., 2013)

The Propagation Approach for Computing Biochemical Reaction Networks. - Thomas A. Henzinger; Maria Mateescu (IEEE ACM Trans. Comput. Biol. Bioinform., 2013)

Regression-Free Synthesis for Concurrency. - Pavol Cerný; Thomas A. Henzinger; Arjun Radhakrishna; Leonid Ryzhyk; Thorsten Tarrach (CAV, 2014)

Computer-aided verification technology for biology. - Thomas A. Henzinger (FMCAD, 2014)

Lipschitz Robustness of Finite-state Transducers. - Thomas A. Henzinger; Jan Otop; Roopsha Samanta (FSTTCS, 2014)

Model measuring for hybrid systems. - Thomas A. Henzinger; Jan Otop (HSCC, 2014)

Probabilistic programming. - Andrew D. Gordon 001; Thomas A. Henzinger; Aditya V. Nori; Sriram K. Rajamani (FOSE, 2014)

Compositional Specifications for ioco Testing. - Przemyslaw Daca; Thomas A. Henzinger; Willibald Krenn; Dejan Nickovic (ICST, 2014)

Battery transition systems. - Udi Boker; Thomas A. Henzinger; Arjun Radhakrishna (POPL, 2014)

A Logic-Based Framework for Verifying Consensus Algorithms. - Cezara Dragoi; Thomas A. Henzinger; Helmut Veith; Josef Widder; Damien Zufferey (VMCAI, 2014)

Synthesizing robust systems. - Roderick Bloem; Krishnendu Chatterjee; Karin Greimel; Thomas A. Henzinger; Georg Hofferek; Barbara Jobstmann; Bettina Könighofer; Robert Könighofer (Acta Informatica, 2014)

Exact and Approximate Determinization of Discounted-Sum Automata. - Udi Boker; Thomas A. Henzinger (Log. Methods Comput. Sci., 2014)

Abstractions from proofs. - Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar; Kenneth L. McMillan (ACM SIGPLAN Notices, 2014)

Interface simulation distances. - Pavol Cerný; Martin Chmelik; Thomas A. Henzinger; Arjun Radhakrishna (Theor. Comput. Sci., 2014)

Temporal Specifications with Accumulative Values. - Udi Boker; Krishnendu Chatterjee; Thomas A. Henzinger; Orna Kupferman (ACM Trans. Comput. Log., 2014)

Complete Composition Operators for IOCO-Testing Theory. - Nikola Benes; Przemyslaw Daca; Thomas A. Henzinger; Jan Kretínský; Dejan Nickovic (CBSE, 2015)

Segment Abstraction for Worst-Case Execution Time Analysis. - Pavol Cerný; Thomas A. Henzinger; Laura Kovács; Arjun Radhakrishna; Jakob Zwirchmayr (ESOP, 2015)

The Target Discounted-Sum Problem. - Udi Boker; Thomas A. Henzinger; Jan Otop (LICS, 2015)

Succinct Representation of Concurrent Trace Sets. - Ashutosh Gupta 001; Thomas A. Henzinger; Arjun Radhakrishna; Roopsha Samanta; Thorsten Tarrach (POPL, 2015)

The Need for Language Support for Fault-Tolerant Distributed Systems. - Cezara Dragoi; Thomas A. Henzinger; Damien Zufferey (SNAPL, 2015)

Model Checking Gene Regulatory Networks. - Mirco Giacobbe; Calin C. Guet; Ashutosh Gupta 001; Thomas A. Henzinger; Tiago Paixão; Tatjana Petrov (TACAS, 2015)

The equivalence problem for finite automata: technical perspective. - Thomas A. Henzinger; Jean-François Raskin (Commun. ACM, 2015)

Optimizing Solution Quality in Synchronization Synthesis. - Pavol Cerný; Edmund M. Clarke; Thomas A. Henzinger; Arjun Radhakrishna; Leonid Ryzhyk; Roopsha Samanta; Thorsten Tarrach (CoRR, 2015)

Aspect-oriented linearizability proofs. - Soham Chakraborty 001; Thomas A. Henzinger; Ali Sezgin; Viktor Vafeiadis (Log. Methods Comput. Sci., 2015)

Local Linearizability. - Andreas Haas; Thomas A. Henzinger; Andreas Holzer; Christoph M. Kirsch; Michael Lippautz; Hannes Payer; Ali Sezgin; Ana Sokolova; Helmut Veith (CoRR, 2015)

Randomness for free. - Krishnendu Chatterjee; Laurent Doyen 001; Hugo Gimbert; Thomas A. Henzinger (Inf. Comput., 2015)

The complexity of multi-mean-payoff and multi-energy games. - Yaron Velner; Krishnendu Chatterjee; Laurent Doyen 001; Thomas A. Henzinger; Alexander Moshe Rabinovich; Jean-François Raskin (Inf. Comput., 2015)

Measuring and Synthesizing Systems in Probabilistic Environments. - Krishnendu Chatterjee; Thomas A. Henzinger; Barbara Jobstmann; Rohit Singh 002 (J. ACM, 2015)

Theory in practice for system design and verification. - Rajeev Alur; Thomas A. Henzinger; Moshe Y. Vardi (ACM SIGLOG News, 2015)

Guest Editors' Introduction to Special Issue on Computational Methods in Systems Biology. - Ashutosh Gupta 001; Thomas A. Henzinger (ACM Trans. Model. Comput. Simul., 2015)

Array Folds Logic. - Przemyslaw Daca; Thomas A. Henzinger; Andrey Kupriyanov (CAV (2), 2016)

Linear Distances between Markov Chains. - Przemyslaw Daca; Thomas A. Henzinger; Jan Kretínský; Tatjana Petrov (CONCUR, 2016)

Local Linearizability for Concurrent Container-Type Data Structures. - Andreas Haas; Thomas A. Henzinger; Andreas Holzer; Christoph M. Kirsch; Michael Lippautz; Hannes Payer; Ali Sezgin; Ana Sokolova; Helmut Veith (CONCUR, 2016)

Discrete Abstraction of Multiaffine Systems. - Hui Kong 004; Ezio Bartocci; Sergiy Bogomolov; Radu Grosu; Thomas A. Henzinger; Yu Jiang 001; Christian Schilling 001 (HSB, 2016)

Scalable Static Hybridization Methods for Analysis of Nonlinear Systems. - Stanley Bak; Sergiy Bogomolov; Thomas A. Henzinger; Taylor T. Johnson; Pradyot Prakash (HSCC, 2016)

Nested Weighted Limit-Average Automata of Bounded Width. - Krishnendu Chatterjee; Thomas A. Henzinger; Jan Otop (MFCS, 2016)

PSync: a partially synchronous language for fault-tolerant distributed algorithms. - Cezara Dragoi; Thomas A. Henzinger; Damien Zufferey (POPL, 2016)

Quantitative Monitor Automata. - Krishnendu Chatterjee; Thomas A. Henzinger; Jan Otop (SAS, 2016)

Abstraction-driven Concolic Testing. - Przemyslaw Daca; Ashutosh Gupta 001; Thomas A. Henzinger (VMCAI, 2016)

Lipschitz Robustness of Timed I/O Systems. - Thomas A. Henzinger; Jan Otop; Roopsha Samanta (VMCAI, 2016)

Adaptive moment closure for parameter inference of biochemical reaction networks. - Christian Schilling 001; Sergiy Bogomolov; Thomas A. Henzinger; Andreas Podelski; Jakob Ruess (Biosyst., 2016)

Invariant Clusters for Hybrid Systems. - Hui Kong 004; Sergiy Bogomolov; Christian Schilling 001; Yu Jiang 001; Thomas A. Henzinger (CoRR, 2016)

Viewpoints on "Logic activities in Europe", twenty years later. - Luca Aceto; Thomas A. Henzinger; Joost-Pieter Katoen; Wolfgang Thomas; Moshe Y. Vardi (Bull. EATCS, 2016)

The Cost of Exactness in Quantitative Reachability. - Krishnendu Chatterjee; Laurent Doyen 001; Thomas A. Henzinger (Models, Algorithms, Logics and Tools, 2017)

Challenges and Tool Implementation of Hybrid Rapidly-Exploring Random Trees. - Stanley Bak; Sergiy Bogomolov; Thomas A. Henzinger; Aviral Kumar (NSV@CAV, 2017)

Bidirectional Nested Weighted Automata. - Krishnendu Chatterjee; Thomas A. Henzinger; Jan Otop (CONCUR, 2017)

Conic Abstractions for Hybrid Systems. - Sergiy Bogomolov; Mirco Giacobbe; Thomas A. Henzinger; Hui Kong 004 (FORMATS, 2017)

Safety Verification of Nonlinear Hybrid Systems Based on Invariant Clusters. - Hui Kong 004; Sergiy Bogomolov; Christian Schilling 001; Yu Jiang 001; Thomas A. Henzinger (HSCC, 2017)

The quest for average response time. - Thomas A. Henzinger (MEMOCODE, 2017)

Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults. - Guy Avni; Shubham Goel 001; Thomas A. Henzinger; Guillermo Rodríguez-Navas (TACAS (2), 2017)

Counterexample-Guided Refinement of Template Polyhedra. - Sergiy Bogomolov; Goran Frehse; Mirco Giacobbe; Thomas A. Henzinger (TACAS (1), 2017)

Model checking the evolution of gene regulatory networks. - Mirco Giacobbe; Calin C. Guet; Ashutosh Gupta 001; Thomas A. Henzinger; Tiago Paixão; Tatjana Petrov (Acta Informatica, 2017)

From non-preemptive to preemptive scheduling using synchronization synthesis. - Pavol Cerný; Edmund M. Clarke; Thomas A. Henzinger; Arjun Radhakrishna; Leonid Ryzhyk; Roopsha Samanta; Thorsten Tarrach (Formal Methods Syst. Des., 2017)

Preface of the Special Issue in Memoriam Helmut Veith. - Georg Gottlob; Thomas A. Henzinger; Georg Weissenbacher (Formal Methods Syst. Des., 2017)

Quantitative fair simulation games. - Krishnendu Chatterjee; Thomas A. Henzinger; Jan Otop; Yaron Velner (Inf. Comput., 2017)

Edit Distance for Pushdown Automata. - Krishnendu Chatterjee; Thomas A. Henzinger; Rasmus Ibsen-Jensen; Jan Otop (Log. Methods Comput. Sci., 2017)

Nested Weighted Automata. - Krishnendu Chatterjee; Thomas A. Henzinger; Jan Otop (ACM Trans. Comput. Log., 2017)

Faster Statistical Model Checking for Unbounded Temporal Properties. - Przemyslaw Daca; Thomas A. Henzinger; Jan Kretínský; Tatjana Petrov (ACM Trans. Comput. Log., 2017)

Temporal Logics for Multi-Agent Systems. - Thomas A. Henzinger (AAMAS, 2018)

Computing Average Response Time. - Krishnendu Chatterjee; Thomas A. Henzinger; Jan Otop (Principles of Modeling, 2018)

Space-Time Interpolants. - Goran Frehse; Mirco Giacobbe; Thomas A. Henzinger (CAV (1), 2018)

Reachable Set Over-Approximation for Nonlinear Systems Using Piecewise Barrier Tubes. - Hui Kong 004; Ezio Bartocci; Thomas A. Henzinger (CAV (1), 2018)

Synchronizing the Asynchronous. - Bernhard Kragl; Shaz Qadeer; Thomas A. Henzinger (CONCUR, 2018)

The first-order logic of signals: keynote. - Alexey Bakhirkin; Thomas Ferrère; Thomas A. Henzinger; Dejan Nickovic (EMSOFT, 2018)

Monitoring Temporal Logic with Clock Variables. - Adrián Elgyütt; Thomas Ferrère; Thomas A. Henzinger (FORMATS, 2018)

A Theory of Register Monitors. - Thomas Ferrère; Thomas A. Henzinger; N. Ege Saraç (LICS, 2018)

Infinite-Duration Poorman-Bidding Games. - Guy Avni; Thomas A. Henzinger; Rasmus Ibsen-Jensen (WINE, 2018)

Contracts for System Design. - Albert Benveniste; Benoît Caillaud; Dejan Nickovic; Roberto Passerone; Jean-Baptiste Raclet; Philipp Reinkemeier; Alberto L. Sangiovanni-Vincentelli; Werner Damm; Thomas A. Henzinger; Kim G. Larsen (Found. Trends Electron. Des. Autom., 2018)

Introduction to Model Checking. - Edmund M. Clarke; Thomas A. Henzinger; Helmut Veith (Handbook of Model Checking, 2018)

Run-Time Optimization for Learned Controllers Through Quantitative Games. - Guy Avni; Roderick Bloem; Krishnendu Chatterjee; Thomas A. Henzinger; Bettina Könighofer; Stefan Pranger (CAV (1), 2019)

Membership-Based Synthesis of Linear Hybrid Automata. - Miriam García Soto; Thomas A. Henzinger; Christian Schilling 001; Luka Zeleznik (CAV (1), 2019)

Transient Memory in Gene Regulation. - Calin C. Guet; Thomas A. Henzinger; Claudia Igler; Tatjana Petrov; Ali Sezgin (CMSB, 2019)

Long-Run Average Behavior of Vector Addition Systems with States. - Krishnendu Chatterjee; Thomas A. Henzinger; Jan Otop (CONCUR, 2019)

Piecewise Robust Barrier Tubes for Nonlinear Hybrid Systems with Uncertainty. - Hui Kong 004; Ezio Bartocci; Yu Jiang 001; Thomas A. Henzinger (FORMATS, 2019)

Designing Worm-inspired Neural Networks for Interpretable Robotic Control. - Mathias Lechner; Ramin M. Hasani; Manuel Zimmer; Thomas A. Henzinger; Radu Grosu (ICRA, 2019)

Bidding Games on Markov Decision Processes. - Guy Avni; Thomas A. Henzinger; Rasmus Ibsen-Jensen; Petr Novotný 001 (RP, 2019)

Infinite-duration Bidding Games. - Guy Avni; Thomas A. Henzinger; Ventsislav Chonev (J. ACM, 2019)

Quantitative Automata under Probabilistic Semantics. - Krishnendu Chatterjee; Thomas A. Henzinger; Jan Otop (Log. Methods Comput. Sci., 2019)

Continuous-Time Models for System Design and Analysis. - Rajeev Alur; Mirco Giacobbe; Thomas A. Henzinger; Kim G. Larsen; Marius Mikucionis (Computing and Software Science, 2019)

Refinement for Structured Concurrent Programs. - Bernhard Kragl; Shaz Qadeer; Thomas A. Henzinger (CAV (1), 2020)

A Survey of Bidding Games on Graphs (Invited Paper). - Guy Avni; Thomas A. Henzinger (CONCUR, 2020)

Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States. - Krishnendu Chatterjee; Thomas A. Henzinger; Jan Otop (CONCUR, 2020)

Monitoring Event Frequencies. - Thomas Ferrère; Thomas A. Henzinger; Bernhard Kragl (CSL, 2020)

Outside the Box: Abstraction-Based Monitoring of Neural Networks. - Thomas A. Henzinger; Anna Lukina; Christian Schilling 001 (ECAI, 2020)

Formal Methods with a Touch of Magic. - Parand Alizadeh Alamdari; Guy Avni; Thomas A. Henzinger; Anna Lukina (FMCAD, 2020)

Inductive sequentialization of asynchronous programs. - Bernhard Kragl; Constantin Enea; Thomas A. Henzinger; Suha Orhun Mutluergil; Shaz Qadeer (PLDI, 2020)

Monitorability Under Assumptions. - Thomas A. Henzinger; N. Ege Saraç (RV, 2020)

How Many Bits Does it Take to Quantize Your Neural Network? - Mirco Giacobbe; Thomas A. Henzinger; Mathias Lechner (TACAS (2), 2020)

Scalable Verification of Quantized Neural Networks (Technical Report). - Thomas A. Henzinger; Mathias Lechner; Dorde Zikelic (CoRR, 2020)

Neural circuit policies enabling auditable autonomy. - Mathias Lechner; Ramin M. Hasani; Alexander Amini; Thomas A. Henzinger; Daniela Rus; Radu Grosu (Nat. Mach. Intell., 2020)

Dynamic resource allocation games. - Guy Avni; Thomas A. Henzinger; Orna Kupferman (Theor. Comput. Sci., 2020)

Inductive Sequentialization of Asynchronous Programs (Evaluated Artifact). - Bernhard Kragl; Constantin Enea; Thomas A. Henzinger; Suha Orhun Mutluergil; Shaz Qadeer (Zenodo, 2020)

Scalable Verification of Quantized Neural Networks. - Thomas A. Henzinger; Mathias Lechner; Dorde Zikelic (AAAI, 2021)

Synthesis of hybrid automata with affine dynamics from time-series data. - Miriam García Soto; Thomas A. Henzinger; Christian Schilling 001 (HSCC, 2021)

Adversarial Training is Not Ready for Robot Learning. - Mathias Lechner; Ramin M. Hasani; Radu Grosu; Daniela Rus; Thomas A. Henzinger (ICRA, 2021)

Quantitative and Approximate Monitoring. - Thomas A. Henzinger; N. Ege Saraç (LICS, 2021)

Infinite Time Horizon Safety of Bayesian Neural Networks. - Mathias Lechner; Dorde Zikelic; Krishnendu Chatterjee; Thomas A. Henzinger (NeurIPS, 2021)

Into the Unknown: Active Monitoring of Neural Networks. - Anna Lukina; Christian Schilling 001; Thomas A. Henzinger (RV, 2021)

Differential Monitoring. - Fabian Muehlboeck; Thomas A. Henzinger (RV, 2021)

Quantitative Monitoring of Software. - Thomas A. Henzinger (VSTTE, 2021)

Flavours of Sequential Information Flow. - Ezio Bartocci; Thomas Ferrère; Thomas A. Henzinger; Dejan Nickovic; Ana Oliveira da Costa (CoRR, 2021)

GoTube: Scalable Stochastic Verification of Continuous-Depth Models. - Sophie Gruenbacher; Mathias Lechner; Ramin M. Hasani; Daniela Rus; Thomas A. Henzinger; Scott A. Smolka; Radu Grosu (CoRR, 2021)

Bidding mechanisms in graph games. - Guy Avni; Thomas A. Henzinger; Dorde Zikelic (J. Comput. Syst. Sci., 2021)

Determinacy in Discrete-Bidding Infinite-Duration Games. - Milad Aghajohari; Guy Avni; Thomas A. Henzinger (Log. Methods Comput. Sci., 2021)

Long lived transients in gene regulation. - Tatjana Petrov; Claudia Igler; Ali Sezgin; Thomas A. Henzinger; Calin C. Guet (Theor. Comput. Sci., 2021)

GoTube: Scalable Statistical Verification of Continuous-Depth Models. - Sophie A. Gruenbacher; Mathias Lechner; Ramin M. Hasani; Daniela Rus; Thomas A. Henzinger; Scott A. Smolka; Radu Grosu (AAAI, 2022)

Stability Verification in Stochastic Control Systems via Neural Network Supermartingales. - Mathias Lechner; Dorde Zikelic; Krishnendu Chatterjee; Thomas A. Henzinger (AAAI, 2022)

Synthesis of Parametric Hybrid Automata from Time Series. - Miriam García Soto; Thomas A. Henzinger; Christian Schilling 001 (ATVA, 2022)

History-Deterministic Timed Automata. - Thomas A. Henzinger; Karoliina Lehtinen; Patrick Totzke (CONCUR, 2022)

An Updated Survey of Bidding Games on Graphs (Invited Talk). - Guy Avni; Thomas A. Henzinger (MFCS, 2022)

History-Deterministic Timed Automata Are Not Determinizable. - Sougata Bose; Thomas A. Henzinger; Karoliina Lehtinen; Sven Schewe; Patrick Totzke (RP, 2022)

Abstract Monitors for Quantitative Specifications. - Thomas A. Henzinger; Nicolas Mazzocchi; N. Ege Saraç (RV, 2022)

Flavors of Sequential Information Flow. - Ezio Bartocci; Thomas Ferrère; Thomas A. Henzinger; Dejan Nickovic; Ana Oliveira da Costa (VMCAI, 2022)

Learning Stabilizing Policies in Stochastic Control Systems. - Dorde Zikelic; Mathias Lechner; Krishnendu Chatterjee; Thomas A. Henzinger (CoRR, 2022)

Entangled Residual Mappings. - Mathias Lechner; Ramin M. Hasani; Zahra Babaiee; Radu Grosu; Daniela Rus; Thomas A. Henzinger; Sepp Hochreiter (CoRR, 2022)

Are All Vision Models Created Equal? A Study of the Open-Loop to Closed-Loop Causality Gap. - Mathias Lechner; Ramin M. Hasani; Alexander Amini; Tsun-Hsuan Wang; Thomas A. Henzinger; Daniela Rus (CoRR, 2022)

Learning Control Policies for Region Stabilization in Stochastic Systems. - Matin Ansaripour; Mathias Lechner; Dorde Zikelic; Krishnendu Chatterjee; Thomas A. Henzinger (CoRR, 2022)

Quantization-Aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks. - Mathias Lechner; Dorde Zikelic; Krishnendu Chatterjee; Thomas A. Henzinger; Daniela Rus (AAAI, 2023)

Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees. - Dorde Zikelic; Mathias Lechner; Thomas A. Henzinger; Krishnendu Chatterjee (AAAI, 2023)

Learning Provably Stabilizing Neural Controllers for Discrete-Time Stochastic Systems. - Matin Ansaripour; Krishnendu Chatterjee; Thomas A. Henzinger; Mathias Lechner; Dorde Zikelic (ATVA (1), 2023)

Monitoring Algorithmic Fairness. - Thomas A. Henzinger; Mahyar Karimi 001; Konstantin Kueffner; Kaushik Mallik (CAV (2), 2023)

Hypernode Automata. - Ezio Bartocci; Thomas A. Henzinger; Dejan Nickovic; Ana Oliveira da Costa (CONCUR, 2023)

Safety and Liveness of Quantitative Automata. - Udi Boker; Thomas A. Henzinger; Nicolas Mazzocchi; N. Ege Saraç (CONCUR, 2023)

Runtime Monitoring of Dynamic Fairness Properties. - Thomas A. Henzinger; Mahyar Karimi 001; Konstantin Kueffner; Kaushik Mallik (FAccT, 2023)

Binary Decision Diagrams on Modern Hardware. - Samuel Pastva; Thomas A. Henzinger (FMCAD, 2023)

Quantitative Safety and Liveness. - Thomas A. Henzinger; Nicolas Mazzocchi; N. Ege Saraç (FoSSaCS, 2023)

Regular Methods for Operator Precedence Languages. - Thomas A. Henzinger; Pavol Kebis; Nicolas Mazzocchi; N. Ege Saraç (ICALP, 2023)

Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees. - Dorde Zikelic; Mathias Lechner; Abhinav Verma; Krishnendu Chatterjee; Thomas A. Henzinger (NeurIPS, 2023)

Monitoring Hyperproperties with Prefix Transducers. - Marek Chalupa; Thomas A. Henzinger (RV, 2023)

Monitoring Algorithmic Fairness Under Partial Observations. - Thomas A. Henzinger; Konstantin Kueffner; Kaushik Mallik (RV, 2023)

Bubaak: Runtime Monitoring of Program Verifiers - (Competition Contribution). - Marek Chalupa; Thomas A. Henzinger (TACAS (2), 2023)

A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems. - Krishnendu Chatterjee; Thomas A. Henzinger; Mathias Lechner; Dorde Zikelic (TACAS (1), 2023)

Trap spaces of multi-valued networks: definition, computation, and applications. - Van-Giang Trinh; Belaid Benhamou; Thomas A. Henzinger; Samuel Pastva (Bioinform., 2023)

VAMOS: Middleware for Best-Effort Third-Party Monitoring. - Marek Chalupa; Stefanie Muroya Lei; Fabian Muehlboeck; Thomas A. Henzinger (Zenodo, 2023)

Revisiting the Adversarial Robustness-Accuracy Tradeoff in Robot Learning. - Mathias Lechner; Alexander Amini; Daniela Rus; Thomas A. Henzinger (IEEE Robotics Autom. Lett., 2023)

Monitoring Hyperproperties With Prefix Transducers. - Marek Chalupa; Thomas A. Henzinger (Zenodo, 2023)

Into the unknown: active monitoring of neural networks (extended version). - Konstantin Kueffner; Anna Lukina; Christian Schilling 001; Thomas A. Henzinger (Int. J. Softw. Tools Technol. Transf., 2023)

Bidding Games with Charging. - Guy Avni; Ehsan Kafshdar Goharshady; Thomas A. Henzinger; Kaushik Mallik (CONCUR, 2024)

History-Determinism vs Fair Simulation. - Udi Boker; Thomas A. Henzinger; Karoliina Lehtinen; Aditya Prakash 002 (CONCUR, 2024)

Strategic Dominance: A New Preorder for Nondeterministic Processes. - Thomas A. Henzinger; Nicolas Mazzocchi; N. Ege Saraç (CONCUR, 2024)

Abstraction-Based Decision Making for Statistical Properties (Invited Talk). - Filip Cano 001; Thomas A. Henzinger; Bettina Könighofer; Konstantin Kueffner; Kaushik Mallik (FSCD, 2024)

Overparametrization helps offline-to-online generalization of closed-loop control from pixels. - Mathias Lechner; Ramin M. Hasani; Alexander Amini; Tsun-Hsuan Wang; Thomas A. Henzinger; Daniela Rus (ICRA, 2024)

Monitoring Extended Hypernode Logic. - Marek Chalupa; Thomas A. Henzinger; Ana Oliveira da Costa (IFM, 2024)

QuAK: Quantitative Automata Kit. - Marek Chalupa; Thomas A. Henzinger; Nicolas Mazzocchi; N. Ege Saraç (ISoLA (4), 2024)

Information-flow Interfaces and Security Lattices. - Ezio Bartocci; Thomas A. Henzinger; Dejan Nickovic; Ana Oliveira da Costa (CoRR, 2024)

History-deterministic Timed Automata. - Sougata Bose; Thomas A. Henzinger; Karoliina Lehtinen; Sven Schewe; Patrick Totzke (Log. Methods Comput. Sci., 2024)

VAMOS: Middleware for Best-Effort Third-Party Monitoring. - Marek Chalupa; Stefanie Muroya Lei; Fabian Muehlboeck; Thomas A. Henzinger (Zenodo, 2024)

QuAK: Quantitative Automata Kit (artifact). - Marek Chalupa; Thomas A. Henzinger; Nicolas Mazzochci; N. Ege Saraç (Zenodo, 2024)

Fairness Shields: Safeguarding against Biased Decision Makers. - Filip Cano 001; Thomas A. Henzinger; Bettina Könighofer; Konstantin Kueffner; Kaushik Mallik (AAAI, 2025)

Neural Control and Certificate Repair via Runtime Monitoring. - Emily Yu; Dorde Zikelic; Thomas A. Henzinger (AAAI, 2025)

Reminiscences of a Real-Time Researcher. - Thomas A. Henzinger (Real Time and Such, 2025)

Supermartingale Certificates for Quantitative Omega-Regular Verification and Control. - Thomas A. Henzinger; Kaushik Mallik; Pouya Sadeghi; Dorde Zikelic (CAV (2), 2025)

Quantitative Language Automata. - Thomas A. Henzinger; Pavol Kebis; Nicolas Mazzocchi; N. Ege Saraç (CONCUR, 2025)

Predictive Monitoring of Black-Box Dynamical Systems. - Thomas A. Henzinger; Fabian Kresse; Kaushik Mallik; Emily Yu; Djordje Zikelic (L4DC, 2025)

Finding Equilibria: Simpler for Pessimists, Simplest for Optimists. - Léonard Brice; Thomas A. Henzinger; K. S. Thejaswini (MFCS, 2025)

Resolving Nondeterminism with Randomness. - Thomas A. Henzinger; Aditya Prakash 002; K. S. Thejaswini (MFCS, 2025)

Logic Gate Neural Networks are Good for Verification. - Fabian Kresse; Emily Yu; Christoph H. Lampert; Thomas A. Henzinger (NeuS, 2025)

Automating the Analysis of Quantitative Automata with QuAK. - Marek Chalupa; Thomas A. Henzinger; Nicolas Mazzocchi; N. Ege Saraç (TACAS (1), 2025)

Safety and Liveness of Quantitative Properties and Automata. - Udi Boker; Thomas A. Henzinger; Nicolas Mazzocchi; N. Ege Saraç (Log. Methods Comput. Sci., 2025)

Vamos: Middleware for best-effort third-party monitoring. - Marek Chalupa; Fabian Muehlboeck; Stefanie Muroya Lei; Thomas A. Henzinger (Sci. Comput. Program., 2025)

Privacy-Preserving Runtime Verification. - Thomas A. Henzinger; Mahyar Karimi 001; K. S. Thejaswini (CoRR, 2025)

Information-flow interfaces. - Ezio Bartocci; Thomas Ferrère; Thomas A. Henzinger; Dejan Nickovic; Ana Oliveira da Costa (Formal Methods Syst. Des., 2025)

Monitoring Robustness and Individual Fairness. - Ashutosh Gupta 001; Thomas A. Henzinger; Konstantin Kueffner; Kaushik Mallik; David Pape (CoRR, 2025)

Monitoring of Static Fairness. - Thomas A. Henzinger; Mahyar Karimi 001; Konstantin Kueffner; Kaushik Mallik (CoRR, 2025)

Formal Verification of Neural Certificates Done Dynamically. - Thomas A. Henzinger; Konstantin Kueffner; Emily Yu (CoRR, 2025)

Algorithmic Fairness: A Runtime Perspective. - Filip Cano 001; Thomas A. Henzinger; Konstantin Kueffner (CoRR, 2025)

Alignment Monitoring. - Thomas A. Henzinger; Konstantin Kueffner; Vasu Singh; I Sun (CoRR, 2025)

Monitoring Hyperproperties over Observed and Constructed Traces. - Marek Chalupa; Thomas A. Henzinger; Ana Oliveira da Costa (CoRR, 2025)