@inproceedings{
AluHen89,
        author="R. Alur and T.A. Henzinger",
	title="A really temporal logic",
	booktitle="Proceedings of the 30th Annual Symposium on 
        	Foundations of Computer	Science",
	publisher="IEEE Computer Society Press",
        year="1989",
	pages="164--169"
	}

	@inproceedings{
AluHen90,
        author="R. Alur and T.A. Henzinger",
	title="Real-time logics: {C}omplexity and expressiveness",
	booktitle="Proceedings of the Fifth Annual Symposium on 
        	Logic in Computer Science",
	publisher="IEEE Computer Society Press",
        year="1990",
	pages="390--401"
	}

	@inproceedings{
Hen90,
        author="T.A. Henzinger",
	title="Half-order modal logic: {H}ow to prove real-time properties",
	booktitle="Proceedings of the Ninth Annual Symposium on 
        	Principles of Distributed Computing",
	publisher="ACM Press",
        year="1990",
	pages="281--296"
	}

	@inproceedings{
HMP90,
        author="T.A. Henzinger and Z. Manna and A. Pnueli",
	title="An interleaving model for real time",
	booktitle="Proceedings of the Fifth Jerusalem Conference on
        	Information Technology",
	publisher="IEEE Computer Society Press",
        year="1990",
	pages="717--730"
	}

	@inproceedings{
HMP91,
        author="T.A. Henzinger and Z. Manna and A. Pnueli",
	title="Temporal proof methodologies for real-time systems",
	booktitle="Proceedings of the 18th Annual Symposium on
		Principles of Programming Languages",
	publisher="ACM Press",
        year="1991",
	pages="353--366"
	}

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

	@inproceedings{
AFH91,
        author="R. Alur and T. Feder and T.A. Henzinger",
	title="The benefits of relaxing punctuality",
	booktitle="Proceedings of the Tenth Annual Symposium on 
        	Principles of Distributed Computing",
	publisher="ACM Press",
        year="1991",
	pages="139--152"
	}

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

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

        @incollection{
AluHen92a,
        author="R. Alur and T.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="T.A. Henzinger and Z. Manna and A. 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="T.A. Henzinger and Z. Manna and A. 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="T.A. Henzinger and X. Nicollin and J. Sifakis and S. Yovine",
        title="Symbolic model checking for real-time systems",
        booktitle="Proceedings of the Seventh Annual Symposium on 
        	Logic in Computer Science",
        publisher="IEEE Computer Society Press",
        year="1992",
	pages="394--406"
        }

	@inproceedings{
AluHen92,
        author="R. Alur and T.A. Henzinger",
        title="Back to the future: {T}owards a theory of timed regular 
		languages",
	booktitle="Proceedings of the 33rd Annual Symposium on 
        	Foundations of Computer	Science",
	publisher="IEEE Computer Society Press",
        year="1992",
	pages="177--186"
	}

	@incollection{
ACHH93,
        author="R. Alur and C. Courcoubetis and T.A. Henzinger and P.-H. 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="T.A. Henzinger and Z. Manna and A. 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="R. Alur and T.A. Henzinger and M.Y. Vardi",
        title="Parametric real-time reasoning",
	booktitle="Proceedings of the 25th Annual Symposium on
		Theory of Computing",
	publisher="ACM Press",
        year="1993",
	pages="592--601"
	}

	@incollection{
ACH93,
        author="R. Alur and C. Courcoubetis and T.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="R. Alur and T.A. Henzinger and P.-H. Ho",
	title="Automatic symbolic verification of embedded systems",
	booktitle="Proceedings of the 14th Annual Real-Time Systems 
		Symposium",
	publisher="IEEE Computer Society Press",
        year="1993",
	pages="2--11"
	}

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

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

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

	@incollection{
ACHH+94,
        author="R. Alur and C. Courcoubetis and T.A. Henzinger and 
		P.-H. Ho and X. Nicollin and A. Olivero and 
		J. Sifakis and S. Yovine",
        title="The algorithmic analysis of hybrid systems",
	booktitle="ICAOS: International Conference on 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="R. Alur and L. Fix and T.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="R. Alur and T.A. Henzinger",
        title="Finitary fairness",
        booktitle="Proceedings of the Ninth Annual Symposium on 
        	Logic in Computer Science",
        publisher="IEEE Computer Society Press",
        year="1994",
	pages="52--61"
        }

	@incollection{
ACH94,
        author="R. Alur and C. Courcoubetis and T.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="T.A. Henzinger and P.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="A. Kapur and T.A. Henzinger and Z. Manna and A. 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="T.A. Henzinger and X. Nicollin and J. Sifakis and S. Yovine",
        title="Symbolic model checking for real-time systems",
	journal="Information and Computation",
        volume="111",
        year="1994",
        pages="193--244"
	}

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

	@article{
ACHH+95,
        author="R. Alur and C. Courcoubetis and N. Halbwachs and 
   		T.A. Henzinger and P.-H. Ho and X. Nicollin and 
		A. Olivero and J. Sifakis and S. Yovine",
        title="The algorithmic analysis of hybrid systems",
	journal="Theoretical Computer Science",
        volume="138",
        year="1995",
	pages="3--34"
	}

	@inproceedings{
HKPV95,
	author="T.A. Henzinger and P.W. Kopke and A. Puri and P. Varaiya",
 	title="What's decidable about hybrid automata?",
	booktitle="Proceedings of the 27th Annual Symposium on
		Theory of Computing",
	publisher="ACM Press",
        year="1995",
	pages="373--382"
	}

	@incollection{
HenHo95,
        author="T.A. Henzinger and P.-H. 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="R. Alur and T.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="T.A. Henzinger and P.W. Kopke and H. 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="T.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="T.A. Henzinger and P.-H. 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="T.A. Henzinger and P.-H. 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="T.A. Henzinger and P.-H. Ho and H. 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="M.R. Henzinger and T.A. Henzinger and P.W. Kopke",
	title="Computing simulations on finite and infinite graphs",
	booktitle="Proceedings of the 36th Annual Symposium on 
        	Foundations of Computer	Science",
	publisher="IEEE Computer Society Press",
        year="1995",
	pages="453--462"
	}

	@inproceedings{
HHW95,
	author="T.A. Henzinger and P.-H. Ho and H. Wong-Toi",
	title="{{\sc HyTech}}: {T}he next generation",
	booktitle="Proceedings of the 16th Annual Real-Time Systems 
		Symposium",
	publisher="IEEE Computer Society Press",
        year="1995",
	pages="56--65"
	}

	@incollection{
HenWon96a,
	author="T.A. Henzinger and H. 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="R. Alur and T. Feder and T.A. Henzinger",
	title="The benefits of relaxing punctuality",
	journal="Journal of the ACM",
        volume="43",
        year="1996",
        pages="116--146"
	}

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

	@inproceedings{
Hen96,
        author="T.A. Henzinger",
	title="The theory of hybrid automata",
	booktitle="Proceedings of the 11th Annual Symposium on 
        	Logic in Computer Science",
	publisher="IEEE Computer Society Press",
        year="1996",
	pages="278--292"
	}

	@inproceedings{
AluHen96,
        author="R. Alur and T.A. Henzinger",
	title="Reactive modules",
	booktitle="Proceedings of the 11th Annual Symposium on 
        	Logic in Computer Science",
	publisher="IEEE Computer Society Press",
        year="1996",
	pages="207--218"
	}

	@incollection{
HenKop96,
        author="T.A. Henzinger and P.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="T.A. Henzinger and O. Kupferman and M.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="T.A. Henzinger and H. 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="R. Alur and T.A. Henzinger and E.D. Sontag",
	series="Lecture Notes in Computer Science 1066",
	publisher="Springer",
        year="1996"
	}

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

	@article{
ACH97,
        author="R. Alur and C. Courcoubetis and T.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="R. Alur and T.A. Henzinger",
 	title="Real-time system = discrete system + clock variables",
	journal="Software Tools for Technology Transfer",
        year="1997",
	pages="86--109"
	}

	@incollection{
HenKup97,
	author="T.A. Henzinger and O. 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="V. Gupta and T.A. Henzinger and R. 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="T.A. Henzinger and P.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="T.A. Henzinger and O. Kupferman and S.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="R. Alur and T.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="R. Alur and R.K. Brayton and T.A. Henzinger and S. Qadeer and 
		S.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="T.A. Henzinger and P.-H. Ho and H. 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="T.A. Henzinger and P.-H. Ho and H. 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="R. Alur and T.A. Henzinger and O. Kupferman", 
        title="Alternating-time temporal logic",
    	booktitle="Proceedings of the 38th Annual Symposium on 
        	Foundations of Computer	Science",
	publisher="IEEE Computer Society Press",
        year="1997",
	pages="100--109"
	}

	@inproceedings{
AHW97,
	author="R. Alur and T.A. Henzinger and H. Wong-Toi",
        title="Symbolic analysis of hybrid systems",
        booktitle="Proceedings of the 36th Annual Conference on 
        	Decision and Control",
	publisher="IEEE Press",
        year="1997",
	pages="702--707"
	}

	@article{
HKPV98,
	author="T.A. Henzinger and P.W. Kopke and A. Puri and P. 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="R. Alur and T.A. Henzinger and S. 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="T.A. Henzinger and V. 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="T.A. Henzinger and S. Sastry",
	series="Lecture Notes in Computer Science 1386",
	publisher="Springer",
        year="1998"
	}

	@article{
HHW98,
        author="T.A. Henzinger and P.-H. Ho and H. 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="R. Alur and T.A. Henzinger and F.Y.C. Mang and S. Qadeer and 
		   S.K. Rajamani and S. 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="T.A. Henzinger and S. Qadeer and S.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="T.A. Henzinger and O. Kupferman and S. 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="T.A. Henzinger and J.-F. Raskin and P.-Y. 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="J.-F. Raskin and P.-Y. Schobbens and T.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="T.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="R. Alur and T.A. Henzinger and O. Kupferman and M.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. Preu{\ss}ig and S. Kowalewski and H. {Wong-Toi} and
		   T.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="T.A. Henzinger and S. Qadeer and S.K. Rajamani and 
		   S. 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="L. de Alfaro and T.A. Henzinger and O. Kupferman",
	title="Concurrent reachability games",
	booktitle="Proceedings of the 39th Annual Symposium on 
        	Foundations of Computer	Science",
	publisher="IEEE Computer Society Press",
        year="1998",
	pages="564--575"
	}

	@incollection{
HQR99,
	author="T.A. Henzinger and S. Qadeer and S.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="T.A. Henzinger and S. Qadeer and S.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="T.A. Henzinger and B. Horowitz and R. 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="R. Alur and L. de Alfaro and T.A. Henzinger and F.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="R. Alur and T.A. Henzinger and O. 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="R. Alur and T.A. Henzinger",
	title="Reactive modules",
	journal="Formal Methods in System Design",
	volume="15",
        year="1999",
	pages="7--48"
	}

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

	@inproceedings{
HLQR99,
        author="T.A. Henzinger and X. Liu and S. Qadeer and S.K. Rajamani",
	title="Formal specification and verification of a dataflow processor 
		array",
	booktitle="Proceedings of the International Conference on
                Computer-Aided Design",
	publisher="IEEE Computer Society Press",
        year="1999",
	pages="494--499"
	}

	@incollection{
HenMaj00,
	author="T.A. Henzinger and R. 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="T.A. Henzinger and B. Horowitz and R. Majumdar and H. 
		{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="T.A. Henzinger and J.-F. 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="T.A. Henzinger and R. 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="T.A. Henzinger and S.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="L. de Alfaro and T.A. Henzinger",
	title="Concurrent omega-regular games",
	booktitle="Proceedings of the 15th Annual Symposium on 
        	Logic in Computer Science",
	publisher="IEEE Computer Society Press",
        year="2000",
	pages="141--154"
	}

	@incollection{
HMMR00,
	author="T.A. Henzinger and R. Majumdar and F.Y.C. Mang and
		J.-F. 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="L. de Alfaro and T.A. Henzinger and F.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="T.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="L. de Alfaro and T.A. Henzinger and F.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="R. Alur and T.A. Henzinger and G. Lafferriere and 
		   G.J. Pappas",
	title="Discrete abstractions of hybrid systems",
	journal="Proceedings of the IEEE",
	volume="88",
        year="2000",
	pages="971--984"
	}	

	@inproceedings{
HQR00,
        author="T.A. Henzinger and S. Qadeer and S.K. Rajamani",
	title="Decomposing refinement proofs using assume-guarantee
                reasoning", 
	booktitle="Proceedings of the International Conference on
                Computer-Aided Design",
	publisher="IEEE Computer Society Press",
        year="2000",
	pages="245--252"
	}

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

	@article{
ABHQ+01,
        author="R. Alur and R.K. Brayton and T.A. Henzinger and S. Qadeer and 
		S.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="T.A. Henzinger and M. Minea and V.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="R. Alur and L. de Alfaro and R. Grosu and T.A. Henzinger and
 		M. Kang and C.M. Kirsch and R. Majumdar and F.Y.C. Mang and
		B.Y. Wang",
	title="{{\sc jMocha}}: {A} model-checking tool that exploits design 
		structure",
	booktitle="Proceedings of the 23rd Annual International Conference 
		on Software Engineering",
	publisher="IEEE Computer Society Press",
	year="2001",
	pages="835--836"
	}

	@inproceedings{
AHM01c,
     	author="L. de Alfaro and T.A. Henzinger and F.Y.C. Mang", 
	title="{{\sc McWeb}}: {A} model-checking tool for web-site debugging",
	booktitle="Poster Proceedings of the Tenth International Word-Wide 
		Web Conference",
	year="2001",
	pages="86--87"
	} 

	@inproceedings{
HHK01a,
	author="T.A. Henzinger and B. Horowitz and C.M. Kirsch",
	title="Embedded control systems development with {{\sc Giotto}}",
	booktitle="Proceedings of the International Conference on Languages, 
	        Compilers, and Tools for Embedded Systems",
	publisher="ACM Press",
	year="2001",
	pages="64--72"
	}

	@inproceedings{
AHM01,
        author="L. de Alfaro and T.A. Henzinger and R. Majumdar",
	title="From verification to control: {D}ynamic programs for
		omega-regular objectives",
	booktitle="Proceedings of the 16th Annual Symposium on 
        	Logic in Computer Science",
	publisher="IEEE Computer Society Press",
        year="2001",
	pages="279--290"
	}

	@incollection{
AHM01b,
	author="L. de Alfaro and T.A. Henzinger and R. 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="L. de Alfaro and T.A. Henzinger and F.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="L. de Alfaro and T.A. Henzinger and R. 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="L. de Alfaro and T.A. Henzinger",
	title="Interface automata",
	booktitle="Proceedings of the Ninth Annual Symposium on
     		Foundations of Software Engineering",
	publisher="ACM Press",
	year="2001",
	pages="109--120"
	}

	@incollection{
HHK01,
	author="T.A. Henzinger and B. Horowitz and C.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="L. de Alfaro and T.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="T.A. Henzinger and C.M. Kirsch",
	series="Lecture Notes in Computer Science 2211",
	publisher="Springer",
        year="2001"
	}

	@inproceedings{
BPPH+01,
	author="T. Brown and A. Pasetti and W. Pree and T.A. Henzinger and 
		C.M. Kirsch",
	title="A reusable and platform-independent framework for distributed 
		control systems",
	booktitle="Proceedings of the 20th Annual Digital Avionics 
		Systems Conference",
        volume="2",
	publisher="IEEE Press",
	year="2001",
	pages="1--11"
	}

	@inproceedings{
HPW01,
	author="T.A. Henzinger and J. Preu\ss ig and H. Wong-Toi",
	title="Some lessons from the {{\sc HyTech}} experience",
	booktitle="Proceedings of the 40th Annual Conference on 
                Decision and Control",
	publisher="IEEE Press",
	year="2001",
	pages="2887--2892"
	}

	@inproceedings{
HJMS02,
	author="T.A. Henzinger and R. Jhala and R. Majumdar and G. Sutre",
	title="Lazy abstraction",
	booktitle="Proceedings of the 29th Annual Symposium on 
	        Principles of Programming Languages",
	publisher="ACM Press",
	year="2002",
	pages="58--70"
	}

	@incollection{
CHR02,
	author="F. Cassez and T.A. Henzinger and J.-F. 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="T.A. Henzinger and C.M. Kirsch",
	title="The {E}mbedded {M}achine: 
                {P}redictable, portable real-time code",
	booktitle="Proceedings of the International Conference on 
                Programming Language Design and Implementation",
	publisher="ACM Press",
	year="2002",
	pages="315--326"
	}

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

	@article{
RSH02,
	author="J.-F. Raskin and P.-Y. Schobbens and T.A. Henzinger",
        title="Axioms for real-time logics",
	journal="Theoretical Computer Science",
	volume="274",
	year="2002",
	pages="151--182"
	}

	@article{
HQRT02,
        author="T.A. Henzinger and S. Qadeer and S.K. Rajamani and 
		   S. 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="R. Alur and T.A. Henzinger and O. Kupferman", 
        title="Alternating-time temporal logic",
        journal="Journal of the ACM",
        volume="49",
        year="2002",
	pages="672--713"
	}

	@inproceedings{
HLMK+02,
	author="B. Horowitz and J. Liebman and C. Ma and T.J. Koo and
		T.A. Henzinger and A. Sangiovanni-Vincentelli and S. Sastry",
	title="Embedded software design and system integration for rotorcraft
		{UAV} using platforms",
	booktitle="Proceedings of the 15th IFAC World Congress on Automatic 
		Control",
	publisher="Elsevier",
	year="2002"
	}

	@incollection{
HKKM02,
	author="T.A. Henzinger and S.C. Krishnan and O. Kupferman and 
		F.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="A. Chakrabarti and L. de Alfaro and T.A. Henzinger and 
		F.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="A. Chakrabarti and L. de Alfaro and T.A. Henzinger and 
		M. Jurdzi\'{n}ski and F.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="T.A. Henzinger and R. Jhala and R. Majumdar and G.C. Necula
		and G. Sutre and W. 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="M. Jurdzi\'{n}ski and O. Kupferman and T.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="T.A. Henzinger and C.M. Kirsch and R. Majumdar and 
		S. 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="L. de Alfaro and T.A. Henzinger and M. 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="C.M. Kirsch and M.A.A. Sanvido and T.A. Henzinger and W. 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="R. Passerone and L. de Alfaro and T.A. Henzinger and 
		A. Sangiovanni-Vincentelli",
	title="Convertibility verification and converter synthesis: 
		{T}wo faces of the same coin",
	booktitle="Proceedings of the International Conference on
                Computer-Aided Design",
	publisher="IEEE Computer Society Press",
        year="2002",
        pages="132--139"
	}

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

	@article{
HHK03,
	author="T.A. Henzinger and B. Horowitz and C.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="T.A. Henzinger and B. Horowitz and C.M. Kirsch",
	title="Embedded control systems development with {{\sc Giotto}}",
	booktitle="Software-Enabled Control: Information Technology for 
                Dynamical Systems",
        editor="T. Samad and G. Balas",
	publisher="IEEE Press and Wiley-Interscience",
	year="2003",
	pages="123--146"
	}

        @incollection{
HKM03a,
        author="T.A. Henzinger and O. Kupferman and R. 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="T.A. Henzinger and R. Jhala and R. Majumdar and G. 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="K. Chatterjee and D. Ma and R. Majumdar and T. Zhao and 
                T.A. Henzinger and J. 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="T.A. Henzinger and R. Jhala and R. 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="L. de Alfaro and T.A. Henzinger and R. 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="T.A. Henzinger and R. Jhala and R. Majumdar and S. 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="L. de Alfaro and M. Faella and T.A. Henzinger and 
                R. Majumdar and M. 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="K. Chatterjee and M. Jurdzi\'{n}ski and T.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="A. Chakrabarti and L. de Alfaro and T.A. Henzinger and 
                M. 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="T.A. Henzinger and C.M. Kirsch and S. 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="T.A. Henzinger and O. Kupferman and S. 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="T.A. Henzinger and R. Jhala and R. Majumdar and
                M.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="K. Chatterjee and M. Jurdzi\'{n}ski and T.A. Henzinger",
	title="Quantitative stochastic parity games",
	booktitle="Proceedings of the 
                15th Annual Symposium on Discrete Algorithms",
        publisher="ACM Press",
        year="2004",
        pages="114--123"
        }

	@inproceedings{
HJMM04,
	author="T.A. Henzinger and R. Jhala and R. Majumdar and K.L. McMillan",
	title="Abstractions from proofs",
	booktitle="Proceedings of the 31st Annual Symposium on 
	        Principles of Programming Languages",
	publisher="ACM Press",
	year="2004",
        pages="232--244"
	}

        @incollection{
AFHM+04,
        author="L. de Alfaro and M. Faella and T.A. Henzinger and R. Majumdar 
                and M. 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="A. Ghosal and T.A. Henzinger and C.M. Kirsch and 
                M.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="D. Beyer and A. Chlipala and T.A. Henzinger and R. Jhala and 
                R. Majumdar",
        title="Generating tests from counterexamples",
        booktitle="Proceedings of the 26th Annual International Conference 
                on Software Engineering",
        publisher="IEEE Computer Society Press",
        year="2004",
        pages="326--335"
        }

        @inproceedings{
BHJM04,
        author="D. Beyer and T.A. Henzinger and R. Jhala and R. Majumdar",
        title="An {E}clipse plug-in for model checking",
        booktitle="Proceedings of the 26th Annual International Workshop
                on Program Comprehension",
        publisher="IEEE Computer Society Press",
        year="2004",
        pages="251--257"
        }

	@inproceedings{
HJM04,
	author="T.A. Henzinger and R. Jhala and R. Majumdar",
	title="Race checking by context inference",
	booktitle="Proceedings of the International Conference on 
                Programming Language Design and Implementation",
	publisher="ACM Press",
	year="2004",
        pages="1--13"
	}

	@incollection{
CHJH04,
	author="K. Chatterjee and T.A. Henzinger and M. Jurdzi\'{n}ski",
	title="Games with secure equilibria",
	booktitle="Proceedings of the 19th Annual Symposium on 
        	Logic in Computer Science",
	publisher="IEEE Computer Society Press",
        year="2004",
        pages="160--169"
        }

	@incollection{
BCHJ+04a,
        author="D. Beyer and A. Chlipala and T.A. Henzinger and R. Jhala and 
                R. 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="T.A. Henzinger and C.M. Kirsch",
        title="A typed assembly language for real-time programs",
	booktitle="Proceedings of the Fourth Annual Conference on 
                 Embedded Software",
	publisher="ACM Press", 
        year="2004",
        pages="104--113"
        }

        @inproceedings{
CAH04,
        author="K. Chatterjee and L. de Alfaro and T.A. Henzinger",
        title="Trading memory for randomness",
        booktitle="Proceedings of the First Annual Conference on 
                 Quantitative Evaluation of Systems",
        publisher="IEEE Computer Society Press",
        year="2004",
        pages="206--217"
        }

	@article{
CMMZ+04,
	author="K. Chatterjee and D. Ma and R. Majumdar and T. Zhao and 
                T.A. Henzinger and J. Palsberg",
	title="Stack size analysis for interrupt-driven programs",
	journal="Information and Computation",
	volume="194",
	year="2004",
	pages="144--174"
	}

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

	@article{
HMR05,
	author="T.A. Henzinger and R. Majumdar and J.-F. Raskin",
	title="A classification of symbolic transition systems", 
	journal="ACM Transactions on Computational Logic",
	volume="6",
	year="2005",
	pages="1--32"
	}

        @inproceedings{
ChaHen05,
        author="K. Chatterjee and T.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="L. de Alfaro and T.A. Henzinger",
        title="Interface-based design",
        booktitle="Engineering Theories of Software-intensive Systems",
        editor="M. Broy and J. Gr{\"u}nbauer and D. 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="D. Beyer and T.A. Henzinger and R. Jhala and R. 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="S. Matic and T.A. Henzinger",
        title="Trading end-to-end latency for composability",
        booktitle="Proceedings of the 26th Annual Real-Time Systems Symposium",
        publisher="IEEE Computer Society Press",
        year="2005",
        pages="99--110"
        }

        @incollection{
DHR05,
        author="L. Doyen and T.A. Henzinger and J.-F. 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="T.A. Henzinger and R. Majumdar and V.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="A. Chakrabarti and K. Chatterjee and T.A. Henzinger and
                 O. Kupferman and R. 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="T.A. Henzinger and R. Jhala and R. Majumdar",
        title="Permissive interfaces",
        booktitle="Proceedings of the 13th Annual Symposium on 
                 Foundations of Software Engineering",
        publisher="ACM Press",
        year="2005",
        pages="31--40"
        }

        @inproceedings{
CHJM05,
        author="K. Chatterjee and T.A. Henzinger and R. Jhala and R. Majumdar",
        title="Counterexample-guided planning",
        booktitle="Proceedings of the 21st International Conference on 
                 Uncertainty in Artificial Intelligence",
        publisher="AUAI Press",
        year="2005",
        pages="104--111"
        }

        @inproceedings{
CAH05,
        author="K. Chatterjee and L. de Alfaro and T.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="K. Chatterjee and T.A. Henzinger and M. Jurdzi\'{n}ski",
        title="Mean-payoff parity games",
        booktitle="Proceedings of the 20th Annual Symposium on 
                 Logic in Computer Science",
        publisher="IEEE Computer Society Press",
        year="2005",
        pages="178--187"
        }

        @inproceedings{
HKM05,
        author="T.A. Henzinger and C.M. Kirsch and S. Matic",
        title="Composable code generation for distributed {{\sc Giotto}}",
        booktitle="Proceedings of the International Conference on 
                 Languages, Compilers, and Tools for Embedded Systems",
        publisher="ACM Press",
        year="2005",
        pages="21--30"
        }

        @inproceedings{
KSH05,
        author="C.M. Kirsch and M.A.A. Sanvido and T.A. Henzinger", 
        title="A programmable microkernel for real-time systems",
        booktitle="Proceedings of the First International Conference on 
                 Virtual Execution Environments",
        publisher="ACM Press",
        year="2005",
        pages="35--45"
        }
 
        @inproceedings{
BCH05,
        author="D. Beyer and A. Chakrabarti and T.A. Henzinger", 
        title="Web service interfaces",
        booktitle="Proceedings of the 14th International 
                 World-Wide Web Conference",
        year="2005",
        pages="148--159"
        }

        @inproceedings{
CAH06,
        author="K. Chatterjee and L. de Alfaro and T.A. Henzinger",
        title="The complexity of quantitative concurrent parity games",
        booktitle="Proceedings of the 17th Annual Symposium on 
                 Discrete Algorithms",
        publisher="ACM Press", 
        year="2006",
        pages="678--687"
        }

        @inproceedings{
ChaHen06,
        author="K. Chatterjee and T.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="T.A. Henzinger and S. Matic",
        title="An interface algebra for real-time components",
        booktitle="Proceedings of the 12th Annual Real-Time and Embedded 
                 Technology and Applications Symposium",
        publisher="IEEE Computer Society Press",
        year="2006",
        pages="253--266"
        }

        @inproceedings{
ChaHen06a,
        author="K. Chatterjee and T.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="K. Chatterjee and R. Majumdar and T.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="T.A. Henzinger and O. Kupferman and R. 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="M. De Wulf and L. Doyen and T.A. Henzinger and 
                 J.-F. 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="D. Beyer and T.A. Henzinger and G. Th{\'e}oduloz",
        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="K. Chatterjee and T.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="T.A. Henzinger and J. 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="K. Chatterjee and L. de Alfaro and T.A. Henzinger",
        title="Strategy improvement for concurrent reachability games",
        booktitle="Proceedings of the Third Annual Conference on 
                 Quantitative Evaluation of Systems",
        publisher="IEEE Computer Society Press",
        year="2006",
        pages="291--300"
        }


        @inproceedings{
CAFH+06,
        author="K. Chatterjee and L. de Alfaro and M. Faella and 
                 T.A. Henzinger and R. Majumdar and M. Stoelinga",
        title="Compositional quantitative reasoning",
        booktitle="Proceedings of the Third Annual Conference on 
                 Quantitative Evaluation of Systems",
        publisher="IEEE Computer Society Press",
        year="2006",
        pages="179--188"
        }

	@incollection{
HenPit06,
	author="T.A. Henzinger and N. 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="L. Doyen and K. Chatterjee and T.A. Henzinger and 
                 J.-F. 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="T.A. Henzinger and V.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="J. Fisher and T.A. Henzinger",
        title="Executable biology",
        booktitle="Proceedings of the Winter Simulation Conference",
        publisher="IEEE Computer Society Press",
        year="2006",
        pages="1675--1682"
        }

        @inproceedings{
GHIK+06,
        author="A. Ghosal and T.A. Henzinger and D. Iercan and 
                 C.M. Kirsch and A. Sangiovanni-Vincentelli",
        title="A hierarchical coordination language for interacting 
                 real-time tasks",
	booktitle="Proceedings of the Sixth Annual Conference on 
                 Embedded Software",
	publisher="ACM Press", 
        year="2006",
        pages="131--141"
        }

	@inproceedings{
GHKN+06,
	author="B. Gulavani and T.A. Henzinger and Y. Kannan and A. Nori 
                 and S.K. Rajamani",
	title="{{\sc Synergy}}: {A} new algorithm for property checking",
	booktitle="Proceedings of the 14th Annual Symposium on
     		Foundations of Software Engineering",
	publisher="ACM Press",
	year="2006",
        pages="117--127"
	}

        @article{
CHJ06,
        author="K. Chatterjee and T.A. Henzinger and M. Jurdzi\'{n}ski",
        title="Games with secure equilibria",
        journal="Theoretical Computer Science",
        volume="365",
        year="2006",
        pages="67--82"
        }

        @incollection{
Hen07a,
        author="T.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{
CHP07b,
        author="K. Chatterjee and T.A. Henzinger and N. 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="D. Beyer and A. Chakrabarti and T.A. Henzinger and 
               S.A. Seshia",
        title="An application of web-service interfaces",
        booktitle="Proceedings of the International Conference on Web 
               Services",
        publisher="IEEE Computer Society Press", 
        year="2007",
        pages="831--838"
        }

        @incollection{
BHPR07,
        author="T. Brihaye and T.A. Henzinger and V.S. Prabhu and 
               J.-F. 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="D. Beyer and T.A. Henzinger and G. Th{\'e}oduloz",
        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{
Hen07b,
        author="T.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="D. Beyer and T.A. Henzinger and V. 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{
BHMR07b,
        author="D. Beyer and T.A. Henzinger and R. Majumdar and 
               A. Rybalchenko",
        title="Path invariants",
        booktitle="Proceedings of the International Conference on 
               Programming Language Design and Implementation",
        publisher="ACM Press", 
        year="2007",
        pages="300--309"
        }

        @incollection{
ChaHen07,
        author="K. Chatterjee and T.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="K. Chatterjee and T.A. Henzinger and N. 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="R. Manevich and J. Field and T.A. Henzinger and
               G. Ramalingam and M. 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="D. Beyer and T.A. Henzinger and R. Majumdar and 
               A. 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="J. Fisher and N. Piterman and A. Hajnal and T.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="M.A. Schaub and T.A. Henzinger and J 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="J. Duparc and T.A. Henzinger",
	series="Lecture Notes in Computer Science 4646",
	publisher="Springer",
        year="2007"
	}

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

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

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

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

        @article{
CDHR07, 
        author="K. Chatterjee and L. Doyen and T.A. Henzinger and 
                J.-F. Raskin",
        title="Algorithms for omega-regular games with imperfect 
                information",
        journal="Logical Methods in Computer Science",
        volume="3",
        number="3",
        year="2007"
        }

        @article{
AHK07, 
        author="L. de Alfaro and T.A. Henzinger and O. Kupferman",
        title="Concurrent reachability games",
        journal="Theoretical Computer Science",
        volume="386",
        year="2007",
        pages="188--217"
        }
 
        @article{
DHR08, 
        author="L. Doyen and T.A. Henzinger and J.-F. 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="K. Chatterjee and T.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{
CMH08,
        author="K. Chatterjee and R. Majumdar and T.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="L. Doyen and T.A. Henzinger and B. Jobstmann and T. Petrov",
        title="Interface theories with component reuse",
	booktitle="Proceedings of the Eighth Annual Conference on 
                 Embedded Software",
	publisher="ACM Press", 
        year="2008",
        pages="79--88"
        }

	@incollection{
CDH08,
	author="K. Chatterjee and L. Doyen and T.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="D. Berwanger and K. Chatterjee and L. Doyen and 
                T.A. Henzinger and S. 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="K. Chatterjee and T.A. Henzinger and B. 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="R. Guerraoui and T.A. Henzinger and V. 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="J. Fisher and T.A. Henzinger and M. Mateescu and 
                N. Piterman",
        title="Bounded asynchrony: {C}oncurrency for modeling 
                cell-cell interactions",
        booktitle="FMSB: Formal Methods in Systems Biology",
        series="Lecture Notes in Computer Science 5054",
        publisher="Springer", 
        year="2008",
        pages="17--32"
        }

	@inproceedings{
GHJS08,
        author="R. Guerraoui and T.A. Henzinger and B. Jobstmann and 
                V. Singh",
        title="Model checking transactional memories",
        booktitle="Proceedings of the International Conference on 
               Programming Language Design and Implementation",
        publisher="ACM Press", 
        year="2008",
        pages="372--382"
        }

	@inproceedings{
GHMR+08,
	author="A. Gupta and T.A. Henzinger and R. Majumdar and 
                A. Rybalchenko",
	title="Proving non-termination",
	booktitle="Proceedings of the 35th Annual Symposium on 
	        Principles of Programming Languages",
	publisher="ACM Press",
	year="2008",
        pages="147--158"
	}

	@inproceedings{
BHT08,
	author="D. Beyer and T.A. Henzinger and G. Theoduloz",
	title="Program analysis with dynamic change of precision",
	booktitle="Proceedings of the 23rd International Conference on 
	        Automated Software Engineering",
	publisher="ACM Press",
	year="2008",
        pages="29--38"
	}

	@inproceedings{
CGHI+08,
	author="K. Chatterjee and A. Ghosal and T.A. Henzinger and 
                D. Iercan and C.M. Kirsch and C. Pinello and 
                A. Sangiovanni-Vincentelli",
	title="Logical reliability of interacting real-time tasks",
	booktitle="Proceedings of the International Conference on 
	        Design, Automation, and Test in Europe",
        publisher="IEEE Press",
	year="2008",
        pages="909--914"
	}

        @incollection{
CHP08,
        author="K. Chatterjee and T.A. Henzinger and V.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="K. Chatterjee and R. Majumdar and T.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="K. Chatterjee and K. Sen and T.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="K. Chatterjee and T.A. Henzinger and V.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{
GHS08b,
        author="R. Guerraoui and T.A. Henzinger and V. 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{
ChaHen08b,
	author="K. Chatterjee and T.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="T.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="T.A. Henzinger and T. Hottelier and L. Kov{\'a}cs",
        title="{{\sc Valigator}}: {A} verification tool with bound and 
                 invariant generation",
        booktitle="LPAR: Logic for Programming, Artificial Intelligence, 
                 and Reasoning",
        series="Lecture Notes in Computer Science 5330",
        publisher="Springer", 
        year="2008",
        pages="333--342"
        }

	@incollection{
CAH09,
	author="K. Chatterjee and L. de Alfaro and T.A. Henzinger",
	title="Termination criteria for solving concurrent safety and 
                reachability games", 
	booktitle="Proceedings of the 
                20th Annual Symposium on Discrete Algorithms",
        publisher="ACM Press",
        year="2009",
        pages="197--206"
        }

        @incollection{
GHS09,
        author="R. Guerraoui and T.A. Henzinger and V. 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="T.A. Henzinger and M. Mateescu and V. Wolf",
        title="Sliding-window abstraction for infinite Markov chains",
        booktitle="CAV: Computer-Aided Verification",
        series="Lecture Notes in Computer Science 5643",
        publisher="Springer", 
        year="2009",
        pages="337--352"
        }

        @incollection{
BCHJ09,
        author="R. Bloem and K. Chatterjee and T.A. Henzinger and 
                B. 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="D. Berwanger and K. Chatterjee and M. De Wulf and L. Doyen
                and T.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{
CDH09,
        author="K. Chatterjee and L. Doyen and T.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"
        }

	@article{
ChaHen09,
	author="K. Chatterjee and T.A. Henzinger",
 	title="A survey of stochastic omega-regular games",
	journal="Journal of Computer and System Sciences",
        year="{T}o appear"
	}

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

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

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

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

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

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

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

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

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

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

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

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

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