@inproceedings{
AluHen89,
        author="Rajeev Alur and Thomas A. Henzinger",
	title="A really temporal logic",
	booktitle="FOCS: Foundations of Computer Science",
	publisher="IEEE Computer Society",
        year="1989",
	pages="164-169"
	}

	@inproceedings{
AluHen90,
        author="Rajeev Alur and Thomas A. Henzinger",
	title="Real-time logics: {C}omplexity and expressiveness",
	booktitle="LICS: Logic in Computer Science",
	publisher="IEEE Computer Society",
        year="1990",
	pages="390-401"
	}

	@inproceedings{
Hen90,
        author="Thomas A. Henzinger",
	title="Half-order modal logic: {H}ow to prove real-time properties",
	booktitle="PODC: Principles of Distributed Computing",
	publisher="ACM",
        year="1990",
	pages="281-296"
	}

	@inproceedings{
HMP90,
        author="Thomas A. Henzinger and Zohar Manna and Amir Pnueli",
	title="An interleaving model for real time",
	booktitle="JCIT: Jerusalem Conference on Information Technology",
	publisher="IEEE Computer Society",
        year="1990",
	pages="717-730"
	}

	@inproceedings{
HMP91,
        author="Thomas A. Henzinger and Zohar Manna and Amir Pnueli",
	title="Temporal proof methodologies for real-time systems",
	booktitle="POPL: Principles of Programming Languages",
	publisher="ACM",
        year="1991",
	pages="353-366"
	}

	@phdthesis{
Hen91,
	author="Thomas A. Henzinger",
	title="The Temporal Specification and Verification of Real-Time Systems",
        school="Stanford University",
        year="1991"
	}

	@inproceedings{
AFH91,
        author="Rajeev Alur and Tom\'as Feder and Thomas A. Henzinger",
	title="The benefits of relaxing punctuality",
	booktitle="PODC: Principles of Distributed Computing",
	publisher="ACM",
        year="1991",
	pages="139-152"
	}

	@article{
AluHen91,
	author="Rajeev Alur and Thomas A. Henzinger",
	title="Time for logic",
	journal="SIGACT News",
	volume="22(3)",
	year="1991",
        pages="6-12"
	}

	@article{
Hen92,
	author="Thomas A. Henzinger",
	title="Sooner Is Safer Than Later",
        journal="Information Processing Letters",
        volume="43",
        year="1992",
        pages="135-141"
	}

        @incollection{
AluHen92a,
        author="Rajeev Alur and Thomas A. Henzinger",
        title="Logics and models of real time: {A} survey",
        booktitle="Real Time: Theory in Practice",
        series="Lecture Notes in Computer Science 600",
        publisher="Springer",
        year="1992",
	pages="74-106"
        }

        @incollection{
HMP92a,
        author="Thomas A. Henzinger and Zohar Manna and Amir Pnueli",
        title="Timed transition systems",
        booktitle="Real Time: Theory in Practice",
        series="Lecture Notes in Computer Science 600",
        publisher="Springer",
        year="1992",
	pages="226-251"
        }

	@incollection{
HMP92,
        author="Thomas A. Henzinger and Zohar Manna and Amir Pnueli",
	title="What good are digital clocks?",
	booktitle="ICALP: Automata, Languages, and Programming",
	series="Lecture Notes in Computer Science 623",
	publisher="Springer",
        year="1992",
	pages="545-558"
	}

        @inproceedings{
HNSY92,
        author="Thomas A. Henzinger and Xavier Nicollin and Joseph Sifakis and Sergio Yovine",
        title="Symbolic model checking for real-time systems",
        booktitle="LICS: Logic in Computer Science",
        publisher="IEEE Computer Society",
        year="1992",
	pages="394-406"
        }

	@inproceedings{
AluHen92,
        author="Rajeev Alur and Thomas A. Henzinger",
        title="Back to the future: {T}owards a theory of timed regular languages",
	booktitle="FOCS: Foundations of Computer Science",
	publisher="IEEE Computer Society",
        year="1992",
	pages="177-186"
	}

	@incollection{
ACHH93,
        author="Rajeev Alur and Costas Courcoubetis and Thomas A. Henzinger and Pei-Hsin Ho",
	title="Hybrid automata: {A}n algorithmic approach to the specification and verification of hybrid systems",
	booktitle="Hybrid Systems",
	series="Lecture Notes in Computer Science 736",
	publisher="Springer",
        year="1993",
	pages="209-229"
        }

	@incollection{
HMP93,
        author="Thomas A. Henzinger and Zohar Manna and Amir Pnueli",
	title="Towards refining temporal specifications into hybrid systems",
	booktitle="Hybrid Systems",
	series="Lecture Notes in Computer Science 736",
	publisher="Springer",
        year="1993",
	pages="60-76"
        }

	@inproceedings{
AHV93,
        author="Rajeev Alur and Thomas A. Henzinger and Moshe Y. Vardi",
        title="Parametric real-time reasoning",
	booktitle="STOC: Theory of Computing",
	publisher="ACM",
        year="1993",
	pages="592-601"
	}

	@incollection{
ACH93,
        author="Rajeev Alur and Costas Courcoubetis and Thomas A. Henzinger",
	title="Computing accumulated delays in real-time systems",
	booktitle="CAV: Computer-Aided Verification",
	series="Lecture Notes in Computer Science 697",
	publisher="Springer",
        year="1993",
	pages="181-193"
        }

	@inproceedings{
AHH93,
        author="Rajeev Alur and Thomas A. Henzinger and Pei-Hsin Ho",
	title="Automatic symbolic verification of embedded systems",
	booktitle="RTSS: Real-Time Systems Symposium",
	publisher="IEEE Computer Society",
        year="1993",
	pages="2-11"
	}

	@article{
AluHen93,
        author="Rajeev Alur and Thomas A. Henzinger",
	title="Real-time logics: {C}omplexity and expressiveness",
	journal="Information and Computation",
        volume="104",
        year="1993",
        pages="35-77"
	}

	@incollection{
AluHen94a,
	author="Rajeev Alur and Thomas A. Henzinger",
 	title="Real-time system = discrete system + clock variables",
	booktitle="Theories and Experiences for Real-Time System Development",
	editor="Teodor Rus and Charles Rattray",
	series="AMAST Series in Computing 2",
	publisher="World Scientific",
        year="1994",
	pages="1-29"
	}

	@article{
AluHen94b,
        author="Rajeev Alur and Thomas A. Henzinger",
	title="A really temporal logic",
	journal="Journal of the ACM",
        volume="41",
        year="1994",
        pages="181-204"
	}

	@incollection{
ACHH+94,
        author="Rajeev Alur and Costas Courcoubetis and Thomas A. Henzinger and Pei-Hsin Ho and Xavier Nicollin and Alfredo Olivero and Joseph Sifakis and Sergio Yovine",
        title="The algorithmic analysis of hybrid systems",
	booktitle="ICAOS: Analysis and Optimization of Systems---Discrete-Event Systems",
	series="Lecture Notes in Control and Information Sciences 199",
	publisher="Springer",
        year="1994",
	pages="331-351"
	}

	@incollection{
AFH94,
        author="Rajeev Alur and Limor Fix and Thomas A. Henzinger",
	title="A determinizable class of timed automata",
	booktitle="CAV: Computer-Aided Verification",
	series="Lecture Notes in Computer Science 818",
	publisher="Springer",
        year="1994",
	pages="1-13"
        }

        @inproceedings{
AluHen94,
        author="Rajeev Alur and Thomas A. Henzinger",
        title="Finitary fairness",
        booktitle="LICS: Logic in Computer Science",
        publisher="IEEE Computer Society",
        year="1994",
	pages="52-61"
        }

	@incollection{
ACH94,
        author="Rajeev Alur and Costas Courcoubetis and Thomas A. Henzinger",
	title="The observational power of clocks",
	booktitle="CONCUR: Concurrency Theory",
	series="Lecture Notes in Computer Science 836",
	publisher="Springer",
        year="1994",
        pages="162-177"
        }

	@incollection{
HenKop94,
        author="Thomas A. Henzinger and Peter W. Kopke",
	title="Verification methods for the divergent runs of clock systems",
	booktitle="FTRTFT: Formal Techniques in Real-Time and Fault-Tolerant Systems",
	series="Lecture Notes in Computer Science 863",
	publisher="Springer",
        year="1994",
	pages="351-372"
        }

	@incollection{
KHMP94,
        author="Arjun Kapur and Thomas A. Henzinger and Zohar Manna and Amir Pnueli",
	title="Proving safety properties of hybrid systems",
	booktitle="FTRTFT: Formal Techniques in Real-Time and Fault-Tolerant Systems",
	series="Lecture Notes in Computer Science 863",
	publisher="Springer",
        year="1994",
	pages="431-454"
        }

	@article{
HNSY94,
        author="Thomas A. Henzinger and Xavier Nicollin and Joseph Sifakis and Sergio Yovine",
        title="Symbolic model checking for real-time systems",
	journal="Information and Computation",
        volume="111",
        year="1994",
        pages="193-244"
	}

	@article{
HMP94,
        author="Thomas A. Henzinger and Zohar Manna and Amir Pnueli",
	title="Temporal proof methodologies for timed transition systems",
	journal="Information and Computation",
        volume="112",
        year="1994",
        pages="273-337"
	}

	@article{
ACHH+95,
        author="Rajeev Alur and Costas Courcoubetis and Nicolas Halbwachs and Thomas A. Henzinger and Pei-Hsin Ho and Xavier Nicollin and Alfredo Olivero and Joseph Sifakis and Sergio Yovine",
        title="The algorithmic analysis of hybrid systems",
	journal="Theoretical Computer Science",
        volume="138",
        year="1995",
	pages="3-34"
	}

	@inproceedings{
HKPV95,
	author="Thomas A. Henzinger and Peter W. Kopke and Anuj Puri and Pravin Varaiya",
 	title="What's decidable about hybrid automata?",
	booktitle="STOC: Theory of Computing",
	publisher="ACM",
        year="1995",
	pages="373-382"
	}

	@incollection{
HenHo95,
        author="Thomas A. Henzinger and Pei-Hsin Ho",
	title="Algorithmic analysis of nonlinear hybrid systems",	    
	booktitle="CAV: Computer-Aided Verification",
	series="Lecture Notes in Computer Science 939",
	publisher="Springer",
        year="1995",
	pages="225-238"
	}

	@incollection{
AluHen95,
        author="Rajeev Alur and Thomas A. Henzinger",
        title="Local liveness for compositional modeling of fair reactive systems",
	booktitle="CAV: Computer-Aided Verification",
	series="Lecture Notes in Computer Science 939",
	publisher="Springer",
        year="1995",
	pages="166-179"
	}

	@incollection{
HKW95,
        author="Thomas A. Henzinger and Peter W. Kopke and Howard Wong-Toi",
	title="The expressive power of clocks",
	booktitle="ICALP: Automata, Languages, and Programming",
	series="Lecture Notes in Computer Science 944",
	publisher="Springer",
        year="1995",
	pages="417-428"
	}

	@incollection{
Hen95,
        author="Thomas A. Henzinger",
	title="Hybrid automata with finite bisimulations",
	booktitle="ICALP: Automata, Languages, and Programming",
	series="Lecture Notes in Computer Science 944",
	publisher="Springer",
        year="1995",
	pages="324-335"
	}

	@incollection{
HenHo95a,
        author="Thomas A. Henzinger and Pei-Hsin Ho",
	title="{{\sc HyTech}}: {T}he {C}ornell {H}ybrid {T}echnology {T}ool",
	booktitle="Hybrid Systems II",
	series="Lecture Notes in Computer Science 999",
	publisher="Springer",
        year="1995",
        pages="265-293"
	}

	@incollection{
HenHo95b,
        author="Thomas A. Henzinger and Pei-Hsin Ho",
	title="A note on abstract-interpretation strategies for hybrid automata",
	booktitle="Hybrid Systems II",
	series="Lecture Notes in Computer Science 999",
	publisher="Springer",
        year="1995",
        pages="252-264"
	}

	@incollection{
HHW95a,
	author="Thomas A. Henzinger and Pei-Hsin Ho and Howard Wong-Toi",
	title="A user guide to {{\sc HyTech}}",
	booktitle="TACAS: Tools and Algorithms for the Construction and Analysis of Systems",
	series="Lecture Notes in Computer Science 1019",
	publisher="Springer",
        year="1995",
	pages="41-71"
	}

	@inproceedings{
HHK95,
	author="Monika R. Henzinger and Thomas A. Henzinger and Peter W. Kopke",
	title="Computing simulations on finite and infinite graphs",
	booktitle="FOCS: Foundations of Computer Science",
	publisher="IEEE Computer Society",
        year="1995",
	pages="453-462"
	}

	@inproceedings{
HHW95,
	author="Thomas A. Henzinger and Pei-Hsin Ho and Howard Wong-Toi",
	title="{{\sc HyTech}}: {T}he next generation",
	booktitle="RTSS: Real-Time Systems Symposium",
	publisher="IEEE Computer Society",
        year="1995",
	pages="56-65"
	}

	@incollection{
HenWon96a,
	author="Thomas A. Henzinger and Howard Wong-Toi",
	title="Linear phase-portrait approximations for nonlinear hybrid systems",
	booktitle="Hybrid Systems III",
	series="Lecture Notes in Computer Science 1066",
	publisher="Springer",
        year="1996",
        pages="377-388"
	}

	@article{
AFH96,
        author="Rajeev Alur and Tom\'as Feder and Thomas A. Henzinger",
	title="The benefits of relaxing punctuality",
	journal="Journal of the ACM",
        volume="43",
        year="1996",
        pages="116-146"
	}

	@article{
AHH96,
        author="Rajeev Alur and Thomas A. Henzinger and Pei-Hsin Ho",
	title="Automatic symbolic verification of embedded systems",
	journal="IEEE Transactions on Software Engineering",		   
        volume="22",
        year="1996",
	pages="181-201"
	}

	@inproceedings{
Hen96,
        author="Thomas A. Henzinger",
	title="The theory of hybrid automata",
	booktitle="LICS: Logic in Computer Science",
	publisher="IEEE Computer Society",
        year="1996",
	pages="278-292"
	}

	@inproceedings{
AluHen96,
        author="Rajeev Alur and Thomas A. Henzinger",
	title="Reactive modules",
	booktitle="LICS: Logic in Computer Science",
	publisher="IEEE Computer Society",
        year="1996",
	pages="207-218"
	}

	@incollection{
HenKop96,
        author="Thomas A. Henzinger and Peter W. Kopke",
	title="State equivalences for rectangular hybrid automata",
	booktitle="CONCUR: Concurrency Theory",
	series="Lecture Notes in Computer Science 1119",
	publisher="Springer",
        year="1996",
	pages="530-545"
        }

	@incollection{
HKV96,
        author="Thomas A. Henzinger and Orna Kupferman and Moshe Y. Vardi",
	title="A space-efficient on-the-fly algorithm for real-time model checking",
	booktitle="CONCUR: Concurrency Theory",
	series="Lecture Notes in Computer Science 1119",
	publisher="Springer",
        year="1996",
	pages="514-529"
        }

	@incollection{
HenWon96,
        author="Thomas A. Henzinger and Howard Wong-Toi",
	title="Using {{\sc HyTech}} to synthesize control parameters for a steam boiler",
        booktitle="Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control",
	series="Lecture Notes in Computer Science 1165",
	publisher="Springer",
        year="1996",
	pages="265-282"
        }	

	@book{
AHS96,
	title="Hybrid Systems III: Verification and Control",
	editor="Rajeev Alur and Thomas A. Henzinger and Eduardo D. Sontag",
	series="Lecture Notes in Computer Science 1066",
	publisher="Springer",
        year="1996"
	}

	@book{
AluHen96a,
	title="CAV: Computer-Aided Verification",
	editor="Rajeev Alur and Thomas A. Henzinger",
	series="Lecture Notes in Computer Science 1102",
	publisher="Springer",
        year="1996"
	}

	@article{
ACH97,
        author="Rajeev Alur and Costas Courcoubetis and Thomas A. Henzinger",
	title="Computing accumulated delays in real-time systems",
	journal="Formal Methods in System Design",
	volume="11",
        year="1997",
	pages="137-156"
	}

	@article{
AluHen97a,
	author="Rajeev Alur and Thomas A. Henzinger",
 	title="Real-time system = discrete system + clock variables",
	journal="Software Tools for Technology Transfer",
        year="1997",
	pages="86-109"
	}

	@incollection{
HenKup97,
	author="Thomas A. Henzinger and Orna Kupferman",
	title="From quantity to quality",
	booktitle="HART: Hybrid and Real-Time Systems",
	series="Lecture Notes in Computer Science 1201",
	publisher="Springer",
        year="1997",
	pages="48-62"
	}

	@incollection{
GHJ97,
	author="Vineet Gupta and Thomas A. Henzinger and Radha Jagadeesan",
        title="Robust timed automata",
	booktitle="HART: Hybrid and Real-Time Systems",
	series="Lecture Notes in Computer Science 1201",
	publisher="Springer",
        year="1997",
	pages="331-345"
	}

	@incollection{
HenKop97,
	author="Thomas A. Henzinger and Peter W. Kopke",
        title="Discrete-time control for rectangular hybrid automata",
	booktitle="ICALP: Automata, Languages, and Programming",
	series="Lecture Notes in Computer Science 1256",
	publisher="Springer",
        year="1997",
	pages="582-593"
	}

	@incollection{
HKR97,
	author="Thomas A. Henzinger and Orna Kupferman and Sriram K. Rajamani",
        title="Fair simulation",
	booktitle="CONCUR: Concurrency Theory",
	series="Lecture Notes in Computer Science 1243",
	publisher="Springer",
        year="1997",
	pages="273-287"
        }

	@incollection{
AluHen97,
	author="Rajeev Alur and Thomas A. Henzinger",
        title="Modularity for timed and hybrid systems",
	booktitle="CONCUR: Concurrency Theory",
	series="Lecture Notes in Computer Science 1243",
	publisher="Springer",
        year="1997",
	pages="74-88"
        }

	@incollection{
ABHQ+97,
        author="Rajeev Alur and Robert K. Brayton and Thomas A. Henzinger and Shaz Qadeer and Sriram K. Rajamani",
        title="Partial-order reduction in symbolic state-space exploration",
	booktitle="CAV: Computer-Aided Verification",
	series="Lecture Notes in Computer Science 1254",
	publisher="Springer",
        year="1997",
	pages="340-351"
	}

	@incollection{
HHW97a,
        author="Thomas A. Henzinger and Pei-Hsin Ho and Howard Wong-Toi",
        title="{{\sc HyTech}}: {A} model checker for hybrid systems",
	booktitle="CAV: Computer-Aided Verification",
	series="Lecture Notes in Computer Science 1254",
	publisher="Springer",
        year="1997",
	pages="460-463"
	}

	@article{
HHW97,
        author="Thomas A. Henzinger and Pei-Hsin Ho and Howard Wong-Toi",
        title="{{\sc HyTech}}: A model checker for hybrid systems",
	journal="Software Tools for Technology Transfer",
        year="1997",
	pages="110-122"
	}

	@inproceedings{
AHK97,
	author="Rajeev Alur and Thomas A. Henzinger and Orna Kupferman", 
        title="Alternating-time temporal logic",
    	booktitle="FOCS: Foundations of Computer	Science",
	publisher="IEEE Computer Society",
        year="1997",
	pages="100-109"
	}

	@inproceedings{
AHW97,
	author="Rajeev Alur and Thomas A. Henzinger and Howard Wong-Toi",
        title="Symbolic analysis of hybrid systems",
        booktitle="CDC: Decision and Control",
	publisher="IEEE",
        year="1997",
	pages="702-707"
	}

	@article{
HKPV98,
	author="Thomas A. Henzinger and Peter W. Kopke and Anuj Puri and Pravin Varaiya",
 	title="What's decidable about hybrid automata?",
	journal="Journal of Computer and System Sciences",
	volume="57",
        year="1998",
	pages="94-124"
	}

	@incollection{
AHR98,
	author="Rajeev Alur and Thomas A. Henzinger and Sriram K. Rajamani",
	title="Symbolic exploration of transition hierarchies", 
	booktitle="TACAS: Tools and Algorithms for the Construction and Analysis of Systems",
	series="Lecture Notes in Computer Science 1384",
	publisher="Springer",
        year="1998",
	pages="330-344"
	}
	
	@incollection{
HenRus98,
	author="Thomas A. Henzinger and Vlad Rusu",
	title="Reachability verification for hybrid automata",
	booktitle="HSCC: Hybrid Systems---Computation and Control",
	series="Lecture Notes in Computer Science 1386",
	publisher="Springer",
        year="1998",
	pages="190-204"
	}

	@book{
HenSas98,
	title="HSCC: Hybrid Systems---Computation and Control",
        editor="Thomas A. Henzinger and Shankar Sastry",
	series="Lecture Notes in Computer Science 1386",
	publisher="Springer",
        year="1998"
	}

	@article{
HHW98,
        author="Thomas A. Henzinger and Pei-Hsin Ho and Howard Wong-Toi",
	title="Algorithmic analysis of nonlinear hybrid systems",	    
	journal="IEEE Transactions on Automatic Control",
	volume="43",
        year="1998",
	pages="540-554"
	}

	@incollection{
AHMQ+98,
	author="Rajeev Alur and Thomas A. Henzinger and Freddy Y.C. Mang and Shaz Qadeer and Sriram K. Rajamani and Serdar Tasiran",
        title="{{\sc Mocha}}: {M}odularity in model checking",
	booktitle="CAV: Computer-Aided Verification",
	series="Lecture Notes in Computer Science 1427",
	publisher="Springer",
        year="1998",
	pages="521-525"
	}

	@incollection{
HQR98,
	author="Thomas A. Henzinger and Shaz Qadeer and Sriram K. Rajamani",
        title="You assume, we guarantee: {M}ethodology and case studies",
	booktitle="CAV: Computer-Aided Verification",
	series="Lecture Notes in Computer Science 1427",
	publisher="Springer",
        year="1998",
	pages="440-451"
	}

	@incollection{
HKQ98,
	author="Thomas A. Henzinger and Orna Kupferman and Shaz Qadeer",
        title="From {\em pre\/}historic to {\em post\/}modern symbolic model checking", 
	booktitle="CAV: Computer-Aided Verification",
	series="Lecture Notes in Computer Science 1427",
	publisher="Springer",
        year="1998",
	pages="195-206"
	}

	@incollection{
HRS98,
	author="Thomas A. Henzinger and Jean-Fran\c{c}ois Raskin and Pierre-Yves Schobbens",
        title="The regular real-time languages",
	booktitle="ICALP: Automata, Languages, and Programming",
	series="Lecture Notes in Computer Science 1443",
	publisher="Springer",
        year="1998",
	pages="580-591"
	}

	@incollection{
RSH98,
	author="Jean-Fran\c{c}ois Raskin and Pierre-Yves Schobbens and Thomas A. Henzinger",
        title="Axioms for real-time logics",
	booktitle="CONCUR: Concurrency Theory",
	series="Lecture Notes in Computer Science 1466",
	publisher="Springer",
        year="1998",
	pages="219-236"
        }

	@incollection{
Hen98,
	author="Thomas A. Henzinger",
        title="It's about time: {R}eal-time logics reviewed",
	booktitle="CONCUR: Concurrency Theory",
	series="Lecture Notes in Computer Science 1466",
	publisher="Springer",
        year="1998",
	pages="439-454"
        }

	@incollection{
AHKV98,
	author="Rajeev Alur and Thomas A. Henzinger and Orna Kupferman and Moshe Y. Vardi",
        title="Alternating refinement relations",
	booktitle="CONCUR: Concurrency Theory",
	series="Lecture Notes in Computer Science 1466",
	publisher="Springer",
        year="1998",
	pages="163-178"
        }

	@incollection{
PKWH98,
        author="J\"org Preu\ss ig and Stephan Kowalewski and Howard Wong-Toi and Thomas A. Henzinger",
	title="An algorithm for the approximative analysis of rectangular automata",
	booktitle="FTRTFT: Formal Techniques in Real-Time and Fault-Tolerant Systems",
	series="Lecture Notes in Computer Science 1486",
	publisher="Springer",
        year="1998",
	pages="228-240"
        }

	@incollection{
HQRT98,
        author="Thomas A. Henzinger and Shaz Qadeer and Sriram K. Rajamani and Serdar Tasiran",
	title="An assume-guarantee rule for checking simulation",
	booktitle="FMCAD: Formal Methods in Computer-Aided Design",
	series="Lecture Notes in Computer Science 1522",
	publisher="Springer",
        year="1998",
	pages="421-432"
        }

	@inproceedings{
AHK98,
        author="Luca de Alfaro and Thomas A. Henzinger and Orna Kupferman",
	title="Concurrent reachability games",
	booktitle="FOCS: Foundations of Computer Science",
	publisher="IEEE Computer Society",
        year="1998",
	pages="564-575"
	}

	@incollection{
HQR99,
	author="Thomas A. Henzinger and Shaz Qadeer and Sriram K. Rajamani",
        title="Assume-guarantee refinement between different time scales",
	booktitle="CAV: Computer-Aided Verification",
	series="Lecture Notes in Computer Science 1633",
	publisher="Springer",
        year="1999",
	pages="208-221"
	}

	@incollection{
HQR99a,
	author="Thomas A. Henzinger and Shaz Qadeer and Sriram K. Rajamani",
        title="Verifying sequential consistency on shared-memory multiprocessor systems", 
	booktitle="CAV: Computer-Aided Verification",
	series="Lecture Notes in Computer Science 1633",
	publisher="Springer",
        year="1999",
	pages="301-315"
	}

	@incollection{
HHM99,
	author="Thomas A. Henzinger and Benjamin Horowitz and Rupak Majumdar",
        title="Rectangular hybrid games",
	booktitle="CONCUR: Concurrency Theory",
	series="Lecture Notes in Computer Science 1664",
	publisher="Springer",
        year="1999",
	pages="320-335"
        }

	@incollection{
AAHM99,
	author="Rajeev Alur and Luca de Alfaro and Thomas A. Henzinger and Freddy Y.C. Mang",
        title="Automating modular verification",
	booktitle="CONCUR: Concurrency Theory",
	series="Lecture Notes in Computer Science 1664",
	publisher="Springer",
        year="1999",
	pages="82-97"
        }

        @incollection{
AHK99,
        author="Rajeev Alur and Thomas A. Henzinger and Orna Kupferman",
        title="Alternating-time temporal logic",
        booktitle="Compositionality: The Significant Difference",
        series="Lecture Notes in Computer Science 1536",
        publisher="Springer",
        year="1999",
	pages="23-60"
        }

	@article{
AluHen99,
        author="Rajeev Alur and Thomas A. Henzinger",
	title="Reactive modules",
	journal="Formal Methods in System Design",
	volume="15",
        year="1999",
	pages="7-48"
	}

	@article{
HenKop99,
	author="Thomas A. Henzinger and Peter W. Kopke",
        title="Discrete-time control for rectangular hybrid automata",
	journal="Theoretical Computer Science",
	volume="221",
        year="1999",
	pages="369-392"
	}

	@inproceedings{
HLQR99,
        author="Thomas A. Henzinger and Xiaojun Liu and Shaz Qadeer and Sriram K. Rajamani",
	title="Formal specification and verification of a dataflow processor array",
	booktitle="ICCAD: Computer-Aided Design",
	publisher="IEEE Computer Society",
        year="1999",
	pages="494-499"
	}

	@incollection{
HenMaj00,
	author="Thomas A. Henzinger and Rupak Majumdar",
	title="A classification of symbolic transition systems", 
	booktitle="STACS: Theoretical Aspects of Computer Science",
	series="Lecture Notes in Computer Science 1770",
	publisher="Springer",
        year="2000",
	pages="13-34"
	}

	@incollection{
HHMW00,
	author="Thomas A. Henzinger and Benjamin Horowitz and Rupak Majumdar and Howard Wong-Toi",
	title="Beyond {{\sc HyTech}}: {H}ybrid systems analysis using interval numerical methods",
	booktitle="HSCC: Hybrid Systems---Computation and Control",
	series="Lecture Notes in Computer Science 1790",
	publisher="Springer",
        year="2000",
	pages="130-144"
	}

	@incollection{
HenRas00,
	author="Thomas A. Henzinger and Jean-Fran\c{c}ois Raskin",
	title="Robust undecidability of timed and hybrid systems",
	booktitle="HSCC: Hybrid Systems---Computation and Control",
	series="Lecture Notes in Computer Science 1790",
	publisher="Springer",
        year="2000",
	pages="145-159"
	}

	@incollection{
HenMaj00a,
	author="Thomas A. Henzinger and Rupak Majumdar",
	title="Symbolic model checking for rectangular hybrid systems", 
	booktitle="TACAS: Tools and Algorithms for the Construction and Analysis of Systems",
	series="Lecture Notes in Computer Science 1785",
	publisher="Springer",
        year="2000",
	pages="142-156"
	}

	@incollection{
HenRaj00,
	author="Thomas A. Henzinger and Sriram K. Rajamani",
	title="Fair bisimulation", 
	booktitle="TACAS: Tools and Algorithms for the Construction and Analysis of Systems",
	series="Lecture Notes in Computer Science 1785",
	publisher="Springer",
        year="2000",
	pages="299-314"
	}

	@inproceedings{
AlfHen00,
        author="Luca de Alfaro and Thomas A. Henzinger",
	title="Concurrent omega-regular games",
	booktitle="LICS: Logic in Computer Science",
	publisher="IEEE Computer Society",
        year="2000",
	pages="141-154"
	}

	@incollection{
HMMR00,
	author="Thomas A. Henzinger and Rupak Majumdar and Freddy Y.C. Mang and Jean-Fran\c{c}ois Raskin",
	title="Abstract interpretation of game properties",
	booktitle="SAS: Static Analysis",
	series="Lecture Notes in Computer Science 1824",
	publisher="Springer",
        year="2000",
	pages="220-239"
	}

	@incollection{
AHM00,
	author="Luca de Alfaro and Thomas A. Henzinger and Freddy Y.C. Mang",
	title="Detecting errors before reaching them", 
	booktitle="CAV: Computer-Aided Verification",
	series="Lecture Notes in Computer Science 1855",
	publisher="Springer",
        year="2000",
	pages="186-201"
	}

	@incollection{
Hen00,
	author="Thomas A. Henzinger",
	title="{{\sc Masaccio}}: {A} formal model for embedded components",
	booktitle="TCS: Theoretical Computer Science",
	series="Lecture Notes in Computer Science 1872",
	publisher="Springer",
        year="2000",
	pages="549-563"
	}

	@incollection{
AHM00a,
	author="Luca de Alfaro and Thomas A. Henzinger and Freddy Y.C. Mang",
	title="The control of synchronous systems",
	booktitle="CONCUR: Concurrency Theory",
	series="Lecture Notes in Computer Science 1877",
	publisher="Springer",
        year="2000",
	pages="458-473"
	}

	@article{
AHLP00,
        author="Rajeev Alur and Thomas A. Henzinger and Gerardo Lafferriere and George J. Pappas",
	title="Discrete abstractions of hybrid systems",
	journal="Proceedings of the IEEE",
	volume="88",
        year="2000",
	pages="971-984"
	}	

	@inproceedings{
HQR00,
        author="Thomas A. Henzinger and Shaz Qadeer and Sriram K. Rajamani",
	title="Decomposing refinement proofs using assume-guarantee reasoning", 
	booktitle="ICCAD: Computer-Aided Design",
	publisher="IEEE Computer Society",
        year="2000",
	pages="245-252"
	}

	@incollection{
Hen00a,
        author="Thomas A. Henzinger",
	title="The theory of hybrid automata",
	booktitle="Verification of Digital and Hybrid Systems",
        editor="M. Kemal Inan and Robert P. Kurshan",
	series="NATO ASI Series F: Computer and Systems Sciences 170",
	publisher="Springer",
        year="2000",
	pages="265-292"
        }

	@article{
ABHQ+01,
        author="Rajeev Alur and Robert K. Brayton and Thomas A. Henzinger and Shaz Qadeer and Sriram K. Rajamani",
        title="Partial-order reduction in symbolic state-space exploration",
	journal="Formal Methods in System Design",
	volume="18",
	year="2001",
	pages="97-116"
	}

	@incollection{
HMP01,
	author="Thomas A. Henzinger and Marius Minea and Vinayak S. Prabhu",
	title="Assume-guarantee reasoning for hierarchical hybrid systems",
	booktitle="HSCC: Hybrid Systems---Computation and Control",
	series="Lecture Notes in Computer Science 2034",
	publisher="Springer",
        year="2001",
	pages="275-290"
	}

	@inproceedings{
AAGH+01,
	author="Rajeev Alur and Luca de Alfaro and Radhu Grosu and Thomas A. Henzinger and Minsu Kang and Christoph M. Kirsch and Rupak Majumdar and Freddy Y.C. Mang and Bow-Yaw Wang",
	title="{{\sc jMocha}}: {A} model-checking tool that exploits design structure",
	booktitle="ICSE: Software Engineering",
	publisher="IEEE Computer Society",
	year="2001",
	pages="835-836"
	}

	@inproceedings{
AHM01c,
     	author="Luca de Alfaro and Thomas A. Henzinger and Freddy Y.C. Mang", 
	title="{{\sc McWeb}}: {A} model-checking tool for web-site debugging",
	booktitle="WWW: Word-Wide Web Conference (Poster Proceedings)",
	year="2001",
	pages="86-87"
	} 

	@inproceedings{
HHK01a,
	author="Thomas A. Henzinger and Benjamin Horowitz and Christoph M. Kirsch",
	title="Embedded control systems development with {{\sc Giotto}}",
	booktitle="LCTES: Languages, Compilers, and Tools for Embedded Systems",
	publisher="ACM",
	year="2001",
	pages="64-72"
	}

	@inproceedings{
AHM01,
        author="Luca de Alfaro and Thomas A. Henzinger and Rupak Majumdar",
	title="From verification to control: {D}ynamic programs for omega-regular objectives",
	booktitle="LICS: Logic in Computer Science",
	publisher="IEEE Computer Society",
        year="2001",
	pages="279-290"
	}

	@incollection{
AHM01b,
	author="Luca de Alfaro and Thomas A. Henzinger and Rupak Majumdar",
	title="Symbolic algorithms for infinite-state games",
	booktitle="CONCUR: Concurrency Theory",
	series="Lecture Notes in Computer Science 2154",
	publisher="Springer",
        year="2001",
	pages="536-550"
	}

	@incollection{
AHM01a,
	author="Luca de Alfaro and Thomas A. Henzinger and Freddy Y.C. Mang",
	title="The control of synchronous systems, Part II",
	booktitle="CONCUR: Concurrency Theory",
	series="Lecture Notes in Computer Science 2154",
	publisher="Springer",
        year="2001",
	pages="566-580"
	}

	@incollection{
AHJ01,
	author="Luca de Alfaro and Thomas A. Henzinger and Ranjit Jhala",
	title="Compositional methods for probabilistic systems",
	booktitle="CONCUR: Concurrency Theory",
	series="Lecture Notes in Computer Science 2154",
	publisher="Springer",
        year="2001",
	pages="351-365"
	}

	@inproceedings{
AlfHen01,
	author="Luca de Alfaro and Thomas A. Henzinger",
	title="Interface automata",
	booktitle="FSE:	Foundations of Software Engineering",
	publisher="ACM",
	year="2001",
	pages="109-120"
	}

	@incollection{
HHK01,
	author="Thomas A. Henzinger and Benjamin Horowitz and Christoph M. Kirsch",
	title="{{\sc Giotto}}: {A} time-triggered language for embedded programming",
	booktitle="EMSOFT: Embedded Software",
	series="Lecture Notes in Computer Science 2211", 
	publisher="Springer", 
	year="2001",
	pages="166-184"
	} 

	@incollection{
AlfHen01a,
	author="Luca de Alfaro and Thomas A. Henzinger",
	title="Interface theories for component-based design",
	booktitle="EMSOFT: Embedded Software",
	series="Lecture Notes in Computer Science 2211", 
	publisher="Springer", 
	year="2001",
	pages="148-165"
	} 

	@book{
HenKir01,
	title="EMSOFT: Embedded Software",
        editor="Thomas A. Henzinger and Christoph M. Kirsch",
	series="Lecture Notes in Computer Science 2211",
	publisher="Springer",
        year="2001"
	}

	@inproceedings{
BPPH+01,
	author="Timothy Brown and Alessandro Pasetti and Wolfgang Pree and Thomas A. Henzinger and Christoph M. Kirsch",
	title="A reusable and platform-independent framework for distributed control systems",
	booktitle="DASC: Digital Avionics Systems Conference",
        volume="2",
	publisher="IEEE",
	year="2001",
	pages="1-11"
	}

	@inproceedings{
HPW01,
	author="Thomas A. Henzinger and J\"org Preu\ss ig and Howard Wong-Toi",
	title="Some lessons from the {{\sc HyTech}} experience",
	booktitle="CDC: Decision and Control",
	publisher="IEEE",
	year="2001",
	pages="2887-2892"
	}

	@inproceedings{
HJMS02,
	author="Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar and Gr\'egoire Sutre",
	title="Lazy abstraction",
	booktitle="POPL: Principles of Programming Languages",
	publisher="ACM",
	year="2002",
	pages="58-70"
	}

	@incollection{
CHR02,
	author="Franck Cassez and Thomas A. Henzinger and Jean-Fran\c{c}ois Raskin",
	title="A comparison of control problems for timed and hybrid systems",
	booktitle="HSCC: Hybrid Systems---Computation and Control",
	series="Lecture Notes in Computer Science 2289",
	publisher="Springer",
        year="2002",
	pages="134-148"
	}

	@inproceedings{
HenKir02,
	author="Thomas A. Henzinger and Christoph M. Kirsch",
	title="The {E}mbedded {M}achine: {P}redictable, portable real-time code",
	booktitle="PLDI: Programming Language Design and Implementation",
	publisher="ACM",
	year="2002",
	pages="315-326"
	}

	@article{
HKR02,
	author="Thomas A. Henzinger and Orna Kupferman and Sriram K. Rajamani",
	title="Fair simulation",
	journal="Information and Computation",
	volume="173",
	year="2002", 
	pages="64-81"
	}

	@article{
RSH02,
	author="Jean-Fran\c{c}ois Raskin and Pierre-Yves Schobbens and Thomas A. Henzinger",
        title="Axioms for real-time logics",
	journal="Theoretical Computer Science",
	volume="274",
	year="2002",
	pages="151-182"
	}

	@article{
HQRT02,
        author="Thomas A. Henzinger and Shaz Qadeer and Sriram K. Rajamani and Serdar Tasiran",
	title="An assume-guarantee rule for checking simulation",
        journal="ACM Transactions on Programming Languages and Systems",
        volume="24",
        year="2002",
	pages="51-64"
        }

	@article{
AHK02,
	author="Rajeev Alur and Thomas A. Henzinger and Orna Kupferman", 
        title="Alternating-time temporal logic",
        journal="Journal of the ACM",
        volume="49",
        year="2002",
	pages="672-713"
	}

	@inproceedings{
HLMK+02,
	author="Benjamin Horowitz and Judith Liebman and Cedric Ma and T. John Koo and Thomas A. Henzinger and Alberto L. Sangiovanni-Vincentelli and Shankar Sastry",
	title="Embedded software design and system integration for rotorcraft {UAV} using platforms",
	booktitle="IFAC World Congress on Automatic Control",
	publisher="Elsevier",
	year="2002"
	}

	@incollection{
HKKM02,
	author="Thomas A. Henzinger and Sriram C. Krishnan and Orna Kupferman and Freddy Y.C. Mang",
        title="Synthesis of uninitialized systems",
	booktitle="ICALP: Automata, Languages, and Programming",
	series="Lecture Notes in Computer Science 2380",
	publisher="Springer",
        year="2002",
	pages="644-656"
	}

	@incollection{
CAHM02,
	author="Arindam Chakrabarti and Luca de Alfaro and Thomas A. Henzinger and Freddy Y.C. Mang",
	title="Synchronous and bidirectional component interfaces",
	booktitle="CAV: Computer-Aided Verification",
	series="Lecture Notes in Computer Science 2404",
	publisher="Springer",
        year="2002",
	pages="414-427"
	}

	@incollection{
CAHJ+02,
	author="Arindam Chakrabarti and Luca de Alfaro and Thomas A. Henzinger and Marcin Jurdzi\'nski and Freddy Y.C. Mang",
	title="Interface compatibility checking for software modules",
	booktitle="CAV: Computer-Aided Verification",
	series="Lecture Notes in Computer Science 2404",
	publisher="Springer",
        year="2002",
	pages="428-441"
	}

	@incollection{
HJMN+02,
	author="Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar and George C. Necula and Gr\'egoire Sutre and Westley Weimer",
	title="Temporal safety proofs for systems code",
	booktitle="CAV: Computer-Aided Verification",
	series="Lecture Notes in Computer Science 2404",
	publisher="Springer",
        year="2002",
	pages="526-538"
	}

	@incollection{
JKH02,
	author="Marcin Jurdzi\'nski and Orna Kupferman and Thomas A. Henzinger",
	title="Trading probability for fairness",
	booktitle="CSL: Computer Science Logic",
	series="Lecture Notes in Computer Science 2471", 
	publisher="Springer", 
	year="2002",
        pages="292-305"
	} 

	@incollection{
HKMM02,
	author="Thomas A. Henzinger and Christoph M. Kirsch and Rupak Majumdar and Slobodan Matic",
	title="Time-safety checking for embedded programs",
	booktitle="EMSOFT: Embedded Software",
	series="Lecture Notes in Computer Science 2491", 
	publisher="Springer", 
	year="2002",
        pages="76-92"
	} 

	@incollection{
AHS02,
	author="Luca de Alfaro and Thomas A. Henzinger and Marielle Stoelinga",
	title="Timed interfaces",
	booktitle="EMSOFT: Embedded Software",
	series="Lecture Notes in Computer Science 2491", 
	publisher="Springer", 
	year="2002",
        pages="108-122"
	} 

	@incollection{
KSHP02,
	author="Christoph M. Kirsch and Marco A.A. Sanvido and Thomas A. Henzinger and Wolfgang Pree",
	title="A {{\sc Giotto}}-based helicopter control system",
	booktitle="EMSOFT: Embedded Software",
	series="Lecture Notes in Computer Science 2491", 
	publisher="Springer", 
	year="2002",
        pages="46-60"
	} 

	@inproceedings{
PAHS02,
        author="Roberto Passerone and Luca de Alfaro and Thomas A. Henzinger and Alberto L. Sangiovanni-Vincentelli",
	title="Convertibility verification and converter synthesis: {T}wo faces of the same coin",
	booktitle="ICCAD: Computer-Aided Design",
	publisher="IEEE Computer Society",
        year="2002",
        pages="132-139"
	}

	@article{
HKSP03,
	author="Thomas A. Henzinger and Christoph M. Kirsch and Marco A.A. Sanvido and Wolfgang Pree", 
        title="From control models to real-time code using {{\sc Giotto}}",
        journal="IEEE Control Systems Magazine",
        volume="23(1)",
        year="2003",
	pages="50-64"
	}

	@article{
HHK03,
	author="Thomas A. Henzinger and Benjamin Horowitz and Christoph M. Kirsch", 
	title="{{\sc Giotto}}: {A} time-triggered language for embedded programming",
        journal="Proceedings of the IEEE",
        volume="91",
        year="2003",
	pages="84-99"
	}

	@incollection{
HHK03a,
	author="Thomas A. Henzinger and Benjamin Horowitz and Christoph M. Kirsch",
	title="Embedded control systems development with {{\sc Giotto}}",
	booktitle="Software-Enabled Control: Information Technology for Dynamical Systems",
        editor="Tariq Samad and Gary Balas",
	publisher="Wiley",
	year="2003",
	pages="123-146"
	}

        @incollection{
HKM03a,
        author="Thomas A. Henzinger and Orna Kupferman and Rupak Majumdar",
        title="On the universal and existential fragments of the mu-calculus",
        booktitle="TACAS: Tools and Algorithms for the Construction and Analysis of Systems",
        series="Lecture Notes in Computer Science 2619",
        publisher="Springer", 
        year="2003",
        pages="49-64"
        }

        @incollection{
HJMS03,
        author="Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar and Gr\'egoire Sutre",
        title="Software verification with {{\sc Blast}}",
        booktitle="SPIN: Model Checking of Software",
        series="Lecture Notes in Computer Science 2648",
        publisher="Springer", 
        year="2003",
        pages="235-239"
        }

	@incollection{
CMMZ+03,
	author="Krishnendu Chatterjee and Di Ma and Rupak Majumdar and Tian Zhao and Thomas A. Henzinger and Jens Palsberg",
	title="Stack size analysis for interrupt-driven programs",
	booktitle="SAS: Static Analysis",
	series="Lecture Notes in Computer Science 2694",
	publisher="Springer",
        year="2003",
        pages="109-126"
	}

	@incollection{
HJM03,
	author="Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar",
        title="Counterexample-guided control",
	booktitle="ICALP: Automata, Languages, and Programming",
	series="Lecture Notes in Computer Science 2719",
	publisher="Springer",
        year="2003",
        pages="886-902"
	}

	@incollection{
AHM03,
	author="Luca de Alfaro and Thomas A. Henzinger and Rupak Majumdar",
        title="Discounting the future in systems theory",
	booktitle="ICALP: Automata, Languages, and Programming",
	series="Lecture Notes in Computer Science 2719",
	publisher="Springer",
        year="2003",
        pages="1022-1037"
	}

        @incollection{
HJMQ03,
        author="Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar and Shaz Qadeer",
        title="Thread-modular abstraction refinement",
        booktitle="CAV: Computer-Aided Verification",
	series="Lecture Notes in Computer Science 2725",
	publisher="Springer",
        year="2003",
        pages="262-274"
        }

        @incollection{
AFHM+03,
        author="Luca de Alfaro and Marco Faella and Thomas A. Henzinger and Rupak Majumdar and Marielle Stoelinga",
        title="The element of surprise in timed games",
	booktitle="CONCUR: Concurrency Theory",
	series="Lecture Notes in Computer Science 2761",
	publisher="Springer",
        year="2003",
        pages="144-158"
        }

	@incollection{
CJH03,
	author="Krishnendu Chatterjee and Marcin Jurdzi\'nski and Thomas A. Henzinger",
	title="Simple stochastic parity games",
	booktitle="CSL: Computer Science Logic",
	series="Lecture Notes in Computer Science 2803", 
	publisher="Springer", 
        year="2003",
        pages="100-113"
        }

        @incollection{
CAHS03,
        author="Arindam Chakrabarti and Luca de Alfaro and Thomas A. Henzinger and Marielle Stoelinga",
        title="Resource interfaces",
	booktitle="EMSOFT: Embedded Software",
	series="Lecture Notes in Computer Science 2855", 
	publisher="Springer", 
        year="2003",
        pages="117-133"
        }

        @incollection{
HKM03,
        author="Thomas A. Henzinger and Christoph M. Kirsch and Slobodan Matic",
        title="Schedule-carrying code",
	booktitle="EMSOFT: Embedded Software",
	series="Lecture Notes in Computer Science 2855", 
	publisher="Springer", 
        year="2003",
        pages="241-256"
        }

	@article{
HKQ03,
	author="Thomas A. Henzinger and Orna Kupferman and Shaz Qadeer",
        title="From {\em pre\/}historic to {\em post\/}modern symbolic model checking", 
	journal="Formal Methods in System Design",
	volume="23",
	year="2003",
	pages="303-327"
	}

        @incollection{
HJMS04,
        author="Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar and Marco A.A. Sanvido",
        title="Extreme model checking",
        booktitle="Verification: Theory and Practice",
	series="Lecture Notes in Computer Science 2772",
	publisher="Springer",
        year="2004",
        pages="332-358"
	}

	@incollection{
CJH04,
	author="Krishnendu Chatterjee and Marcin Jurdzi\'nski and Thomas A. Henzinger",
	title="Quantitative stochastic parity games",
	booktitle="SODA: Discrete Algorithms",
        publisher="ACM",
        year="2004",
        pages="114-123"
        }

	@inproceedings{
HJMM04,
	author="Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar and Kenneth L. McMillan",
	title="Abstractions from proofs",
	booktitle="POPL: Principles of Programming Languages",
	publisher="ACM",
	year="2004",
        pages="232-244"
	}

        @incollection{
AFHM+04,
        author="Luca de Alfaro and Marco Faella and Thomas A. Henzinger and Rupak Majumdar and Marielle Stoelinga",
        title="Model checking discounted temporal properties",
        booktitle="TACAS: Tools and Algorithms for the Construction and Analysis of Systems",
        series="Lecture Notes in Computer Science 2988",
        publisher="Springer", 
        year="2004",
        pages="77-92"
        }

        @incollection{
GHKS04,
        author="Arkadeb Ghosal and Thomas A. Henzinger and Christoph M. Kirsch and Marco A.A. Sanvido",
        title="Event-driven programming with logical execution times",
        booktitle="HSCC: Hybrid Systems---Computation and Control",
        series="Lecture Notes in Computer Science 2993",
        publisher="Springer",
        year="2004",
        pages="357-371"
        }

        @inproceedings{
BCHJ+04,
        author="Dirk Beyer and Adam Chlipala and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar",
        title="Generating tests from counterexamples",
        booktitle="ICSE: Software Engineering",
        publisher="IEEE Computer Society",
        year="2004",
        pages="326-335"
        }

        @inproceedings{
BHJM04,
        author="Dirk Beyer and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar",
        title="An {E}clipse plug-in for model checking",
        booktitle="IWPC: Program Comprehension",
        publisher="IEEE Computer Society",
        year="2004",
        pages="251-257"
        }

	@inproceedings{
HJM04,
	author="Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar",
	title="Race checking by context inference",
	booktitle="PLDI: Programming Language Design and Implementation",
	publisher="ACM",
	year="2004",
        pages="1-13"
	}

	@incollection{
CHJH04,
	author="Krishnendu Chatterjee and Thomas A. Henzinger and Marcin Jurdzi\'nski",
	title="Games with secure equilibria",
	booktitle="LICS: Logic in Computer Science",
	publisher="IEEE Computer Society",
        year="2004",
        pages="160-169"
        }

	@incollection{
BCHJ+04a,
        author="Dirk Beyer and Adam Chlipala and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar",
        title="The {{\sc Blast}} query language for software verification",
	booktitle="SAS: Static Analysis",
	series="Lecture Notes in Computer Science 3148",
	publisher="Springer",
        year="2004",
        pages="2-18"
	}

        @inproceedings{
HenKir04,
        author="Thomas A. Henzinger and Christoph M. Kirsch",
        title="A typed assembly language for real-time programs",
	booktitle="EMSOFT: Embedded Software",
	publisher="ACM", 
        year="2004",
        pages="104-113"
        }

        @inproceedings{
CAH04,
        author="Krishnendu Chatterjee and Luca de Alfaro and Thomas A. Henzinger",
        title="Trading memory for randomness",
        booktitle="QEST: Quantitative Evaluation of Systems",
        publisher="IEEE Computer Society",
        year="2004",
        pages="206-217"
        }

	@article{
CMMZ+04,
	author="Krishnendu Chatterjee and Di Ma and Rupak Majumdar and Tian Zhao and Thomas A. Henzinger and Jens Palsberg",
	title="Stack size analysis for interrupt-driven programs",
	journal="Information and Computation",
	volume="194",
	year="2004",
	pages="144-174"
	}

        @article{
AFHM+05,
        author="Luca de Alfaro and Marco Faella and Thomas A. Henzinger and Rupak Majumdar and Marielle Stoelinga",
        title="Model checking discounted temporal properties",
	journal="Theoretical Computer Science",
	volume="345",
	year="2005",
	pages="139-170"
	}

	@article{
HMR05,
	author="Thomas A. Henzinger and Rupak Majumdar and Jean-Fran\c{c}ois Raskin",
	title="A classification of symbolic transition systems", 
	journal="ACM Transactions on Computational Logic",
	volume="6",
	year="2005",
	pages="1-32"
	}

        @inproceedings{
ChaHen05,
        author="Krishnendu Chatterjee and Thomas A. Henzinger",
        title="Semiperfect-information games",
        booktitle="FSTTCS: Foundations of Software Technology and Theoretical Computer Science",
        series="Lecture Notes in Computer Science 3821",
        publisher="Springer", 
        year="2005",
        pages="1-18"
        }

        @inproceedings{
AlfHen05,
        author="Luca de Alfaro and Thomas A. Henzinger",
        title="Interface-based design",
        booktitle="Engineering Theories of Software-intensive Systems",
        editor="Manfred Broy and Johannes Gr\"unbauer and David Harel and C.A.R. Hoare",
	series="NATO Science Series: Mathematics, Physics, and Chemistry 195",
        publisher="Springer",
        year="2005",
        pages="83-104"
        }

        @inproceedings{
BHJM05,
        author="Dirk Beyer and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar",
        title="Checking memory safety with {{\sc Blast}}",
        booktitle="FASE: Fundamental Approaches to Software Engineering",
        series="Lecture Notes in Computer Science 3442",
        publisher="Springer", 
        year="2005",
        pages="2-18"
        }

        @inproceedings{
MatHen05,
        author="Slobodan Matic and Thomas A. Henzinger",
        title="Trading end-to-end latency for composability",
        booktitle="RTSS: Real-Time Systems Symposium",
        publisher="IEEE Computer Society",
        year="2005",
        pages="99-110"
        }

        @incollection{
DHR05,
        author="Laurent Doyen and Thomas A. Henzinger and Jean-Fran\c{c}ois Raskin",
        title="Automatic rectangular refinement of affine hybrid systems",
        booktitle="FORMATS: Formal Modeling and Analysis of Timed Systems",
        series="Lecture Notes in Computer Science 3829",
        publisher="Springer",
        year="2005",
        pages="144-161"
        }

        @incollection{
HMP05,
        author="Thomas A. Henzinger and Rupak Majumdar and Vinayak S. Prabhu",
        title="Quantifying similarities between timed systems",
        booktitle="FORMATS: Formal Modeling and Analysis of Timed Systems",
        series="Lecture Notes in Computer Science 3829",
        publisher="Springer",
        year="2005",
        pages="226-241"
        }

        @inproceedings{
CCHK+05,
        author="Arindam Chakrabarti and Krishnendu Chatterjee and Thomas A. Henzinger and Orna Kupferman and Rupak Majumdar",
        title="Verifying quantitative properties using bound functions",
        booktitle="CHARME: Correct Hardware Design and Verification Methods",
        series="Lecture Notes in Computer Science 3725",
        publisher="Springer",
        year="2005",
        pages="50-64"
        }

        @inproceedings{
HJM05,
        author="Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar",
        title="Permissive interfaces",
        booktitle="FSE: Foundations of Software Engineering",
        publisher="ACM",
        year="2005",
        pages="31-40"
        }

        @inproceedings{
CHJM05,
        author="Krishnendu Chatterjee and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar",
        title="Counterexample-guided planning",
        booktitle="UAI: Uncertainty in Artificial Intelligence",
        publisher="AUAI",
        year="2005",
        pages="104-111"
        }

        @inproceedings{
CAH05,
        author="Krishnendu Chatterjee and Luca de Alfaro and Thomas A. Henzinger", 
        title="The complexity of stochastic {R}abin and {S}treett games",
        booktitle="ICALP: Automata, Languages, and Programming",
        series="Lecture Notes in Computer Science 3580",
        publisher="Springer", 
        year="2005",
        pages="878-890"
        }

        @inproceedings{
CHJ05,
        author="Krishnendu Chatterjee and Thomas A. Henzinger and Marcin Jurdzi\'nski",
        title="Mean-payoff parity games",
        booktitle="LICS: Logic in Computer Science",
        publisher="IEEE Computer Society",
        year="2005",
        pages="178-187"
        }

        @inproceedings{
HKM05,
        author="Thomas A. Henzinger and Christoph M. Kirsch and Slobodan Matic",
        title="Composable code generation for distributed {{\sc Giotto}}",
        booktitle="LCTES: Languages, Compilers, and Tools for Embedded Systems",
        publisher="ACM",
        year="2005",
        pages="21-30"
        }

        @inproceedings{
KSH05,
        author="Christoph M. Kirsch and Marco A.A. Sanvido and Thomas A. Henzinger", 
        title="A programmable microkernel for real-time systems",
        booktitle="VEE: Virtual Execution Environments",
        publisher="ACM",
        year="2005",
        pages="35-45"
        }
 
        @inproceedings{
BCH05,
        author="Dirk Beyer and Arindam Chakrabarti and Thomas A. Henzinger", 
        title="Web service interfaces",
        booktitle="WWW: World-Wide Web Conference",
        year="2005",
        pages="148-159"
        }

        @inproceedings{
CAH06,
        author="Krishnendu Chatterjee and Luca de Alfaro and Thomas A. Henzinger",
        title="The complexity of quantitative concurrent parity games",
        booktitle="SODA: Discrete Algorithms",
        publisher="ACM", 
        year="2006",
        pages="678-687"
        }

        @inproceedings{
ChaHen06,
        author="Krishnendu Chatterjee and Thomas A. Henzinger",
        title="Finitary winning in omega-regular games",
        booktitle="TACAS: Tools and Algorithms for the Construction and Analysis of Systems",
        series="Lecture Notes in Computer Science 3920",
        publisher="Springer",
        year="2006",
        pages="257-271"
        }

        @inproceedings{
HenMat06,
        author="Thomas A. Henzinger and Slobodan Matic",
        title="An interface algebra for real-time components",
        booktitle="RTAS: Real-Time and Embedded Technology and Applications Symposium",
        publisher="IEEE Computer Society",
        year="2006",
        pages="253-266"
        }

        @inproceedings{
ChaHen06a,
        author="Krishnendu Chatterjee and Thomas A. Henzinger",
        title="Strategy improvement and randomized subexponential algorithms for stochastic parity games",
        booktitle="STACS: Theoretical Aspects of Computer Science",
        series="Lecture Notes in Computer Science 3884",
        publisher="Springer",
        year="2006",
        pages="512-523"
        }

        @inproceedings{
CMH06,
        author="Krishnendu Chatterjee and Rupak Majumdar and Thomas A. Henzinger",
        title="Markov decision processes with multiple objectives",
        booktitle="STACS: Theoretical Aspects of Computer Science",
        series="Lecture Notes in Computer Science 3884",
        publisher="Springer",
        year="2006",
        pages="325-336"
        }

        @article{
HKM06,
        author="Thomas A. Henzinger and Orna Kupferman and Rupak Majumdar",
        title="On the universal and existential fragments of the mu-calculus",
	journal="Theoretical Computer Science",
	volume="354",
	year="2006",
	pages="173-186"
	}

        @incollection{
DDHR06,
        author="Martin {De Wulf} and Laurent Doyen and Thomas A. Henzinger and Jean-Fran\c{c}ois Raskin",
        title="Antichains: {A} new algorithm for checking universality of finite automata",
        booktitle="CAV: Computer-Aided Verification",
	series="Lecture Notes in Computer Science 4144",
	publisher="Springer",
        year="2006",
        pages="17-30"
        }

        @incollection{
BHT06,
        author="Dirk Beyer and Thomas A. Henzinger and Gr\'egory Th\'eoduloz",
        title="Lazy shape analysis",
        booktitle="CAV: Computer-Aided Verification",
	series="Lecture Notes in Computer Science 4144",
	publisher="Springer",
        year="2006",
        pages="532-546"
        }

        @incollection{
ChaHen06b,
        author="Krishnendu Chatterjee and Thomas A. Henzinger",
        title="Strategy improvement for stochastic {R}abin and {S}treett games",
	booktitle="CONCUR: Concurrency Theory",
	series="Lecture Notes in Computer Science 4137",
	publisher="Springer",
        year="2006",
        pages="375-389"
        }

        @incollection{
HenSif06,
        author="Thomas A. Henzinger and Joseph Sifakis",
        title="The embedded systems design challenge",
        booktitle="FM: Formal Methods",
	series="Lecture Notes in Computer Science 4085",
	publisher="Springer",
        year="2006",
        pages="1-15"
        }

        @inproceedings{
CAH06a,
        author="Krishnendu Chatterjee and Luca de Alfaro and Thomas A. Henzinger",
        title="Strategy improvement for concurrent reachability games",
        booktitle="QEST: Quantitative Evaluation of Systems",
        publisher="IEEE Computer Society",
        year="2006",
        pages="291-300"
        }


        @inproceedings{
CAFH+06,
        author="Krishnendu Chatterjee and Luca de Alfaro and Marco Faella and Thomas A. Henzinger and Rupak Majumdar and Marielle Stoelinga",
        title="Compositional quantitative reasoning",
        booktitle="QEST: Quantitative Evaluation of Systems",
        publisher="IEEE Computer Society",
        year="2006",
        pages="179-188"
        }

	@incollection{
HenPit06,
	author="Thomas A. Henzinger and Nir Piterman",
	title="Solving games without determinization",
	booktitle="CSL: Computer Science Logic",
	series="Lecture Notes in Computer Science 4207", 
	publisher="Springer", 
        year="2006",
        pages="395-410"
        }

	@incollection{
CDHR06,
	author="Laurent Doyen and Krishnendu Chatterjee and Thomas A. Henzinger and Jean-Fran\c{c}ois Raskin",
	title="Algorithms for omega-regular games with imperfect information", 
	booktitle="CSL: Computer Science Logic",
	series="Lecture Notes in Computer Science 4207", 
	publisher="Springer", 
        year="2006",
        pages="287-302"
        }

        @incollection{
HenPra06,
        author="Thomas A. Henzinger and Vinayak S. Prabhu",
        title="Timed alternating-time temporal logic",
        booktitle="FORMATS: Formal Modeling and Analysis of Timed Systems",
        series="Lecture Notes in Computer Science 4202",
        publisher="Springer",
        year="2006",
        pages="1-17"
        }

        @inproceedings{
FisHen06,
        author="Jasmin Fisher and Thomas A. Henzinger",
        title="Executable biology",
        booktitle="WSC: Winter Simulation Conference",
        publisher="IEEE Computer Society",
        year="2006",
        pages="1675-1682"
        }

        @inproceedings{
GHIK+06,
        author="Arkadeb Ghosal and Thomas A. Henzinger and Daniel Iercan and Christoph M. Kirsch and Alberto L. Sangiovanni-Vincentelli",
        title="A hierarchical coordination language for interacting real-time tasks",
	booktitle="EMSOFT: Embedded Software",
	publisher="ACM", 
        year="2006",
        pages="131-141"
        }

	@inproceedings{
GHKN+06,
	author="Bhargav Gulavani and Thomas A. Henzinger and Yamini Kannan and Aditya Nori and Sriram K. Rajamani",
	title="{{\sc Synergy}}: {A} new algorithm for property checking",
	booktitle="FSE: Foundations of Software Engineering",
	publisher="ACM",
	year="2006",
        pages="117-127"
	}

        @article{
CHJ06,
        author="Krishnendu Chatterjee and Thomas A. Henzinger and Marcin Jurdzi\'nski",
        title="Games with secure equilibria",
        journal="Theoretical Computer Science",
        volume="365",
        year="2006",
        pages="67-82"
        }

        @incollection{
Hen07a,
        author="Thomas A. Henzinger",
        title="Games, time, and probability: {G}raph models for system design and analysis",
        booktitle="SOFSEM: Current Trends in Theory and Practice of Computer Science",
        series="Lecture Notes in Computer Science 4362",
        publisher="Springer",
        year="2007",
        pages="103-110"
        }

        @incollection{
CHP07,
        author="Krishnendu Chatterjee and Thomas A. Henzinger and Nir Piterman",
        title="Strategy logic",
        booktitle="CONCUR: Concurrency Theory",
        series="Lecture Notes in Computer Science 4703",
        publisher="Springer", 
        year="2007",
        pages="59-73"
        }

	@inproceedings{
BCHS07,
        author="Dirk Beyer and Arindam Chakrabarti and Thomas A. Henzinger and Sanjit A. Seshia",
        title="An application of web-service interfaces",
        booktitle="ICWS: Web Services",
        publisher="IEEE Computer Society", 
        year="2007",
        pages="831-838"
        }

        @incollection{
BHPR07,
        author="Thomas Brihaye and Thomas A. Henzinger and Vinayak S. Prabhu and Jean-Fran\c{c}ois Raskin",
        title="Minimum-time reachability in timed games",
        booktitle="ICALP: Automata, Languages, and Programming",
        series="Lecture Notes in Computer Science 4596",
        publisher="Springer", 
        year="2007",
        pages="825-837"
        }

        @incollection{
BHT07,
        author="Dirk Beyer and Thomas A. Henzinger and Gr\'egory Th\'eoduloz",
        title="Configurable software verification: {C}oncretizing the convergence of model checking and program analysis",
        booktitle="CAV: Computer-Aided Verification",
        series="Lecture Notes in Computer Science 4590",
        publisher="Springer", 
        year="2007", 
        pages="509-523"
        }

        @incollection{
Hen07,
        author="Thomas A. Henzinger",
        title="Quantitative generalizations of languages",
        booktitle="DLT: Developments in Language Theory",
        series="Lecture Notes in Computer Science 4588",
        publisher="Springer", 
        year="2007",
        pages="20-22"
        }

        @incollection{
BHS07,
        author="Dirk Beyer and Thomas A. Henzinger and Vasu Singh",
        title="Algorithms for interface synthesis",
        booktitle="CAV: Computer-Aided Verification",
        series="Lecture Notes in Computer Science 4590",
        publisher="Springer", 
        year="2007",
        pages="4-19"
        }

	@inproceedings{
BHMR07,
        author="Dirk Beyer and Thomas A. Henzinger and Rupak Majumdar and Andrey Rybalchenko",
        title="Path invariants",
        booktitle="PLDI: Programming Language Design and Implementation",
        publisher="ACM", 
        year="2007",
        pages="300-309"
        }

        @incollection{
ChaHen07,
        author="Krishnendu Chatterjee and Thomas A. Henzinger",
        title="Assume-guarantee synthesis",
        booktitle="TACAS: Tools and Algorithms for the Construction and Analysis of Systems",
        series="Lecture Notes in Computer Science 4424",
        publisher="Springer", 
        year="2007",
        pages="261-275"
        }

        @incollection{
CHP07a,
        author="Krishnendu Chatterjee and Thomas A. Henzinger and Nir Piterman",
        title="Generalized parity games",
        booktitle="FOSSACS: Foundations of Software Science and Computation Structures",
        series="Lecture Notes in Computer Science 4423",
        publisher="Springer", 
        year="2007",
        pages="153-167"
        }

        @incollection{
MFHR+07, 
        author="Roman Manevich and John Field and Thomas A. Henzinger and Ganesan Ramalingam and Mooly Sagiv",
        title="Abstract counterexample-based refinement for powerset domains",
        booktitle="Program Analysis and Compilation: Theory and Practice",
        series="Lecture Notes in Computer Science 4444",
        publisher="Springer", 
        year="2007",
        pages="273-292"
        }

        @incollection{
BHMR07a,
        author="Dirk Beyer and Thomas A. Henzinger and Rupak Majumdar and Andrey Rybalchenko",
        title="Invariant synthesis for combined theories",
        booktitle="VMCAI: Verification, Model Checking, and Abstract Interpretation",
        series="Lecture Notes in Computer Science 4349",
        publisher="Springer", 
        year="2007",
        pages="378-394"
        }

        @article{
FPHH07,
        author="Jasmin Fisher and Nir Piterman and Alex Hajnal and Thomas A. Henzinger",
        title="Predictive modeling of signaling crosstalk during {C}.~elegans vulval development",
        journal="PLoS Computational Biology", 
        volume="3(5):e92", 
        year="2007"
        }

        @article{
SHF07,
        author="Marc A. Schaub and Thomas A. Henzinger and Jasmin Fisher",
        title="Qualitative networks: {A} symbolic approach to analyze biological signaling networks",
        journal="BMC Systems Biology",
        volume="1:4", 
        year="2007"
        }

	@book{
DupHen07,
	title="CSL: Computer Science Logic",
        editor="Jacques Duparc and Thomas A. Henzinger",
	series="Lecture Notes in Computer Science 4646",
	publisher="Springer",
        year="2007"
	}

        @article{
HenKir07,
        author="Thomas A. Henzinger and Christoph M. Kirsch",
        title="The {E}mbedded {M}achine: {P}redictable, portable real-time code",
	journal="ACM Transactions on Programming Languages and Systems",
	volume="29(6)",
	year="2007"
	}

        @article{
BHJM07, 
        author="Dirk Beyer and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar",
        title="The software model checker {{\sc Blast}}: {A}pplications to software engineering",
        journal="Software Tools for Technology Transfer",
        volume="9",
        year="2007",
        pages="505-526"
        }

        @article{
HenSif07,
        authoor="Thomas A. Henzinger and Joseph Sifakis",
        title="The discipline of embedded systems design",
        journal="IEEE Computer",
        volume="40(10)",
        year="2007",
        pages="36-44"
        }

        @article{
FisHen07,
        author="Jasmin Fisher and Thomas A. Henzinger",
        title="Executable cell biology",
        journal="Nature Biotechnology",
        volume="25",
        year="2007",
        pages="1239-1249"
        }

        @article{
CDHR07, 
        author="Krishnendu Chatterjee and Laurent Doyen and Thomas A. Henzinger and Jean-Fran\c{c}ois Raskin",
        title="Algorithms for omega-regular games with imperfect information",
        journal="Logical Methods in Computer Science",
        volume="3(3)",
        year="2007"
        }

        @article{
AHK07, 
        author="Luca de Alfaro and Thomas A. Henzinger and Orna Kupferman",
        title="Concurrent reachability games",
        journal="Theoretical Computer Science",
        volume="386",
        year="2007",
        pages="188-217"
        }
 
        @article{
DHR08, 
        author="Laurent Doyen and Thomas A. Henzinger and Jean-Fran\c{c}ois Raskin",
        title="Equivalence of labeled {M}arkov chains",
        journal="International Journal of Foundations of Computer Science",
        volume="19",
        year="2008",
        pages="549-563"
        }

        @incollection{
ChaHen08a,
        author="Krishnendu Chatterjee and Thomas A. Henzinger",
        title="Value iteration",
        booktitle="25 Years of Model Checking",
        series="Lecture Notes in Computer Science 5000",
        publisher="Springer", 
        year="2008",
        pages="107-138"
        }

        @article{
CMH08a,
        author="Krishnendu Chatterjee and Rupak Majumdar and Thomas A. Henzinger",
        title="Stochastic limit-average games are in {EXPTIME}",
        journal="International Journal of Game Theory",
        volume="37",
        year="2008",
        pages="219-234"
        }

        @inproceedings{
DHJP08,
        author="Laurent Doyen and Thomas A. Henzinger and Barbara Jobstmann and Tatjana Petrov",
        title="Interface theories with component reuse",
	booktitle="EMSOFT: Embedded Software",
	publisher="ACM", 
        year="2008",
        pages="79-88"
        }

	@incollection{
CDH08,
	author="Krishnendu Chatterjee and Laurent Doyen and Thomas A. Henzinger",
	title="Quantitative languages",
	booktitle="CSL: Computer Science Logic",
	series="Lecture Notes in Computer Science 5213", 
	publisher="Springer", 
        year="2008",
        pages="385-400"
        }

        @incollection{
BCDH+08,
        author="Dietmar Berwanger and Krishnendu Chatterjee and Laurent Doyen and Thomas A. Henzinger and Sangram Raje",
        title="Strategy construction for parity games with imperfect information",
        booktitle="CONCUR: Concurrency Theory 5201",
        series="Lecture Notes in Computer Science",
        publisher="Springer", 
        year="2008",
        pages="325-339"
        }

        @incollection{
CHJ08,
        author="Krishnendu Chatterjee and Thomas A. Henzinger and Barbara Jobstmann",
        title="Environment assumptions for synthesis",
        booktitle="CONCUR: Concurrency Theory",
        series="Lecture Notes in Computer Science 5201",
        publisher="Springer", 
        year="2008",
        pages="147-161"
        }

        @incollection{
GHS08a,
        author="Rachid Guerraoui and Thomas A. Henzinger and Vasu Singh",
        title="Completeness and nondeterminism in model checking transactional memories",
        booktitle="CONCUR: Concurrency Theory 5201",
        series="Lecture Notes in Computer Science",
        publisher="Springer", 
        year="2008",
        pages="21-35"
        }

        @incollection{
FHMP08,
        author="Jasmin Fisher and Thomas A. Henzinger and Maria Mateescu and Nir Piterman",
        title="Bounded asynchrony: {C}oncurrency for modeling cell-cell interactions",
        booktitle="FMSB: Formal Methods in Systems Biology",
        series="Lecture Notes in Bioinformatics 5054",
        publisher="Springer", 
        year="2008",
        pages="17-32"
        }

	@inproceedings{
GHJS08,
        author="Rachid Guerraoui and Thomas A. Henzinger and Barbara Jobstmann and Vasu Singh",
        title="Model checking transactional memories",
        booktitle="PLDI: Programming Language Design and Implementation",
        publisher="ACM", 
        year="2008",
        pages="372-382"
        }

	@inproceedings{
GHMR+08,
	author="Ashutosh Gupta and Thomas A. Henzinger and Rupak Majumdar and Andrey Rybalchenko",
	title="Proving non-termination",
	booktitle="POPL: Principles of Programming Languages",
	publisher="ACM",
	year="2008",
        pages="147-158"
	}

	@inproceedings{
BHT08,
	author="Dirk Beyer and Thomas A. Henzinger and Gr\'egory Theoduloz",
	title="Program analysis with dynamic change of precision",
	booktitle="ASE: Automated Software Engineering",
	publisher="ACM",
	year="2008",
        pages="29-38"
	}

	@inproceedings{
CGHI+08,
	author="Krishnendu Chatterjee and Arkadeb Ghosal and Thomas A. Henzinger and Daniel Iercan and Christoph M. Kirsch and Claudio Pinello and Alberto L. Sangiovanni-Vincentelli",
	title="Logical reliability of interacting real-time tasks",
	booktitle="DATE: Design, Automation, and Test in Europe",
        publisher="IEEE",
	year="2008",
        pages="909-914"
	}

        @incollection{
CHP08a,
        author="Krishnendu Chatterjee and Thomas A. Henzinger and Vinayak S. Prabhu",
        title="Trading infinite memory for uniform randomness in timed games",
        booktitle="HSCC: Hybrid Systems---Computation and Control",
        series="Lecture Notes in Computer Science 4981",
        publisher="Springer",
        year="2008",
        pages="87-100"
        }

        @incollection{
CMH08,
        author="Krishnendu Chatterjee and Rupak Majumdar and Thomas A. Henzinger",
        title="Controller synthesis with budget constraints",
        booktitle="HSCC: Hybrid Systems---Computation and Control",
        series="Lecture Notes in Computer Science 4981",
        publisher="Springer",
        year="2008",
        pages="72-86"
        }

        @incollection{
CSH08,
        author="Krishnendu Chatterjee and Koushik Sen and Thomas A. Henzinger",
        title="Model checking omega-regular properties of interval {M}arkov chains",
        booktitle="FOSSACS: Foundations of Software Science and Computation Structures",
        series="Lecture Notes in Computer Science 4962",
        publisher="Springer", 
        year="2008",
        pages="302-317"
        }

        @incollection{
CHP08,
        author="Krishnendu Chatterjee and Thomas A. Henzinger and Vinayak S. Prabhu",
        title="Timed parity games: {C}omplexity and robustness",
        booktitle="FORMATS: Formal Modeling and Analysis of Timed Systems",
        series="Lecture Notes in Computer Science 5215",
        publisher="Springer",
        year="2008",
        pages="124-140"
        }

        @incollection{
GHS08,
        author="Rachid Guerraoui and Thomas A. Henzinger and Vasu Singh",
        title="Permissiveness in transactional memories",
        booktitle="DISC: Distributed Computing",
        series="Lecture Notes in Computer Science 5218",
        publisher="Springer", 
        year="2008",
        pages="305-319"
        }

	@article{
ChaHen08,
	author="Krishnendu Chatterjee and Thomas A. Henzinger",
	title="Reduction of stochastic parity to stochastic mean-payoff games",
        journal="Information Processing Letters",
        volume="106",
        year="2008",
        pages="1-7"
	}

	@article{
Hen08,
	author="Thomas A. Henzinger",
	title="Two challenges in embedded systems design: {P}redictability and robustness",
        journal="Philosophical Transactions of the Royal Society~A",
        volume="366",
        year="2008",
        pages="3727-3736"
	}

        @incollection{
HHK08,
        author="Thomas A. Henzinger and Thibaud B. Hottelier and Laura Kov\'acs",
        title="{{\sc Valigator}}: {A} verification tool with bound and invariant generation",
        booktitle="LPAR: Logic for Programming, Artificial Intelligence, and Reasoning",
        series="Lecture Notes in Artificial Intelligence 5330",
        publisher="Springer", 
        year="2008",
        pages="333-342"
        }

	@incollection{
CAH09,
	author="Krishnendu Chatterjee and Luca de Alfaro and Thomas A. Henzinger",
	title="Termination criteria for solving concurrent safety and reachability games", 
	booktitle="SODA: Discrete Algorithms",
        publisher="ACM",
        year="2009",
        pages="197-206"
        }

        @incollection{
GHS09,
        author="Rachid Guerraoui and Thomas A. Henzinger and Vasu Singh",
        title="Software transactional memory on relaxed memory models",
        booktitle="CAV: Computer-Aided Verification",
        series="Lecture Notes in Computer Science 5643",
        publisher="Springer", 
        year="2009",
        pages="321-336"
        }

        @incollection{
HMW09,
        author="Thomas A. Henzinger and Maria Mateescu and Verena Wolf",
        title="Sliding-window abstraction for infinite {M}arkov chains",
        booktitle="CAV: Computer-Aided Verification",
        series="Lecture Notes in Computer Science 5643",
        publisher="Springer", 
        year="2009",
        pages="337-352"
        }

        @incollection{
BCHJ09,
        author="Roderick Bloem and Krishnendu Chatterjee and Thomas A. Henzinger and Barbara Jobstmann",
        title="Better quality in synthesis through quantitative objectives",
        booktitle="CAV: Computer-Aided Verification",
        series="Lecture Notes in Computer Science 5643",
        publisher="Springer", 
        year="2009",
        pages="140-156"
        }

        @incollection{
BCWD+09,
        author="Dietmar Berwanger and Krishnendu Chatterjee and Martin {De Wulf} and Laurent Doyen and Thomas A. Henzinger", 
        title="{{\sc Alpaga}}: {A} tool for solving parity games with imperfect information",
        booktitle="TACAS: Tools and Algorithms for the Construction and Analysis of Systems",
        series="Lecture Notes in Computer Science 5505",
        publisher="Springer", 
        year="2009",
        pages="58-61"
        }

        @incollection{
CDH09a,
        author="Krishnendu Chatterjee and Laurent Doyen and Thomas A. Henzinger",
        title="A survey of stochastic games with limsup and liminf objectives",
        booktitle="ICALP: Automata, Languages, and Programming",
        series="Lecture Notes in Computer Science 5556, Part II",
        publisher="Springer", 
        year="2009",
        pages="1-15"
        }

        @incollection{
CHH09,
        author="Krishnendu Chatterjee and Thomas A. Henzinger and Florian Horn",
        title="Stochastic games with finitary objectives",
        booktitle="MFCS: Mathematical Foundations of Computer Science",
        series="Lecture Notes in Computer Science 5734",
        publisher="Springer", 
        year="2009",
        pages="34-54"
        }


        @incollection{
CDH09,
        author="Krishnendu Chatterjee and Laurent Doyen and Thomas A. Henzinger",
        title="Expressiveness and closure properties for quantitative languages",
        booktitle="LICS: Logic in Computer Science",
        publisher="IEEE Computer Society",
        year="2009",
        pages="199-208"
        }

%%%%%%%%%%%%%%%%%%%%% IST Austria %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

        @incollection{
HJW09,
        author="Thomas A. Henzinger and Barbara Jobstmann and Verena Wolf",
        title="Formalisms for specifying {M}arkovian population models",
        booktitle="RP: Reachability Problems",
        series="Lecture Notes in Computer Science 5797",
        publisher="Springer", 
        year="2009",
        pages="3-23"
        }

        @incollection{
CDH09b,
        author="Krishnendu Chatterjee and Laurent Doyen and Thomas A. Henzinger",
        title="Probabilistic weighted automata",
        booktitle="CONCUR: Concurrency Theory",
        series="Lecture Notes in Computer Science 5710",
        publisher="Springer", 
        year="2009",
        pages="244-258"
        }

        @incollection{
CDH09c,
        author="Krishnendu Chatterjee and Laurent Doyen and Thomas A. Henzinger",
        title="Alternating weighted automata",
        booktitle="FCT: Fundamentals of Computation Theory",
        series="Lecture Notes in Computer Science 5699",
        publisher="Springer", 
        year="2009",
        pages="3-13"
        }

        @incollection{
DHMW09,
        author="Fr\'ed\'eric Didier and Thomas A. Henzinger and Maria Mateescu and Verena Wolf",
        title="Approximation of event probabilities in noisy cellular processes", 
        booktitle="CMSB: Computational Methods in Systems Biology",
        series="Lecture Notes in Bioinformatics 5688",
        publisher="Springer", 
        year="2009",
        pages="173-188"
        }

        @article{
CHH09a,
        author="Krishnendu Chatterjee and Thomas A. Henzinger and Florian Horn",
        title="Finitary winning in omega-regular games",
        journal="ACM Transactions on Computational Logic", 
        volume="11(1)",
        year="2009"
        }

	@inproceedings{
HKMS09,
        author="Thomas A. Henzinger and Christoph M. Kirsch and Eduardo R.B. Marques and Ana Sokolova",
        title="Distributed, modular {{\sc Htl}}",
        booktitle="RTSS: Real-Time Systems Symposium",
        publisher="IEEE Computer Society",
        year="2009",
        pages="171-180"
        }

	@inproceedings{
BGHJ09,
        author="Roderick Bloem and Karin Greimel and Thomas A. Henzinger and Barbara Jobstmann",
        title="Synthesizing robust systems",
        booktitle="FMCAD: Formal Methods in Computer-Aided Design",
        publisher="IEEE Computer Society",
        year="2009",
        pages="85-92"
        }

	@inproceedings{
TLHL09,
        author="Stavros Tripakis and Ben Lickly and Thomas A. Henzinger and Edward A. Lee",
        title="On relational interfaces",
        booktitle="EMSOFT: Embedded Software", 
        publisher="ACM", 
        year="2009",
        pages="67-76"
        }

	@inproceedings{
DHMW09a,
        author="Fr\'ed\'eric Didier and Thomas A. Henzinger and Maria Mateescu and Verena Wolf", 
        title="Fast adaptive uniformization of the chemical master equation",
        booktitle="HIBI: High-Performance Computational Systems Biology",
        publisher="IEEE Computer Society",
        year="2009"
        }

        @incollection{
CDHR10,
        author="Krishnendu Chatterjee and Laurent Doyen and Thomas A. Henzinger and Jean-Fran\c{c}ois Raskin",
        title="Generalized mean-payoff and energy games",
        booktitle="FSTTCS: Foundations of Software Technology and Theoretical Computer Science",
        series="Lecture Notes in Computer Science",
        publisher="Springer", 
        year="2010"
        }

        @incollection{
HMMW10,
        author="Thomas A. Henzinger and Maria Mateescu and Linar Mikeev and Verena Wolf",
        title="Hybrid numerical solution of the chemical master equation",
        booktitle="CMSB: Computational Methods in Systems Biology",
        series="Lecture Notes in Bioinformatics",
        publisher="Springer", 
        year="2010"
        }

	@inproceedings{
DMWH10,
        author="Fr\'ed\'eric Didier and Maria Mateescu and Verena Wolf and Thomas A. Henzinger",
        title="{{\sc Sabre}}: {A} tool for the stochastic analysis of biochemical reaction networks",
        booktitle="QEST: Quantitative Evaluation of Systems",
        publisher="IEEE Computer Society",
        year="2010"
        }

        @incollection{
HHK10,
        author="Thomas A. Henzinger and Thibaud B. Hottelier and Laura Kov\'acs",
        title="Aligators for arrays",
        booktitle="LPAR: Logic for Programming, Artificial Intelligence, and Reasoning", 
        series="Lecture Notes in Artificial Intelligence 6397",
        publisher="Springer", 
        year="2010",
        pages="348-356"
        }

        @incollection{
CHR10,
        author="Pavol Cern\'y and Thomas A. Henzinger and Arjun Radhakrishna",
        title="Simulation distances",
        booktitle="CONCUR: Concurrency Theory",
        series="Lecture Notes in Computer Science 6269",
        publisher="Springer", 
        year="2010",
        pages="253-268"
        }

        @incollection{
CDEH+10,
        author="Krishnendu Chatterjee and Laurent Doyen and Herbert Edelsbrunner and Thomas A. Henzinger and Philippe Rannou",
        title="Mean-payoff automaton expressions",
        booktitle="CONCUR: Concurrency Theory", 
        series="Lecture Notes in Computer Science 6269",
        publisher="Springer", 
        year="2010",
        pages="269-283"
        }

        @incollection{
CDH10,
        author="Krishnendu Chatterjee and Laurent Doyen and Thomas A. Henzinger", 
        title="Qualitative analysis of partially observable {M}arkov decision processes",
        booktitle="MFCS: Mathematical Foundations of Computer Science",
        series="Lecture Notes in Computer Science 6281",
        publisher="Springer", 
        year="2010",
        pages="258-269"
        }

        @incollection{
CDGH10,
        author="Krishnendu Chatterjee and Laurent Doyen and Hugo Gimbert and Thomas A. Henzinger", 
        title="Randomness for free",
        booktitle="MFCS: Mathematical Foundations of Computer Science",
        series="Lecture Notes in Computer Science 6281",
        publisher="Springer", 
        year="2010",
        pages="246-257"
        }

        @incollection{
CHJS10",
        author="Krishnendu Chatterjee and Thomas A. Henzinger and Barbara Jobstmann and Rohit Singh",
        title="Measuring and synthesizing systems in probabilistic environments",
        booktitle="CAV: Computer-Aided Verification",
        series="Lecture Notes in Computer Science 6174",
        publisher="Springer",
        year="2010",
        pages="380-395"
        }

        @incollection{
BCGH+10,
        author="Roderick Bloem and Krishnendu Chatterjee and Karin Greimel and Thomas A. Henzinger and Barbara Jobstmann", 
        title="Robustness in the presence of liveness",
        booktitle="CAV: Computer-Aided Verification",
        series="Lecture Notes in Computer Science 6174",
        publisher="Springer",
        year="2010",
        pages="410-424"
        }

        @incollection{
CHJR10,
        author="Krishnendu Chatterjee and Thomas A. Henzinger and Barbara Jobstmann and Arjun Radhakrishna",
        title="{{\sc Gist}}: {A} solver for probabilistic games",
        booktitle="CAV: Computer-Aided Verification",
        series="Lecture Notes in Computer Science 6174",
        publisher="Springer",
        year="2010",
        pages="665-669"
        }

	@inproceedings{
DHLN10,
        author="Laurent Doyen and Thomas A. Henzinger and Axel Legay and Dejan Ni\v{c}kovi\'c", 
        title="Robustness of sequential circuits",
        booktitle="ACSD: Application of Concurrency to System Design",
        publisher="IEEE Computer Society", 
        year="2010"
        }

        @incollection{
BHTZ10,
        author="Dirk Beyer and Thomas A. Henzinger and Gr\'egory Th\'eoduloz and Damien Zufferey",
        title="Shape refinement through explicit heap analysis",
        booktitle="FASE: Fundamental Approaches to Software Engineering",
        series="Lecture Notes in Computer Science 6013",
        publisher="Springer", 
        year="2010",
        pages="263-277"
        }

        @incollection{
WZH10,
        author="Thomas Wies and Damien Zufferey and Thomas A. Henzinger",
        title="Forward analysis of depth-bounded processes",
        booktitle="FOSSACS: Foundations of Software Science and Computational Structures",
        series="Lecture Notes in Computer Science 6014",
        publisher="Springer", 
        year="2010",
        pages="94-108"
        }

	@inproceedings{
GHKS10,
        author="Rachid Guerraoui and Thomas A. Henzinger and Michal Kapalka and Vasu Singh",
        title="Transactions in the jungle",
        booktitle="SPAA: Parallel Algorithms and Architectures",
        publisher="ACM", 
        year="2010", 
        pages="263-272"
        }

	@inproceedings{
HSSW+10a,
        author="Thomas A. Henzinger and Anmol V. Singh and Vasu Singh and Thomas Wies and Damien Zufferey",
        title="{{\sc FlexPrice}}: {F}lexible provisioning of resources in a cloud environment",
        booktitle="CLOUD: Cloud Computing",
        publisher="IEEE Computer Society",
        year="2010"
        }

        @incollection{
HHKV10,
        author="Thomas A. Henzinger and Thibaud B. Hottelier and Laura Kov\'acs and Andrei Voronkov",
        title="Invariant and type inference for matrices",
        booktitle="VMCAI: Verification, Model Checking, and Abstract Interpretation",
        series="Lecture Notes in Computer Science 5944",
        publisher="Springer", 
        year="2010",
        pages="163-179"
        }

	@inproceedings{
HSSW+10,
        author="Thomas A. Henzinger and Anmol V. Singh and Vasu Singh and Thomas Wies and Damien Zufferey",
        title="A marketplace for cloud resources",
        booktitle="EMSOFT: Embedded Software",
        publisher="ACM", 
        year="2010"
        }

        @incollection{
ChaHen10a,
        author="Krishnendu Chatterjee and Thomas A. Henzinger",
        title="Probabilistic automata on infinite words: {D}ecidability and undecidability results",
        booktitle="ATVA: Automated Technology for Verification and Analysis",
        series="Lecture Notes in Computer Science 6252",
        publisher="Springer", 
        year="2010",
        pages="1-16"
        }

        @incollection{
CHR10a,
        author="Pavol Cern\'y and Thomas A. Henzinger and Arjun Radhakrishna",
        title="Quantitative simulation games",
        booktitle="Time for Verification: Essays in Memory of Amir Pnueli",
        series="Lecture Notes in Computer Science 6200",
        publisher="Springer", 
        year="2010",
        pages="42-60"
        }

	@inproceedings{
Hen10,
        author="Thomas A. Henzinger",
        title="From boolean to quantitative notions of correctness",
        booktitle="POPL: Principles of Programming Languages",
        publisher="ACM",
        year="2010",
        pages="157-158"
        }

        @article{
CDH10b,
        author="Krishnendu Chatterjee and Laurent Doyen and Thomas A. Henzinger",
        title="Quantitative languages",
        journal="ACM Transactions on Computational Logic", 
        volume="11(4)",
        year="2010"
        }

        @article{
GIKH+10,
        author="Arkadeb Ghosal and Daniel Iercan and Christoph M. Kirsch and Thomas A. Henzinger and Alberto L. Sangiovanni-Vincentelli", 
        title="Separate compilation of hierarchical real-time programs into linear-bounded embedded machine code",
        journal="Science of Computer Programming",
        year="2010"
        }

        @article{
CDH10a,
        author="Krishnendu Chatterjee and Laurent Doyen and Thomas A. Henzinger",
        title="Expressiveness and closure properties for quantitative languages",
        journal="Logical Methods in Computer Science", 
        volume="6(3)",
        year="2010"
        }

        @article{
WGMH10,
        author="Verena Wolf and Rushil Goel and Maria Mateescu and Thomas A. Henzinger",
        title="Solving the chemical master equation using sliding windows",
        journal="BMC Systems Biology", 
        volume="4:42", 
        year="2010
        }

        @article{
CHP10,
        author="Krishnendu Chatterjee and Thomas A. Henzinger and Vinayak S. Prabhu", 
        title="Timed parity games: {C}omplexity and robustness",
        journal="Logical Methods in Computer Science",
        year="In press"
        }

        @article{
HJW10,
        author="Thomas A. Henzinger and Barbara Jobstmann and Verena Wolf",
        title="Formalisms for specifying {M}arkovian population models",
        journal="International Journal on Foundations of Computer Science",
        year="In press"
        }

        @article{
ChaHen10b,
        author="Krishnendu Chatterjee and Thomas A. Henzinger",
        title="A survey of stochastic omega-regular games",
        journal="Journal of Computer and System Sciences",
        year="In press"
        }

        @article{
MWDH10,
        author="Maria Mateescu and Verena Wolf and Fr\'ed\'eric Didier and Thomas A. Henzinger", 
        title="Fast adaptive uniformization of the chemical master equation",
        journal="IET Systems Biology",
        year="In press"
        }

        @article{
DHMW10,
        author="Fr\'ed\'eric Didier and Thomas A. Henzinger and Maria Mateescu and Verena Wolf", 
        title="Approximation of event probabilities in noisy cellular processes",
        journal="Theoretical Computer Science",
        year="In press"
        }

        @article{
CAH10,
        author="Krishnendu Chatterjee and Luca de Alfaro and Thomas A. Henzinger",
        title="Qualitative concurrent parity games",
        journal="ACM Transactions on Computational Logic",
        year="In press"
        }

        @article{
BCDD+10,
        author="Dietmar Berwanger and Krishnendu Chatterjee and Martin {De Wulf} and Laurent Doyen and Thomas A. Henzinger",
        title="Strategy construction for parity games with imperfect information",
        journal="Information and Computation",
        volume="208",
        year="2010",
        pages="1206-1220"
        }

        @article{
CHP10a,
        author="Krishnendu Chatterjee and Thomas A. Henzinger and Nir Piterman",
        title="Strategy logic",
        journal="Information and Computation",
        volume="208",
        year="2010",
        pages="677-693"
        }

	@inproceedings{
GHS10,
        author="Rachid Guerraoui and Thomas A. Henzinger and Vasu Singh",
        title="Model checking transactional memories",
        journal="Distributed Computing",
        volume="22",
        year="2010",
        pages="129-145"
        }

	@book{
ChaHen10,
	title="FORMATS: Formal Modeling and Analysis of Timed Systems",
        editor="Krishnendu Chatterjee and Thomas A. Henzinger",
	series="Lecture Notes in Computer Science",
	publisher="Springer",
        year="2010"
	}

        @inproceedings{
FHKP10,
        author="J\'er\^ome Feret and Thomas A. Henzinger and Heinz Koeppl and Tatjana Petrov",
        title="Lumpability abstractions of rule-based systems",  
        booktitle="MECBIC: Membrane Computing and Biologically Inspired Process Calculi",
        publisher="Electronic Proceedings in Theoretical Computer Science",
        year="2010",
        pages="137-156"
        }

        @incollection{
BHHK10,
        author="R\'egis Blanc and Thomas A. Henzinger and Thibaud B. Hottelier and Laura Kov\'acs",
        title="{{\sc Abc}}: {A}lgebraic bound computation for loops",
        booktitle="LPAR: Logic for Programming, Artificial Intelligence, and Reasoning", 
        series="Lecture Notes in Artificial Intelligence 6355",
        publisher="Springer", 
        year="2010",
        pages="103-118
        }

        @article{
FHH11,
        author="Jasmin Fisher and David Harel and Thomas A. Henzinger",
        title="Biology as reactivity",
        journal="Communications of the ACM",
        year="In press"
        }

        @inproceedings{
HSWZ11,
        author="Thomas A. Henzinger and Vasu Singh and Thomas Wies and Damien Zufferey",
        title="Scheduling large jobs by abstraction refinement",
        booktitle="EUROSYS",
        publisher="ACM", 
        year="2011"
        }


        @incollection{
CHH11,
        author="Krishnendu Chatterjee and Thomas A. Henzinger and Florian Horn",
        title="The complexity of request-response games",
        booktitle="LATA: Language and Automata Theory and Applications",
        series="Lecture Notes in Computer Science",
        publisher="Springer", 
        year="2011"
        }

        @incollection{
BCHK11,
        author="Udi Boker and Krishnendu Chatterjee and Thomas A. Henzinger and Orna Kupferman",
        title="Temporal specifications with accumulative values",
        booktitle="LICS: Logic in Computer Science",
        publisher="IEEE Computer Society",
        year="2011"
        }

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

	@phdthesis{
Ho95,
	author="Pei-Hsin Ho",
	title="Automatic Analysis of Hybrid Systems",
        school="Cornell University",
        year="1995"
	}

	@phdthesis{
Kop96,
	author="Peter W. Kopke",
	title="The Theory of Rectangular Hybrid Automata",
        school="Cornell University",
        year="1996"
	}

	@phdthesis{
Qad99,
	author="Shaz Qadeer",
	title="Algorithms and Methodology for Scalable Model Checking",
        school="University of California, Berkeley",
        year="1999"
	}

	@phdthesis{
Raj99,
	author="Sriram K. Rajamani",
	title="New Directions in Refinement Checking",
        school="University of California, Berkeley",
        year="1999"
	}

	@phdthesis{
Man02,
	author="Freddy Y.C. Mang",
	title="Games in Open Systems Verification and Synthesis",
        school="University of California, Berkeley",
        year="2002"
	}

	@phdthesis{
Maj03,
	author="Rupak Majumdar",
	title="Symbolic Algorithms for Verification and Control",
        school="University of California, Berkeley",
        year="2003"
	}

	@phdthesis{
Hor03,
	author="Benjamin Horowitz",
	title="{{\sc Giotto}}: {A} Time-triggered Language for Embedded Programming",
        school="University of California, Berkeley",
        year="2003"
	}

	@phdthesis{
Jha04,
	author="Ranjit Jhala",
	title="Program Verification by Lazy Abstraction",
        school="University of California, Berkeley",
        year="2004"
	}

	@phdthesis{
Chak07,
	author="Arindam Chakrabarti",
	title="A Framework for Compositional Design and Analysis of Systems",
        school="University of California, Berkeley",
        year="2007"
	}

	@phdthesis{
Chat07,
	author="Krishnendu Chatterjee",
	title="Stochastic Omega-Regular Games",
        school="University of California, Berkeley",
        year="2007"
	}

	@phdthesis{
Gho08,
	author="Arkadeb Ghosal",
	title="A Hierarchical Coordination Language for Reliable Real-Time Tasks",
        school="University of California, Berkeley",
        year="2008"
	}

	@phdthesis{
Mat08,
	author="Slobodan Matic",
	title="Compositionality in Deterministic Real-Time Embedded Systems",
        school="University of California, Berkeley",
        year="2008"
	}

	@phdthesis{
Pra08,
	author="Vinayak S. Prabhu",
	title="Games for the Verification of Timed Systems",
        school="University of California, Berkeley",
        year="2008"
	}

	@phdthesis{
Sin09,
        author="Vasu Singh",
        title="Formalizing and Verifying Transactional Memories",
        school="EPFL, Switzerland",
        year="2009"
        }

	@phdthesis{
The10,
        author="Gr\'egory Th\'eoduloz",
        title="Software Verification by Combining Program Analyses of Adjustable Precision",
        school="EPFL, Switzerland",
        year="2010"
        }