BibSLEIGH — Thomas_A

Travelled to:

1 × Belgium
1 × India
1 × Israel
1 × Russia
1 × The Netherlands
10 × Italy
2 × Cyprus
2 × Finland
2 × Greece
2 × Japan
2 × Norway
2 × Poland
3 × Denmark
3 × France
3 × Hungary
33 × USA
5 × Canada
5 × Germany
5 × Portugal
5 × Spain
6 × Austria
7 × United Kingdom

Collaborated with:

K.Chatterjee R.Majumdar ∅ R.Alur D.Beyer R.Jhala L.d.Alfaro S.K.Rajamani A.Radhakrishna L.Doyen S.Qadeer J.Raskin C.M.Kirsch F.Y.C.Mang M.Jurdzinski O.Kupferman D.Zufferey B.Jobstmann U.Boker P.Cerný G.Théoduloz P.Ho A.Gupta P.W.Kopke H.Wong-Toi J.Otop V.Singh C.Dragoi N.Piterman A.Chlipala P.Daca J.Sifakis T.Tarrach R.Singh A.Rybalchenko T.Wies Z.Manna A.Pnueli R.Bloem R.Guerraoui L.Ryzhyk M.Mateescu M.Giacobbe D.Nickovic L.Kovács M.D.Wulf A.Chakrabarti G.Sutre A.Sezgin C.C.Guet R.Samanta F.Horn V.Wolf K.Sen S.Matic B.Horowitz P.Schobbens L.Fix C.Courcoubetis M.Y.Vardi A.Kupriyanov G.Frehse H.Kong E.Bartocci T.Ferrère B.Kragl R.Ibsen-Jensen W.Krenn M.E.Keremoglu P.Wendler T.Hottelier A.Voronkov T.Brihaye V.S.Prabhu K.L.McMillan S.C.Krishnan A.Puri P.Varaiya X.Nicollin S.Yovine M.G.Soto C.S.0001 L.Zeleznik N.Benes J.Kretínský J.Zwirchmayr H.Veith J.Widder H.Payer A.Sokolova K.Greimel D.Berwanger R.Xu B.S.Gulavani Y.Kannan A.V.Nori M.Faella M.Stoelinga R.K.Brayton T.Paixão T.Petrov D.Ma T.Zhao J.Palsberg G.C.Necula W.Weimer S.Tasiran G.Avni B.Könighofer S.Pranger E.M.Clarke A.Ghosal D.T.Iercan C.Pinello A.L.Sangiovanni-Vincentelli R.Grosu M.Kang B.Wang

Talks about:

system (19) check (18) model (17) time (17) game (17) automata (12) synthesi (11) quantit (11) hybrid (9) abstract (8)

♂ Person: Thomas A. Henzinger

DBLP: Henzinger:Thomas_A=

Facilitated 5 volumes:

PrCo

PrCo

Contributed to:

2015

2014

2013

2012

2011

2010

2009

2008

2007

2008

2007

2006

2005

2004

2003

2002

2001

2000

1999

1998

1997

1996

1995

1994

1993

1992

1991

1990

2016

2018

2019

2020

2016

Wrote 133 papers:

CAV-2015-CernyCHRRST #scheduling #synthesis #using: From Non-preemptive to Preemptive Scheduling Using Synchronization Synthesis (PC, EMC, TAH, AR, LR, RS, TT), pp. 180–197.
CBSE-2015-BenesDHKN #composition #testing: Complete Composition Operators for IOCO — Testing Theory (NB, PD, TAH, JK, DN), pp. 101–110.
ESOP-2015-CernyHKRZ #abstraction #analysis #execution #worst-case: Segment Abstraction for Worst-Case Execution Time Analysis (PC, TAH, LK, AR, JZ), pp. 105–131.
ICALP-v2-2015-ChatterjeeHIO #automaton #distance #edit distance: Edit Distance for Pushdown Automata (KC, TAH, RIJ, JO), pp. 121–133.
LICS-2015-BokerHO #problem: The Target Discounted-Sum Problem (UB, TAH, JO), pp. 750–761.
LICS-2015-ChatterjeeHO #automaton: Nested Weighted Automata (KC, TAH, JO), pp. 725–737.
POPL-2015-GuptaHRST #concurrent #representation #set: Succinct Representation of Concurrent Trace Sets (AG, TAH, AR, RS, TT), pp. 433–444.
TACAS-2015-GiacobbeGGHPP #model checking #network: Model Checking Gene Regulatory Networks (MG, CCG, AG, TAH, TP, TP), pp. 469–483.
CAV-2014-CernyHRRT #concurrent #synthesis: Regression-Free Synthesis for Concurrency (PC, TAH, AR, LR, TT), pp. 568–584.
ICST-2014-DacaHKN #composition #specification #testing: Compositional Specifications for ioco Testing (PD, TAH, WK, DN), pp. 373–382.
POPL-2014-BokerHR: Battery transition systems (UB, TAH, AR), pp. 595–606.
VMCAI-2014-DragoiHVWZ #algorithm #framework #verification: A Logic-Based Framework for Verifying Consensus Algorithms (CD, TAH, HV, JW, DZ), pp. 161–181.
CAV-2013-CernyHRRT #concurrent #performance #semantics #synthesis: Efficient Synthesis for Concurrency by Semantics-Preserving Transformations (PC, TAH, AR, LR, TT), pp. 951–967.
CAV-2013-DragoiGH #automation #concurrent #proving: Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates (CD, AG, TAH), pp. 174–190.
POPL-2013-CernyHR #abstraction #refinement: Quantitative abstraction refinement (PC, TAH, AR), pp. 115–128.
POPL-2013-HenzingerKPSS #concurrent #data type: Quantitative relaxation of concurrent data structures (TAH, CMK, HP, AS, AS), pp. 317–328.
CAV-2012-GuetGHMS #markov #search-based: Delayed Continuous-Time Markov Chains for Genetic Regulatory Circuits (CCG, AG, TAH, MM, AS), pp. 294–309.
FSE-2012-BeyerHKW #model checking #verification: Conditional model checking: a technique to pass information between verifiers (DB, TAH, MEK, PW), p. 57.
MoDELS-2012-Henzinger #modelling: Quantitative Reactive Models (TAH), pp. 1–2.
VMCAI-2012-ZuffereyWH #abstraction: Ideal Abstractions for Well-Structured Transition Systems (DZ, TW, TAH), pp. 445–460.
CAV-2011-CernyCHRS #concurrent #source code #synthesis: Quantitative Synthesis for Concurrent Programs (PC, KC, TAH, AR, RS), pp. 243–259.
CSL-2011-BokerH #automaton: Determinizing Discounted-Sum Automata (UB, TAH), pp. 82–96.
LATA-2011-ChatterjeeHH #complexity #game studies: The Complexity of Request-Response Games (KC, TAH, FH), pp. 227–237.
LICS-2011-BokerCHK #cumulative #specification: Temporal Specifications with Accumulative Values (UB, KC, TAH, OK), pp. 43–52.
TACAS-2011-ChatterjeeHJS #named #synthesis: QUASY: Quantitative Synthesis Tool (KC, TAH, BJ, RS), pp. 267–271.
CAV-2010-BloemCGHJ #liveness #robust: Robustness in the Presence of Liveness (RB, KC, KG, TAH, BJ), pp. 410–424.
CAV-2010-ChatterjeeHJR #game studies #named #probability: Gist: A Solver for Probabilistic Games (KC, TAH, BJ, AR), pp. 665–669.
CAV-2010-ChatterjeeHJS #probability: Measuring and Synthesizing Systems in Probabilistic Environments (KC, TAH, BJ, RS), pp. 380–395.
FASE-2010-BeyerHTZ #analysis #refinement: Shape Refinement through Explicit Heap Analysis (DB, TAH, GT, DZ), pp. 263–277.
FoSSaCS-2010-WiesZH #analysis #bound #process: Forward Analysis of Depth-Bounded Processes (TW, DZ, TAH), pp. 94–108.
POPL-2010-Henzinger #correctness: From Boolean to quantitative notions of correctness (TAH), pp. 157–158.
VMCAI-2010-HenzingerHKV #invariant #matrix #type inference: Invariant and Type Inference for Matrices (TAH, TH, LK, AV), pp. 163–179.
CAV-2009-BloemCHJ #quality #synthesis: Better Quality in Synthesis through Quantitative Objectives (RB, KC, TAH, BJ), pp. 140–156.
CAV-2009-GuerraouiHS #memory management #modelling #transaction: Software Transactional Memory on Relaxed Memory Models (RG, TAH, VS), pp. 321–336.
CAV-2009-HenzingerMW #abstraction #infinity #markov: Sliding Window Abstraction for Infinite Markov Chains (TAH, MM, VW), pp. 337–352.
ICALP-v2-2009-ChatterjeeDH #game studies #overview #probability: A Survey of Stochastic Games with Limsup and Liminf Objectives (KC, LD, TAH), pp. 1–15.
LICS-2009-ChatterjeeDH: Expressiveness and Closure Properties for Quantitative Languages (KC, LD, TAH), pp. 199–208.
TACAS-2009-BerwangerCWDH #game studies #named: Alpaga: A Tool for Solving Parity Games with Imperfect Information (DB, KC, MDW, LD, TAH), pp. 58–61.
ASE-2008-BeyerHT #precise #program analysis: Program Analysis with Dynamic Precision Adjustment (DB, TAH, GT), pp. 29–38.
CSL-2008-ChatterjeeDH: Quantitative Languages (KC, LD, TAH), pp. 385–400.
DATE-2008-ChatterjeeGHIKPS #logic #realtime #reliability: Logical Reliability of Interacting Real-Time Tasks (KC, AG, TAH, DTI, CMK, CP, ALSV), pp. 909–914.
FoSSaCS-2008-ChatterjeeSH #markov #model checking: Model-Checking ω-Regular Properties of Interval Markov Chains (KC, KS, TAH), pp. 302–317.
PLDI-2008-GuerraouiHJS #model checking #transaction: Model checking transactional memories (RG, TAH, BJ, VS), pp. 372–382.
POPL-2008-GuptaHMRX #proving: Proving non-termination (AG, TAH, RM, AR, RGX), pp. 147–158.
CAV-2007-BeyerHS #algorithm #interface #synthesis: Algorithms for Interface Synthesis (DB, TAH, VS), pp. 4–19.
CAV-2007-BeyerHT #configuration management #convergence #model checking #program analysis #verification: Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis (DB, TAH, GT), pp. 504–518.
DLT-2007-Henzinger: Quantitative Generalizations of Languages (TAH), pp. 20–22.
DLT-J-2007-DoyenHR08 #equivalence #markov: Equivalence of Labeled Markov Chains (LD, TAH, JFR), pp. 549–563.
FoSSaCS-2007-ChatterjeeHP #game studies: Generalized Parity Games (KC, TAH, NP), pp. 153–167.
ICALP-2007-BrihayeHPR #game studies #reachability: Minimum-Time Reachability in Timed Games (TB, TAH, VSP, JFR), pp. 825–837.
PLDI-2007-BeyerHMR #invariant: Path invariants (DB, TAH, RM, AR), pp. 300–309.
TACAS-2007-ChatterjeeH #synthesis: Assume-Guarantee Synthesis (KC, TAH), pp. 261–275.
VMCAI-2007-BeyerHMR #invariant #synthesis: Invariant Synthesis for Combined Theories (DB, TAH, RM, AR), pp. 378–394.
CAV-2006-BeyerHT #analysis #lazy evaluation: Lazy Shape Analysis (DB, TAH, GT), pp. 532–546.
CAV-2006-WulfDHR #algorithm #anti #automaton #finite #named: Antichains: A New Algorithm for Checking Universality of Finite Automata (MDW, LD, TAH, JFR), pp. 17–30.
CSL-2006-ChatterjeeDHR #algorithm #game studies: Algorithms for ω-Regular Games with Imperfect Information (KC, LD, TAH, JFR), pp. 287–302.
CSL-2006-HenzingerP #game studies: Solving Games Without Determinization (TAH, NP), pp. 395–410.
FM-2006-HenzingerS #challenge #design #embedded: The Embedded Systems Design Challenge (TAH, JS), pp. 1–15.
FSE-2006-GulavaniHKNR #algorithm #named: SYNERGY: a new algorithm for property checking (BSG, TAH, YK, AVN, SKR), pp. 117–127.
TACAS-2006-ChatterjeeH #game studies: Finitary Winning in ω-Regular Games (KC, TAH), pp. 257–271.
ESEC-FSE-2005-HenzingerJM #interface: Permissive interfaces (TAH, RJ, RM), pp. 31–40.
FASE-2005-BeyerHJM #memory management #safety: Checking Memory Safety with Blast (DB, TAH, RJ, RM), pp. 2–18.
ICALP-2005-ChatterjeeAH #complexity #game studies #probability: The Complexity of Stochastic Rabin and Streett Games (KC, LdA, TAH), pp. 878–890.
LCTES-2005-HenzingerKM #code generation #composition #distributed: Composable code generation for distributed giotto (TAH, CMK, SM), pp. 21–30.
LICS-2005-ChatterjeeHJ #game studies: Mean-Payoff Parity Games (KC, TAH, MJ), pp. 178–187.
ECOOP-2004-Henzinger #interface: Rich Interfaces for Software Modules (TAH), pp. 517–518.
ICSE-2004-BeyerCM #generative #testing: Generating Tests from Counterexamples (DB, AC, TAH, RJ, RM), pp. 326–335.
IWPC-2004-BeyerHJM #eclipse #model checking #plugin: An Eclipse Plug-in for Model Checking (DB, TAH, RJ, RM), pp. 251–255.
LICS-2004-ChatterjeeHJ #game studies: Games with Secure Equilibria (KC, TAH, MJ), pp. 160–169.
PEPM-2004-BeyerCHJM #query #verification: Invited talk: the blast query language for software verification (DB, AC, TAH, RJ, RM), pp. 201–202.
PLDI-2004-HenzingerJM: Race checking by context inference (TAH, RJ, RM), pp. 1–13.
POPL-2004-HenzingerJMM #abstraction #proving: Abstractions from proofs (TAH, RJ, RM, KLM), pp. 232–244.
PPDP-2004-BeyerCHJM #query #verification: Invited talk: the blast query language for software verification (DB, AC, TAH, RJ, RM), pp. 1–2.
SAS-2004-BeyerCHJM #query #verification: The Blast Query Language for Software Verification. (DB, AC, TAH, RJ, RM), pp. 2–18.
TACAS-2004-AlfaroFHMS #model checking: Model Checking Discounted Temporal Properties (LdA, MF, TAH, RM, MS), pp. 77–92.
CAV-2003-HenzingerJMQ #abstraction #refinement #thread: Thread-Modular Abstraction Refinement (TAH, RJ, RM, SQ), pp. 262–274.
CIAA-2003-Henzinger #automaton #component #interface #specification: Automata for Specifying Component Interfaces (TAH), pp. 1–2.
CSL-2003-ChatterjeeJH #game studies #probability: Simple Stochastic Parity Games (KC, MJ, TAH), pp. 100–113.
ICALP-2003-AlfaroHM: Discounting the Future in Systems Theory (LdA, TAH, RM), pp. 1022–1037.
ICALP-2003-HenzingerJM: Counterexample-Guided Control (TAH, RJ, RM), pp. 886–902.
SAS-2003-ChatterjeeMMZHP #analysis #source code #stack: Stack Size Analysis for Interrupt-Driven Programs (KC, DM, RM, TZ, TAH, JP), pp. 109–126.
TACAS-2003-HenzingerKM #calculus #on the #μ-calculus: On the Universal and Existential Fragments of the μ-Calculus (TAH, OK, RM), pp. 49–64.
CAV-2002-ChakrabartiAHJM #interface: Interface Compatibility Checking for Software Modules (AC, LdA, TAH, MJ, FYCM), pp. 428–441.
CAV-2002-ChakrabartiAHM #bidirectional #component #interface: Synchronous and Bidirectional Component Interfaces (AC, LdA, TAH, FYCM), pp. 414–427.
CAV-2002-Henzinger #approach #hybrid: The Symbolic Approach to Hybrid Systems (TAH), p. 57.
CAV-2002-HenzingerJMNSW #proving: Temporal-Safety Proofs for Systems Code (TAH, RJ, RM, GCN, GS, WW), pp. 526–538.
CSL-2002-JurdzinskiKH #probability: Trading Probability for Fairness (MJ, OK, TAH), pp. 292–305.
ICALP-2002-HenzingerKKM #synthesis: Synthesis of Uninitialized Systems (TAH, SCK, OK, FYCM), pp. 644–656.
PLDI-2002-HenzingerK #embedded #predict #realtime: The Embedded Machine: Predictable, Portable Real-Time Code (TAH, CMK), pp. 315–326.
POPL-2002-HenzingerJMS #abstraction #lazy evaluation: Lazy abstraction (TAH, RJ, RM, GS), pp. 58–70.
ESEC-FSE-2001-AlfaroH #automaton #interface: Interface automata (LdA, TAH), pp. 109–120.
ICSE-2001-AlurAGHKKMMW #design #model checking #named: JMOCHA: A Model Checking Tool that Exploits Design Structure (RA, LdA, RG, TAH, MK, CMK, RM, FYCM, BYW), pp. 835–836.
LCTES-OM-2001-HenzingerHK #development #embedded: Embedded Control Systems Development with Giotto (TAH, BH, CMK), pp. 64–72.
LICS-2001-AlfaroHM #source code #verification: From Verification to Control: Dynamic Programs for ω-Regular Objectives (LdA, TAH, RM), pp. 279–290.
CAV-2000-AlfaroHM #detection #fault: Detecting Errors Before Reaching Them (LdA, TAH, FYCM), pp. 186–201.
LICS-2000-AlfaroH #concurrent #game studies: Concurrent ω-Regular Games (LdA, TAH), pp. 141–154.
SAS-2000-HenzingerMMR #abstract interpretation #game studies: Abstract Interpretation of Game Properties (TAH, RM, FYCM, JFR), pp. 220–239.
TACAS-2000-HenzingerM #hybrid #model checking: Symbolic Model Checking for Rectangular Hybrid Systems (TAH, RM), pp. 142–156.
TACAS-2000-HenzingerR #bisimulation: Fair Bisimulation (TAH, SKR), pp. 299–314.
CAV-1999-HenzingerQR #refinement: Assume-Guarantee Refinement Between Different Time Scales (TAH, SQ, SKR), pp. 208–221.
CAV-1999-HenzingerQR99a #consistency #multi #verification: Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems (TAH, SQ, SKR), pp. 301–315.
CAV-1998-AlurHMQRT #composition #model checking #named: MOCHA: Modularity in Model Checking (RA, TAH, FYCM, SQ, SKR, ST), pp. 521–525.
CAV-1998-HenzingerKQ #model checking: From Pre-historic to Post-modern Symbolic Model Checking (TAH, OK, SQ), pp. 195–206.
CAV-1998-HenzingerQR #case study: You Assume, We Guarantee: Methodology and Case Studies (TAH, SQ, SKR), pp. 440–451.
ICALP-1998-Henzinger #game studies #model checking #multi: Model Checking Game Properties of Multi-agent Systems (TAH), p. 543.
ICALP-1998-HenzingerRS #realtime: The Regular Real-Time Languages (TAH, JFR, PYS), pp. 580–591.
TACAS-1998-AlurHR: Symbolic Exploration of transition Hierarchies (RA, TAH, SKR), pp. 330–344.
CAV-1997-AlurBHQR #partial order #reduction: Partial-Order Reduction in Symbolic State Space Exploration (RA, RKB, TAH, SQ, SKR), pp. 340–351.
CAV-1997-HenzingerHW #hybrid #model checking #named: HYTECH: A Model Checker for Hybrid Systems (TAH, PHH, HWT), pp. 460–463.
ICALP-1997-HenzingerK97a #automaton #hybrid: Discrete-Time Control for Rectangular Hybrid Automata (TAH, PWK), pp. 582–593.
LICS-1996-AlurH: Reactive Modules (RA, TAH), pp. 207–218.
LICS-1996-Henzinger #automaton #formal method #hybrid: The Theory of Hybrid Automata (TAH), pp. 278–292.
CAV-1995-AlurH #composition #liveness #modelling: Local Liveness for Compositional Modeling of Fair Reactive Systems (RA, TAH), pp. 166–179.
CAV-1995-HenzingerH #algorithm #analysis #hybrid: Algorithmic Analysis of Nonlinear Hybrid Systems (TAH, PHH), pp. 225–238.
ICALP-1995-Henzinger95a #automaton #bisimulation #finite #hybrid: Hybrid Automata with Finite Bisimulatioins (TAH), pp. 324–335.
ICALP-1995-HenzingerKW #power of: The Expressive Power of Clocks (TAH, PWK, HWT), pp. 417–428.
STOC-1995-HenzingerKPV #automaton #decidability #hybrid #question #what: What’s decidable about hybrid automata? (TAH, PWK, AP, PV), pp. 373–382.
TACAS-1995-HenzingerHW: A User Guide to HyTech (TAH, PHH, HWT), pp. 41–71.
CAV-1994-AlurFH #automaton: A Determinizable Class of Timed Automata (RA, LF, TAH), pp. 1–13.
LICS-1994-AlurH: Finitary Fairness (RA, TAH), pp. 52–61.
CAV-1993-AlurCH #realtime: Computing Accumulated Delays in Real-time Systems (RA, CC, TAH), pp. 181–193.
STOC-1993-AlurHV #parametricity #realtime #reasoning: Parametric real-time reasoning (RA, TAH, MYV), pp. 592–601.
ICALP-1992-HenzingerMP #question #what: What Good Are Digital Clocks? (TAH, ZM, AP), pp. 545–558.
LICS-1992-HenzingerNSY #model checking #realtime: Symbolic Model Checking for Real-time Systems (TAH, XN, JS, SY), pp. 394–406.
POPL-1991-HenzingerMP #proving #realtime: Temporal Proof Methodologies for Real-time Systems (TAH, ZM, AP), pp. 353–366.
LICS-1990-AlurH #complexity #logic #realtime: Real-time Logics: Complexity and Expressiveness (RA, TAH), pp. 390–401.
CAV-2016-DacaHK #array #logic: Array Folds Logic (PD, TAH, AK), pp. 230–248.
CAV-2018-FrehseGH: Space-Time Interpolants (GF, MG, TAH), pp. 468–486.
CAV-2018-KongBH #approximate #set #using: Reachable Set Over-Approximation for Nonlinear Systems Using Piecewise Barrier Tubes (HK, EB, TAH), pp. 449–467.
CAV-2019-AvniBCHKP #game studies #optimisation #runtime: Run-Time Optimization for Learned Controllers Through Quantitative Games (GA, RB, KC, TAH, BK, SP), pp. 630–649.
CAV-2019-SotoHSZ #automaton #hybrid #linear #synthesis: Membership-Based Synthesis of Linear Hybrid Automata (MGS, TAH, CS0, LZ), pp. 297–314.
CSL-2020-FerrereHK #monitoring: Monitoring Event Frequencies (TF, TAH, BK), p. 16.
POPL-2016-DragoiHZ #algorithm #distributed #fault tolerance #named: PSync: a partially synchronous language for fault-tolerant distributed algorithms (CD, TAH, DZ), pp. 400–415.