Thomas A. Henzinger
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
298
Venues
60
Active years
1989–2026
Best venue rank
A*
Where they publish
- A*CAV45 papers
- BCONCUR45 papers
- ATACAS18 papers
- A*LICS17 papers
- Journal PublishedEMSOFT16 papers
- A*ICALP14 papers
- BRV10 papers
- A*POPL10 papers
- BMFCS8 papers
- BCSL8 papers
- A*AAAI7 papers
- BVMCAI7 papers
- BFMCAD6 papers
- A*PLDI6 papers
- A*FOCS5 papers
- BFASE4 papers
- BFOSSACS4 papers
- BSAS4 papers
- ARTSS4 papers
- A*ICRA3 papers
- BATVA3 papers
- A*ICSE3 papers
- BLPAR3 papers
- A*SODA3 papers
- ASTACS3 papers
- AICCAD3 papers
- BFM2 papers
- NationalWSC2 papers
- A*WWW2 papers
- A*STOC2 papers
- A*PODC2 papers
- A*CCS1 paper
- A*KDD1 paper
- NationalSYNASC1 paper
- BFSCD1 paper
- BIFM1 paper
- CISoLA1 paper
- AECAI1 paper
- CMEMOCODE1 paper
- BSAGT1 paper
- AESOP1 paper
- AICST1 paper
- CFORTE1 paper
- AMODELS1 paper
- AEuroSys1 paper
- CLATA1 paper
- BSPAA1 paper
- BFCT1 paper
- ADATE1 paper
- CDLT1 paper
- AICWS1 paper
- BSOFSEM1 paper
- ARTAS1 paper
- AUAI1 paper
- BTARK1 paper
- BVEE1 paper
- AECOOP1 paper
- CPEPM1 paper
- CPPDP1 paper
- BAPLAS1 paper
Papers
298 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2026 | CAV | Decoupled Planning for Multiple Omega-Regular Objectives. | Guy Avni, Thomas A. Henzinger, Kaushik Mallik, Suman Sadhukhan, K. S. Thejaswini |
| 2026 | CAV | Randomise Alone, Reach as a Team. | Lonard Brice, Thomas A. Henzinger, Alipasha Montaseri, Ali Shafiee, K. S. Thejaswini |
| 2026 | CAV | Extending QuAK with Nested Quantitative Automata. | Thomas A. Henzinger, Nicolas Mazzocchi, N. Ege Sara, Harun Yilmaz |
| 2026 | CONCUR | Generalized Bidding Games: Where Bidding and Stochastic Games Meet. | Ali Asadi, Thomas A. Henzinger, Ehsan Kafshdar Goharshady, Pavol Kebis, Kaushik Mallik |
| 2026 | CONCUR | Monitoring Discounted Sum Properties. | Filip Cano, Thomas A. Henzinger, Konstantin Kueffner, N. Ege Sara |
| 2026 | CONCUR | A Look Back at Strategy Logic (Invited Contribution for the Test-of-Time Award). | Krishnendu Chatterjee, Thomas A. Henzinger, Nir Piterman |
| 2026 | FM | Quantitative Monitoring of Signal First-Order Logic. | Marek Chalupa, Thomas A. Henzinger, N. Ege Sara, Emily Yu |
| 2026 | LICS | Dicey Games: Shared Sources of Randomness in Distributed Systems. | Lonard Brice, Thomas A. Henzinger, K. S. Thejaswini |
| 2025 | AAAI | Fairness Shields: Safeguarding against Biased Decision Makers. | Filip Cano, Thomas A. Henzinger, Bettina Knighofer, Konstantin Kueffner, Kaushik Mallik |
| 2025 | AAAI | Neural Control and Certificate Repair via Runtime Monitoring. | Emily Yu, Dorde Zikelic, Thomas A. Henzinger |
| 2025 | CAV | Supermartingale Certificates for Quantitative Omega-Regular Verification and Control. | Thomas A. Henzinger, Kaushik Mallik, Pouya Sadeghi, Dorde Zikelic |
| 2025 | CCS | Privacy-Preserving Runtime Verification. | Thomas A. Henzinger, Mahyar Karimi, K. S. Thejaswini |
| 2025 | CONCUR | Quantitative Language Automata. | Thomas A. Henzinger, Pavol Kebis, Nicolas Mazzocchi, N. Ege Sara |
| 2025 | KDD | Monitoring Robustness and Individual Fairness. | Ashutosh Gupta, Thomas A. Henzinger, Konstantin Kueffner, Kaushik Mallik, David Pape |
| 2025 | MFCS | Finding Equilibria: Simpler for Pessimists, Simplest for Optimists. | Lonard Brice, Thomas A. Henzinger, K. S. Thejaswini |
| 2025 | MFCS | Resolving Nondeterminism with Randomness. | Thomas A. Henzinger, Aditya Prakash, K. S. Thejaswini |
| 2025 | RV | Algorithmic Fairness: A Runtime Perspective. | Filip Cano, Thomas A. Henzinger, Konstantin Kueffner |
| 2025 | RV | Monitoring Hypernode Logic Over Infinite Domains. | Marek Chalupa, Thomas A. Henzinger, Ana Oliveira da Costa |
| 2025 | RV | Alignment Monitoring. | Thomas A. Henzinger, Konstantin Kueffner, Vasu Singh, I Sun |
| 2025 | RV | Formal Verification of Neural Certificates Done Dynamically. | Thomas A. Henzinger, Konstantin Kueffner, Emily Yu |
| 2025 | SYNASC | Neural Certificates. | Thomas A. Henzinger |
| 2025 | TACAS | Automating the Analysis of Quantitative Automata with QuAK. | Marek Chalupa, Thomas A. Henzinger, Nicolas Mazzocchi, N. Ege Sara |
| 2024 | CONCUR | Bidding Games with Charging. | Guy Avni, Ehsan Kafshdar Goharshady, Thomas A. Henzinger, Kaushik Mallik |
| 2024 | CONCUR | History-Determinism vs Fair Simulation. | Udi Boker, Thomas A. Henzinger, Karoliina Lehtinen, Aditya Prakash |
| 2024 | CONCUR | Strategic Dominance: A New Preorder for Nondeterministic Processes. | Thomas A. Henzinger, Nicolas Mazzocchi, N. Ege Sara |
| 2024 | FSCD | Abstraction-Based Decision Making for Statistical Properties (Invited Talk). | Filip Cano, Thomas A. Henzinger, Bettina Knighofer, Konstantin Kueffner, Kaushik Mallik |
| 2024 | ICRA | 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 |
| 2024 | IFM | Monitoring Extended Hypernode Logic. | Marek Chalupa, Thomas A. Henzinger, Ana Oliveira da Costa |
| 2024 | ISoLA | QuAK: Quantitative Automata Kit. | Marek Chalupa, Thomas A. Henzinger, Nicolas Mazzocchi, N. Ege Sara |
| 2023 | AAAI | Quantization-Aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks. | Mathias Lechner, Dorde Zikelic, Krishnendu Chatterjee, Thomas A. Henzinger, Daniela Rus |
| 2023 | AAAI | Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees. | Dorde Zikelic, Mathias Lechner, Thomas A. Henzinger, Krishnendu Chatterjee |
| 2023 | ATVA | Learning Provably Stabilizing Neural Controllers for Discrete-Time Stochastic Systems. | Matin Ansaripour, Krishnendu Chatterjee, Thomas A. Henzinger, Mathias Lechner, Dorde Zikelic |
| 2023 | CAV | Monitoring Algorithmic Fairness. | Thomas A. Henzinger, Mahyar Karimi, Konstantin Kueffner, Kaushik Mallik |
| 2023 | CONCUR | Hypernode Automata. | Ezio Bartocci, Thomas A. Henzinger, Dejan Nickovic, Ana Oliveira da Costa |
| 2023 | CONCUR | Safety and Liveness of Quantitative Automata. | Udi Boker, Thomas A. Henzinger, Nicolas Mazzocchi, N. Ege Sara |
| 2023 | FASE | Vamos: Middleware for Best-Effort Third-Party Monitoring. | Marek Chalupa, Fabian Muehlboeck, Stefanie Muroya Lei, Thomas A. Henzinger |
| 2023 | FMCAD | Binary Decision Diagrams on Modern Hardware. | Samuel Pastva, Thomas A. Henzinger |
| 2023 | FOSSACS | Quantitative Safety and Liveness. | Thomas A. Henzinger, Nicolas Mazzocchi, N. Ege Sara |
| 2023 | ICALP | Regular Methods for Operator Precedence Languages. | Thomas A. Henzinger, Pavol Kebis, Nicolas Mazzocchi, N. Ege Sara |
| 2023 | RV | Monitoring Hyperproperties with Prefix Transducers. | Marek Chalupa, Thomas A. Henzinger |
| 2023 | RV | Monitoring Algorithmic Fairness Under Partial Observations. | Thomas A. Henzinger, Konstantin Kueffner, Kaushik Mallik |
| 2023 | TACAS | Bubaak: Runtime Monitoring of Program Verifiers - (Competition Contribution). | Marek Chalupa, Thomas A. Henzinger |
| 2023 | TACAS | A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems. | Krishnendu Chatterjee, Thomas A. Henzinger, Mathias Lechner, Dorde Zikelic |
| 2022 | AAAI | 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 |
| 2022 | AAAI | Stability Verification in Stochastic Control Systems via Neural Network Supermartingales. | Mathias Lechner, Dorde Zikelic, Krishnendu Chatterjee, Thomas A. Henzinger |
| 2022 | ATVA | Synthesis of Parametric Hybrid Automata from Time Series. | Miriam Garca Soto, Thomas A. Henzinger, Christian Schilling |
| 2022 | CONCUR | History-Deterministic Timed Automata. | Thomas A. Henzinger, Karoliina Lehtinen, Patrick Totzke |
| 2022 | FASE | Information-flow Interfaces. | Ezio Bartocci, Thomas Ferrre, Thomas A. Henzinger, Dejan Nickovic, Ana Oliveira da Costa |
| 2022 | MFCS | An Updated Survey of Bidding Games on Graphs (Invited Talk). | Guy Avni, Thomas A. Henzinger |
| 2022 | RV | Abstract Monitors for Quantitative Specifications. | Thomas A. Henzinger, Nicolas Mazzocchi, N. Ege Sara |
| 2022 | VMCAI | Flavors of Sequential Information Flow. | Ezio Bartocci, Thomas Ferrre, Thomas A. Henzinger, Dejan Nickovic, Ana Oliveira da Costa |
| 2021 | AAAI | Scalable Verification of Quantized Neural Networks. | Thomas A. Henzinger, Mathias Lechner, Dorde Zikelic |
| 2021 | ICRA | Adversarial Training is Not Ready for Robot Learning. | Mathias Lechner, Ramin M. Hasani, Radu Grosu, Daniela Rus, Thomas A. Henzinger |
| 2021 | LICS | Quantitative and Approximate Monitoring. | Thomas A. Henzinger, N. Ege Sara |
| 2021 | RV | Into the Unknown: Active Monitoring of Neural Networks. | Anna Lukina, Christian Schilling, Thomas A. Henzinger |
| 2021 | RV | Differential Monitoring. | Fabian Muehlboeck, Thomas A. Henzinger |
| 2020 | CAV | Refinement for Structured Concurrent Programs. | Bernhard Kragl, Shaz Qadeer, Thomas A. Henzinger |
| 2020 | CONCUR | A Survey of Bidding Games on Graphs (Invited Paper). | Guy Avni, Thomas A. Henzinger |
| 2020 | CONCUR | Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States. | Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop |
| 2020 | CSL | Monitoring Event Frequencies. | Thomas Ferrre, Thomas A. Henzinger, Bernhard Kragl |
| 2020 | ECAI | Outside the Box: Abstraction-Based Monitoring of Neural Networks. | Thomas A. Henzinger, Anna Lukina, Christian Schilling |
| 2020 | FMCAD | Formal Methods with a Touch of Magic. | Parand Alizadeh Alamdari, Guy Avni, Thomas A. Henzinger, Anna Lukina |
| 2020 | PLDI | Inductive sequentialization of asynchronous programs. | Bernhard Kragl, Constantin Enea, Thomas A. Henzinger, Suha Orhun Mutluergil, Shaz Qadeer |
| 2020 | RV | Monitorability Under Assumptions. | Thomas A. Henzinger, N. Ege Sara |
| 2020 | TACAS | How Many Bits Does it Take to Quantize Your Neural Network? | Mirco Giacobbe, Thomas A. Henzinger, Mathias Lechner |
| 2019 | CAV | Run-Time Optimization for Learned Controllers Through Quantitative Games. | Guy Avni, Roderick Bloem, Krishnendu Chatterjee, Thomas A. Henzinger, Bettina Knighofer, Stefan Pranger |
| 2019 | CAV | Membership-Based Synthesis of Linear Hybrid Automata. | Miriam Garca Soto, Thomas A. Henzinger, Christian Schilling, Luka Zeleznik |
| 2019 | CONCUR | Determinacy in Discrete-Bidding Infinite-Duration Games. | Milad Aghajohari, Guy Avni, Thomas A. Henzinger |
| 2019 | CONCUR | Long-Run Average Behavior of Vector Addition Systems with States. | Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop |
| 2019 | ICRA | Designing Worm-inspired Neural Networks for Interpretable Robotic Control. | Mathias Lechner, Ramin M. Hasani, Manuel Zimmer, Thomas A. Henzinger, Radu Grosu |
| 2019 | MFCS | Bidding Mechanisms in Graph Games. | Guy Avni, Thomas A. Henzinger, Dorde Zikelic |
| 2018 | CAV | Space-Time Interpolants. | Goran Frehse, Mirco Giacobbe, Thomas A. Henzinger |
| 2018 | CAV | Reachable Set Over-Approximation for Nonlinear Systems Using Piecewise Barrier Tubes. | Hui Kong, Ezio Bartocci, Thomas A. Henzinger |
| 2018 | CONCUR | Synchronizing the Asynchronous. | Bernhard Kragl, Shaz Qadeer, Thomas A. Henzinger |
| 2018 | EMSOFT | The first-order logic of signals: keynote. | Alexey Bakhirkin, Thomas Ferrre, Thomas A. Henzinger, Dejan Nickovic |
| 2018 | LICS | A Theory of Register Monitors. | Thomas Ferrre, Thomas A. Henzinger, N. Ege Sara |
| 2017 | CAV | Challenges and Tool Implementation of Hybrid Rapidly-Exploring Random Trees. | Stanley Bak, Sergiy Bogomolov, Thomas A. Henzinger, Aviral Kumar |
| 2017 | CONCUR | Infinite-Duration Bidding Games. | Guy Avni, Thomas A. Henzinger, Ventsislav Chonev |
| 2017 | CONCUR | Bidirectional Nested Weighted Automata. | Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop |
| 2017 | MEMOCODE | The quest for average response time. | Thomas A. Henzinger |
| 2017 | TACAS | Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults. | Guy Avni, Shubham Goel, Thomas A. Henzinger, Guillermo Rodrguez-Navas |
| 2017 | TACAS | Counterexample-Guided Refinement of Template Polyhedra. | Sergiy Bogomolov, Goran Frehse, Mirco Giacobbe, Thomas A. Henzinger |
| 2016 | CAV | Array Folds Logic. | Przemyslaw Daca, Thomas A. Henzinger, Andrey Kupriyanov |
| 2016 | CONCUR | Linear Distances between Markov Chains. | Przemyslaw Daca, Thomas A. Henzinger, Jan Kretnsk, Tatjana Petrov |
| 2016 | CONCUR | 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 |
| 2016 | LICS | Quantitative Automata under Probabilistic Semantics. | Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop |
| 2016 | MFCS | Nested Weighted Limit-Average Automata of Bounded Width. | Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop |
| 2016 | POPL | PSync: a partially synchronous language for fault-tolerant distributed algorithms. | Cezara Dragoi, Thomas A. Henzinger, Damien Zufferey |
| 2016 | SAGT | Dynamic Resource Allocation Games. | Guy Avni, Thomas A. Henzinger, Orna Kupferman |
| 2016 | SAS | Quantitative Monitor Automata. | Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop |
| 2016 | TACAS | Faster Statistical Model Checking for Unbounded Temporal Properties. | Przemyslaw Daca, Thomas A. Henzinger, Jan Kretnsk, Tatjana Petrov |
| 2016 | VMCAI | Abstraction-driven Concolic Testing. | Przemyslaw Daca, Ashutosh Gupta, Thomas A. Henzinger |
| 2016 | VMCAI | Lipschitz Robustness of Timed I/O Systems. | Thomas A. Henzinger, Jan Otop, Roopsha Samanta |
| 2015 | CAV | 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 |
| 2015 | ESOP | Segment Abstraction for Worst-Case Execution Time Analysis. | Pavol Cern, Thomas A. Henzinger, Laura Kovcs, Arjun Radhakrishna, Jakob Zwirchmayr |
| 2015 | ICALP | Edit Distance for Pushdown Automata. | Krishnendu Chatterjee, Thomas A. Henzinger, Rasmus Ibsen-Jensen, Jan Otop |
| 2015 | LICS | The Target Discounted-Sum Problem. | Udi Boker, Thomas A. Henzinger, Jan Otop |
| 2015 | LICS | Nested Weighted Automata. | Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop |
| 2015 | POPL | Succinct Representation of Concurrent Trace Sets. | Ashutosh Gupta, Thomas A. Henzinger, Arjun Radhakrishna, Roopsha Samanta, Thorsten Tarrach |
| 2015 | TACAS | Model Checking Gene Regulatory Networks. | Mirco Giacobbe, Calin C. Guet, Ashutosh Gupta, Thomas A. Henzinger, Tiago Paixo, Tatjana Petrov |
| 2014 | CAV | Regression-Free Synthesis for Concurrency. | Pavol Cern, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Thorsten Tarrach |
| 2014 | FMCAD | Computer-aided verification technology for biology. | Thomas A. Henzinger |
| 2014 | ICSE | Probabilistic programming. | Andrew D. Gordon, Thomas A. Henzinger, Aditya V. Nori, Sriram K. Rajamani |
| 2014 | ICST | Compositional Specifications for ioco Testing. | Przemyslaw Daca, Thomas A. Henzinger, Willibald Krenn, Dejan Nickovic |
| 2014 | POPL | Battery transition systems. | Udi Boker, Thomas A. Henzinger, Arjun Radhakrishna |
| 2014 | VMCAI | A Logic-Based Framework for Verifying Consensus Algorithms. | Cezara Dragoi, Thomas A. Henzinger, Helmut Veith, Josef Widder, Damien Zufferey |
| 2013 | CAV | Efficient Synthesis for Concurrency by Semantics-Preserving Transformations. | Pavol Cern, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Thorsten Tarrach |
| 2013 | CAV | Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates. | Cezara Dragoi, Ashutosh Gupta, Thomas A. Henzinger |
| 2013 | CONCUR | From Model Checking to Model Measuring. | Thomas A. Henzinger, Jan Otop |
| 2013 | CONCUR | Aspect-Oriented Linearizability Proofs. | Thomas A. Henzinger, Ali Sezgin, Viktor Vafeiadis |
| 2013 | CSL | The Ackermann Award 2013. | Anuj Dawar, Thomas A. Henzinger, Damian Niwinski |
| 2013 | FMCAD | Distributed synthesis for LTL fragments. | Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop, Andreas Pavlogiannis |
| 2013 | POPL | Quantitative abstraction refinement. | Pavol Cern, Thomas A. Henzinger, Arjun Radhakrishna |
| 2013 | POPL | Quantitative relaxation of concurrent data structures. | Thomas A. Henzinger, Christoph M. Kirsch, Hannes Payer, Ali Sezgin, Ana Sokolova |
| 2012 | CAV | Delayed Continuous-Time Markov Chains for Genetic Regulatory Circuits. | Calin C. Guet, Ashutosh Gupta, Thomas A. Henzinger, Maria Mateescu, Ali Sezgin |
| 2012 | EMSOFT | Synthesis from incompatible specifications. | Pavol Cern, Sivakanth Gopi, Thomas A. Henzinger, Arjun Radhakrishna, Nishant Totla |
| 2012 | EMSOFT | Finite automata with time-delay blocks. | Krishnendu Chatterjee, Thomas A. Henzinger, Vinayak S. Prabhu |
| 2012 | FORTE | Synchronous Interface Theories and Time Triggered Scheduling. | Benot Delahaye, Uli Fahrenberg, Thomas A. Henzinger, Axel Legay, Dejan Nickovic |
| 2012 | MODELS | Quantitative Reactive Models. | Thomas A. Henzinger |
| 2012 | WSC | Keynote on "the propagation approach for computing biochemical reaction networks". | Thomas A. Henzinger |
| 2012 | VMCAI | Ideal Abstractions for Well-Structured Transition Systems. | Damien Zufferey, Thomas Wies, Thomas A. Henzinger |
| 2011 | CAV | Quantitative Synthesis for Concurrent Programs. | Pavol Cern, Krishnendu Chatterjee, Thomas A. Henzinger, Arjun Radhakrishna, Rohit Singh |
| 2011 | CONCUR | Dynamic Reactive Modules. | Jasmin Fisher, Thomas A. Henzinger, Dejan Nickovic, Nir Piterman, Anmol V. Singh, Moshe Y. Vardi |
| 2011 | CSL | Determinizing Discounted-Sum Automata. | Udi Boker, Thomas A. Henzinger |
| 2011 | EMSOFT | From boolean to quantitative synthesis. | Pavol Cern, Thomas A. Henzinger |
| 2011 | EuroSys | Scheduling large jobs by abstraction refinement. | Thomas A. Henzinger, Vasu Singh, Thomas Wies, Damien Zufferey |
| 2011 | LATA | The Complexity of Request-Response Games. | Krishnendu Chatterjee, Thomas A. Henzinger, Florian Horn |
| 2011 | LICS | Temporal Specifications with Accumulative Values. | Udi Boker, Krishnendu Chatterjee, Thomas A. Henzinger, Orna Kupferman |
| 2011 | TACAS | QUASY: Quantitative Synthesis Tool. | Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann, Rohit Singh |
| 2010 | ATVA | Probabilistic Automata on Infinite Words: Decidability and Undecidability Results. | Krishnendu Chatterjee, Thomas A. Henzinger |
| 2010 | CAV | Robustness in the Presence of Liveness. | Roderick Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas A. Henzinger, Barbara Jobstmann |
| 2010 | CAV | Gist: A Solver for Probabilistic Games. | Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann, Arjun Radhakrishna |
| 2010 | CAV | Measuring and Synthesizing Systems in Probabilistic Environments. | Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann, Rohit Singh |
| 2010 | CONCUR | Simulation Distances. | Pavol Cern, Thomas A. Henzinger, Arjun Radhakrishna |
| 2010 | CONCUR | Mean-Payoff Automaton Expressions. | Krishnendu Chatterjee, Laurent Doyen, Herbert Edelsbrunner, Thomas A. Henzinger, Philippe Rannou |
| 2010 | EMSOFT | A marketplace for cloud resources. | Thomas A. Henzinger, Anmol V. Singh, Vasu Singh, Thomas Wies, Damien Zufferey |
| 2010 | FASE | Shape Refinement through Explicit Heap Analysis. | Dirk Beyer, Thomas A. Henzinger, Grgory Thoduloz, Damien Zufferey |
| 2010 | FOSSACS | Forward Analysis of Depth-Bounded Processes. | Thomas Wies, Damien Zufferey, Thomas A. Henzinger |
| 2010 | LPAR | ABC: Algebraic Bound Computation for Loops. | Rgis Blanc, Thomas A. Henzinger, Thibaud Hottelier, Laura Kovcs |
| 2010 | LPAR | Aligators for Arrays (Tool Paper). | Thomas A. Henzinger, Thibaud Hottelier, Laura Kovcs, Andrey Rybalchenko |
| 2010 | MFCS | Randomness for Free. | Krishnendu Chatterjee, Laurent Doyen, Hugo Gimbert, Thomas A. Henzinger |
| 2010 | MFCS | Qualitative Analysis of Partially-Observable Markov Decision Processes. | Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger |
| 2010 | POPL | From Boolean to quantitative notions of correctness. | Thomas A. Henzinger |
| 2010 | SPAA | Transactions in the jungle. | Rachid Guerraoui, Thomas A. Henzinger, Michal Kapalka, Vasu Singh |
| 2010 | VMCAI | Invariant and Type Inference for Matrices. | Thomas A. Henzinger, Thibaud Hottelier, Laura Kovcs, Andrei Voronkov |
| 2009 | CAV | Better Quality in Synthesis through Quantitative Objectives. | Roderick Bloem, Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann |
| 2009 | CAV | Software Transactional Memory on Relaxed Memory Models. | Rachid Guerraoui, Thomas A. Henzinger, Vasu Singh |
| 2009 | CAV | Sliding Window Abstraction for Infinite Markov Chains. | Thomas A. Henzinger, Maria Mateescu, Verena Wolf |
| 2009 | CONCUR | Probabilistic Weighted Automata. | Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger |
| 2009 | EMSOFT | On relational interfaces. | Stavros Tripakis, Ben Lickly, Thomas A. Henzinger, Edward A. Lee |
| 2009 | FCT | Alternating Weighted Automata. | Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger |
| 2009 | FMCAD | Synthesizing robust systems. | Roderick Bloem, Karin Greimel, Thomas A. Henzinger, Barbara Jobstmann |
| 2009 | ICALP | A Survey of Stochastic Games with Limsup and Liminf Objectives. | Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger |
| 2009 | LICS | Expressiveness and Closure Properties for Quantitative Languages. | Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger |
| 2009 | MFCS | Stochastic Games with Finitary Objectives. | Krishnendu Chatterjee, Thomas A. Henzinger, Florian Horn |
| 2009 | SODA | Termination criteria for solving concurrent safety and reachability games. | Krishnendu Chatterjee, Luca de Alfaro, Thomas A. Henzinger |
| 2009 | RTSS | Distributed, Modular HTL. | Thomas A. Henzinger, Christoph M. Kirsch, Eduardo R. B. Marques, Ana Sokolova |
| 2009 | TACAS | Alpaga: A Tool for Solving Parity Games with Imperfect Information. | Dietmar Berwanger, Krishnendu Chatterjee, Martin De Wulf, Laurent Doyen, Thomas A. Henzinger |
| 2008 | CONCUR | Strategy Construction for Parity Games with Imperfect Information. | Dietmar Berwanger, Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, Sangram Raje |
| 2008 | CONCUR | Environment Assumptions for Synthesis. | Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann |
| 2008 | CONCUR | Completeness and Nondeterminism in Model Checking Transactional Memories. | Rachid Guerraoui, Thomas A. Henzinger, Vasu Singh |
| 2008 | CSL | Quantitative Languages. | Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger |
| 2008 | DATE | 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 |
| 2008 | EMSOFT | Interface theories with component reuse. | Laurent Doyen, Thomas A. Henzinger, Barbara Jobstmann, Tatjana Petrov |
| 2008 | FOSSACS | Model-Checking omega-Regular Properties of Interval Markov Chains. | Krishnendu Chatterjee, Koushik Sen, Thomas A. Henzinger |
| 2008 | LPAR | Valigator: A Verification Tool with Bound and Invariant Generation. | Thomas A. Henzinger, Thibaud Hottelier, Laura Kovcs |
| 2008 | PLDI | Model checking transactional memories. | Rachid Guerraoui, Thomas A. Henzinger, Barbara Jobstmann, Vasu Singh |
| 2008 | POPL | Proving non-termination. | Ashutosh Gupta, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko, Ru-Gang Xu |
| 2007 | CAV | Algorithms for Interface Synthesis. | Dirk Beyer, Thomas A. Henzinger, Vasu Singh |
| 2007 | CAV | Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis. | Dirk Beyer, Thomas A. Henzinger, Grgory Thoduloz |
| 2007 | CONCUR | Strategy Logic. | Krishnendu Chatterjee, Thomas A. Henzinger, Nir Piterman |
| 2007 | DLT | Quantitative Generalizations of Languages. | Thomas A. Henzinger |
| 2007 | FOSSACS | Generalized Parity Games. | Krishnendu Chatterjee, Thomas A. Henzinger, Nir Piterman |
| 2007 | ICALP | Minimum-Time Reachability in Timed Games. | Thomas Brihaye, Thomas A. Henzinger, Vinayak S. Prabhu, Jean-Franois Raskin |
| 2007 | ICWS | An Application ofWeb-Service Interfaces. | Dirk Beyer, Arindam Chakrabarti, Thomas A. Henzinger, Sanjit A. Seshia |
| 2007 | PLDI | Path invariants. | Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko |
| 2007 | SOFSEM | Games, Time, and Probability: Graph Models for System Design and Analysis. | Thomas A. Henzinger |
| 2007 | TACAS | Assume-Guarantee Synthesis. | Krishnendu Chatterjee, Thomas A. Henzinger |
| 2007 | VMCAI | Invariant Synthesis for Combined Theories. | Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko |
| 2006 | CAV | Lazy Shape Analysis. | Dirk Beyer, Thomas A. Henzinger, Grgory Thoduloz |
| 2006 | CAV | Antichains: A New Algorithm for Checking Universality of Finite Automata. | Martin De Wulf, Laurent Doyen, Thomas A. Henzinger, Jean-Franois Raskin |
| 2006 | CONCUR | Strategy Improvement for Stochastic Rabin and Streett Games. | Krishnendu Chatterjee, Thomas A. Henzinger |
| 2006 | CSL | Algorithms for Omega-Regular Games with Imperfect Information | Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, Jean-Franois Raskin |
| 2006 | CSL | Solving Games Without Determinization. | Thomas A. Henzinger, Nir Piterman |
| 2006 | EMSOFT | A hierarchical coordination language for interacting real-time tasks. | Arkadeb Ghosal, Alberto L. Sangiovanni-Vincentelli, Christoph M. Kirsch, Thomas A. Henzinger, Daniel T. Iercan |
| 2006 | FM | The Embedded Systems Design Challenge. | Thomas A. Henzinger, Joseph Sifakis |
| 2006 | WSC | Executable biology. | Jasmin Fisher, Thomas A. Henzinger |
| 2006 | SODA | The complexity of quantitative concurrent parity games. | Krishnendu Chatterjee, Luca de Alfaro, Thomas A. Henzinger |
| 2006 | STACS | Strategy Improvement and Randomized Subexponential Algorithms for Stochastic Parity Games. | Krishnendu Chatterjee, Thomas A. Henzinger |
| 2006 | STACS | Markov Decision Processes with Multiple Objectives. | Krishnendu Chatterjee, Rupak Majumdar, Thomas A. Henzinger |
| 2006 | RTAS | An Interface Algebra for Real-Time Components. | Thomas A. Henzinger, Slobodan Matic |
| 2006 | TACAS | Finitary Winning in omega-Regular Games. | Krishnendu Chatterjee, Thomas A. Henzinger |
| 2005 | FASE | Checking Memory Safety with Blast. | Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
| 2005 | ICALP | The Complexity of Stochastic Rabin and Streett Games'. | Krishnendu Chatterjee, Luca de Alfaro, Thomas A. Henzinger |
| 2005 | LICS | Mean-Payoff Parity Games. | Krishnendu Chatterjee, Thomas A. Henzinger, Marcin Jurdzinski |
| 2005 | WWW | Web service interfaces. | Dirk Beyer, Arindam Chakrabarti, Thomas A. Henzinger |
| 2005 | UAI | Counterexample-guided Planning. | Krishnendu Chatterjee, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
| 2005 | RTSS | Trading End-to-End Latency for Composability. | Slobodan Matic, Thomas A. Henzinger |
| 2005 | TARK | Games in system design and verification. | Thomas A. Henzinger |
| 2005 | VEE | A programmable microkernel for real-time systems. | Christoph M. Kirsch, Marco A. A. Sanvido, Thomas A. Henzinger |
| 2004 | ECOOP | Rich Interfaces for Software Modules. | Thomas A. Henzinger |
| 2004 | EMSOFT | A typed assembly language for real-time programs. | Thomas A. Henzinger, Christoph M. Kirsch |
| 2004 | ICSE | Generating Tests from Counterexamples. | Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
| 2004 | LICS | Games with Secure Equilibria. | Krishnendu Chatterjee, Thomas A. Henzinger, Marcin Jurdzinski |
| 2004 | PEPM | Invited talk: the blast query language for software verification. | Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
| 2004 | PLDI | Race checking by context inference. | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
| 2004 | POPL | Abstractions from proofs. | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan |
| 2004 | PPDP | Invited talk: the blast query language for software verification. | Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
| 2004 | SODA | Quantitative stochastic parity games. | Krishnendu Chatterjee, Marcin Jurdzinski, Thomas A. Henzinger |
| 2004 | SAS | The Blast Query Language for Software Verification.. | Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
| 2004 | TACAS | Model Checking Discounted Temporal Properties. | Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, Marille Stoelinga |
| 2003 | APLAS | Model Checking: From Hardware to Software. | Thomas A. Henzinger |
| 2003 | CAV | Thread-Modular Abstraction Refinement. | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Shaz Qadeer |
| 2003 | CONCUR | The Element of Surprise in Timed Games. | Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, Marille Stoelinga |
| 2003 | CSL | Simple Stochastic Parity Games. | Krishnendu Chatterjee, Marcin Jurdzinski, Thomas A. Henzinger |
| 2003 | EMSOFT | Resource Interfaces. | Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, Marille Stoelinga |
| 2003 | EMSOFT | Schedule-Carrying Code. | Thomas A. Henzinger, Christoph M. Kirsch, Slobodan Matic |
| 2003 | ICALP | Discounting the Future in Systems Theory. | Luca de Alfaro, Thomas A. Henzinger, Rupak Majumdar |
| 2003 | ICALP | Counterexample-Guided Control. | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
| 2003 | SAS | Stack Size Analysis for Interrupt-Driven Programs. | Krishnendu Chatterjee, Di Ma, Rupak Majumdar, Tian Zhao, Thomas A. Henzinger, Jens Palsberg |
| 2003 | TACAS | On the Universal and Existential Fragments of the -Calculus. | Thomas A. Henzinger, Orna Kupferman, Rupak Majumdar |
| 2002 | CAV | Interface Compatibility Checking for Software Modules. | Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, Marcin Jurdzinski, Freddy Y. C. Mang |
| 2002 | CAV | Synchronous and Bidirectional Component Interfaces. | Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang |
| 2002 | CAV | The Symbolic Approach to Hybrid Systems. | Thomas A. Henzinger |
| 2002 | CAV | Temporal-Safety Proofs for Systems Code. | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, George C. Necula, Grgoire Sutre, Westley Weimer |
| 2002 | CSL | Trading Probability for Fairness. | Marcin Jurdzinski, Orna Kupferman, Thomas A. Henzinger |
| 2002 | EMSOFT | Timed Interfaces. | Luca de Alfaro, Thomas A. Henzinger, Marille Stoelinga |
| 2002 | EMSOFT | Time-Safety Checking for Embedded Programs. | Thomas A. Henzinger, Christoph M. Kirsch, Rupak Majumdar, Slobodan Matic |
| 2002 | EMSOFT | A Giotto-Based Helicopter Control System. | Christoph M. Kirsch, Marco A. A. Sanvido, Thomas A. Henzinger, Wolfgang Pree |
| 2002 | ICALP | Synthesis of Uninitialized Systems. | Thomas A. Henzinger, Sriram C. Krishnan, Orna Kupferman, Freddy Y. C. Mang |
| 2002 | ICCAD | Convertibility verification and converter synthesis: two faces of the same coin. | Roberto Passerone, Luca de Alfaro, Thomas A. Henzinger, Alberto L. Sangiovanni-Vincentelli |
| 2002 | PLDI | The Embedded Machine: Predictable, Portable Real-Time Code. | Thomas A. Henzinger, Christoph M. Kirsch |
| 2002 | POPL | Lazy abstraction. | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Grgoire Sutre |
| 2001 | CONCUR | Compositional Methods for Probabilistic Systems. | Luca de Alfaro, Thomas A. Henzinger, Ranjit Jhala |
| 2001 | CONCUR | Symbolic Algorithms for Infinite-State Games. | Luca de Alfaro, Thomas A. Henzinger, Rupak Majumdar |
| 2001 | CONCUR | The Control of Synchronous Systems, Part II. | Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang |
| 2001 | EMSOFT | Interface Theories for Component-Based Design. | Luca de Alfaro, Thomas A. Henzinger |
| 2001 | EMSOFT | Giotto: A Time-Triggered Language for Embedded Programming. | Thomas A. Henzinger, Benjamin Horowitz, Christoph M. Kirsch |
| 2001 | ICSE | 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 |
| 2001 | LICS | From Verification to Control: Dynamic Programs for Omega-Regular Objectives. | Luca de Alfaro, Thomas A. Henzinger, Rupak Majumdar |
| 2001 | PLDI | Embedded Control Systems Development with Giotto. | Thomas A. Henzinger, Benjamin Horowitz, Christoph Meyer Kirsch |
| 2001 | WWW | MCWEB: A Model-Checking Tool for Web Site Debugging. | Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang |
| 2000 | CAV | Detecting Errors Before Reaching Them. | Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang |
| 2000 | CONCUR | The Control of Synchronous Systems. | Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang |
| 2000 | ICCAD | Decomposing Refinement Proofs Using Assume-Guarantee Reasoning. | Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani |
| 2000 | LICS | Concurrent Omega-Regular Games. | Luca de Alfaro, Thomas A. Henzinger |
| 2000 | STACS | A Classification of Symbolic Transition Systems. | Thomas A. Henzinger, Rupak Majumdar |
| 2000 | SAS | Abstract Interpretation of Game Properties. | Thomas A. Henzinger, Rupak Majumdar, Freddy Y. C. Mang, Jean-Franois Raskin |
| 2000 | TACAS | Symbolic Model Checking for Rectangular Hybrid Systems. | Thomas A. Henzinger, Rupak Majumdar |
| 2000 | TACAS | Fair Bisimulation. | Thomas A. Henzinger, Sriram K. Rajamani |
| 1999 | CAV | Assume-Guarantee Refinement Between Different Time Scales. | Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani |
| 1999 | CAV | Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems. | Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani |
| 1999 | CONCUR | Automating Modular Verification. | Rajeev Alur, Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang |
| 1999 | CONCUR | Rectangular Hybrid Games. | Thomas A. Henzinger, Benjamin Horowitz, Rupak Majumdar |
| 1999 | ICCAD | Formal specification and verification of a dataflow processor array. | Thomas A. Henzinger, Xiaojun Liu, Shaz Qadeer, Sriram K. Rajamani |
| 1998 | CAV | MOCHA: Modularity in Model Checking. | Rajeev Alur, Thomas A. Henzinger, Freddy Y. C. Mang, Shaz Qadeer, Sriram K. Rajamani, Serdar Tasiran |
| 1998 | CAV | From | Thomas A. Henzinger, Orna Kupferman, Shaz Qadeer |
| 1998 | CAV | You Assume, We Guarantee: Methodology and Case Studies. | Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani |
| 1998 | CONCUR | Alternating Refinement Relations. | Rajeev Alur, Thomas A. Henzinger, Orna Kupferman, Moshe Y. Vardi |
| 1998 | CONCUR | It's About Time: Real-Time Logics Reviewed. | Thomas A. Henzinger |
| 1998 | CONCUR | Axioms for Real-Time Logics. | Jean-Franois Raskin, Pierre-Yves Schobbens, Thomas A. Henzinger |
| 1998 | FMCAD | An Assume-Guarantee Rule for Checking Simulation. | Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani, Serdar Tasiran |
| 1998 | FOCS | Concurrent Reachability Games. | Luca de Alfaro, Thomas A. Henzinger, Orna Kupferman |
| 1998 | ICALP | Model Checking Game Properties of Multi-agent Systems (Abstract). | Thomas A. Henzinger |
| 1998 | ICALP | The Regular Real-Time Languages. | Thomas A. Henzinger, Jean-Franois Raskin, Pierre-Yves Schobbens |
| 1998 | TACAS | Symbolic Exploration of transition Hierarchies. | Rajeev Alur, Thomas A. Henzinger, Sriram K. Rajamani |
| 1997 | CAV | Partial-Order Reduction in Symbolic State Space Exploration. | Rajeev Alur, Robert K. Brayton, Thomas A. Henzinger, Shaz Qadeer, Sriram K. Rajamani |
| 1997 | CAV | HYTECH: A Model Checker for Hybrid Systems. | Thomas A. Henzinger, Pei-Hsin Ho, Howard Wong-Toi |
| 1997 | CONCUR | Modularity for Timed and Hybrid Systems. | Rajeev Alur, Thomas A. Henzinger |
| 1997 | CONCUR | Fair Simulation. | Thomas A. Henzinger, Orna Kupferman, Sriram K. Rajamani |
| 1997 | FOCS | Alternating-time Temporal Logic. | Rajeev Alur, Thomas A. Henzinger, Orna Kupferman |
| 1997 | ICALP | Discrete-Time Control for Rectangular Hybrid Automata. | Thomas A. Henzinger, Peter W. Kopke |
| 1996 | CONCUR | State Equivalences for Rectangular Hybrid Automata. | Thomas A. Henzinger, Peter W. Kopke |
| 1996 | CONCUR | A Space-Efficient On-the-fly Algorithm for Real-Time Model Checking. | Thomas A. Henzinger, Orna Kupferman, Moshe Y. Vardi |
| 1996 | LICS | Reactive Modules. | Rajeev Alur, Thomas A. Henzinger |
| 1996 | LICS | The Theory of Hybrid Automata. | Thomas A. Henzinger |
| 1995 | CAV | Local Liveness for Compositional Modeling of Fair Reactive Systems. | Rajeev Alur, Thomas A. Henzinger |
| 1995 | CAV | Algorithmic Analysis of Nonlinear Hybrid Systems. | Thomas A. Henzinger, Pei-Hsin Ho |
| 1995 | FOCS | Computing Simulations on Finite and Infinite Graphs. | Monika Rauch Henzinger, Thomas A. Henzinger, Peter W. Kopke |
| 1995 | ICALP | Hybrid Automata with Finite Bisimulatioins. | Thomas A. Henzinger |
| 1995 | ICALP | The Expressive Power of Clocks. | Thomas A. Henzinger, Peter W. Kopke, Howard Wong-Toi |
| 1995 | STOC | What's decidable about hybrid automata? | Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, Pravin Varaiya |
| 1995 | RTSS | HyTech: The Next Generation. | Thomas A. Henzinger, Pei-Hsin Ho, Howard Wong-Toi |
| 1995 | TACAS | A User Guide to HyTech. | Thomas A. Henzinger, Pei-Hsin Ho, Howard Wong-Toi |
| 1994 | CAV | A Determinizable Class of Timed Automata. | Rajeev Alur, Limor Fix, Thomas A. Henzinger |
| 1994 | CONCUR | The Observational Power of Clocks. | Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger |
| 1994 | LICS | Finitary Fairness | Rajeev Alur, Thomas A. Henzinger |
| 1993 | CAV | Computing Accumulated Delays in Real-time Systems. | Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger |
| 1993 | STOC | Parametric real-time reasoning. | Rajeev Alur, Thomas A. Henzinger, Moshe Y. Vardi |
| 1993 | RTSS | Automatic Symbolic Verification of Embedded Systems. | Rajeev Alur, Thomas A. Henzinger, Pei-Hsin Ho |
| 1992 | FOCS | Back to the Future: Towards a Theory of Timed Regular Languages | Rajeev Alur, Thomas A. Henzinger |
| 1992 | ICALP | What Good Are Digital Clocks? | Thomas A. Henzinger, Zohar Manna, Amir Pnueli |
| 1992 | LICS | Symbolic Model Checking for Real-time Systems | Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, Sergio Yovine |
| 1991 | PODC | The Benefits of Relaxing Punctuality. | Rajeev Alur, Toms Feder, Thomas A. Henzinger |
| 1991 | POPL | Temporal Proof Methodologies for Real-time Systems. | Thomas A. Henzinger, Zohar Manna, Amir Pnueli |
| 1990 | LICS | Real-time Logics: Complexity and Expressiveness | Rajeev Alur, Thomas A. Henzinger |
| 1990 | PODC | Half-Order Modal Logic: How to Prove Real-Time Properties. | Thomas A. Henzinger |
| 1989 | FOCS | A Really Temporal Logic | Rajeev Alur, Thomas A. Henzinger |