SNo.	Author(s)	Title
1	M. Abadi and L. Lamport	An Old-Fashioned Recipe for Real Time
2	T. Henzinger and Z. Manna and A. Pnueli	Towards Refining Temporal Specifications into Hybrid Systems
3	T. Henzinger and Z. Manna and A. Pnueli	Temporal Proof Methodologies for Real-Time Systems
4	Z. Manna and A. Pnueli	Models for Reactivity
5	R. Alur and C. Courcoubetis and T. Henzinger and P. Ho	Hybrid automata: An Algorithmic Approach to the
6	T. Henzinger and X. Nicollin and J. Sifakis and S. Yovine	Symbolic Model Checking for Real-Time Systems
7	T. Henzinger and X. Nicollin and J. Sifakis and S. Yovine	Symbolic Model Checking for Real-Time Systems
8	X. Nicollin and A. Olivero and J. Sifakis and S. Yovine	An Approach to the Description and Analysis of
9	O. Lichtenstein and A. Pnueli and L. Zuck	The Glory of the Past
10	T.A. Henzinger	Sooner Is Safer Than Later
11	Z. Manna and A. Pnueli	Time for Concurrency
12	O. Maler and Z. Manna and A. Pnueli	From Timed to Hybrid Systems
13	R. Alur and T.A. Henzinger	Real-time Logics: Complexity and Expressiveness
14	Y. Kesten and A. Pnueli	Timed and Hybrid Statecharts and their Textual
15	E. Harel and O. Lichtenstein and A. Pnueli	Explicit Clock Temporal Logic
16	E. Chang and Z. Manna and A. Pnueli	The Safety-Progress Classification
17	R. Alur and T.A. Henzinger	Logics and models of real time: a survey
18	T. Henzinger and Z. Manna and A. Pnueli	Timed Transition Systems
19	T. Henzinger and Z. Manna and A. Pnueli	What Good are Digital Clocks?
20	Eric Nassor and Guy Vidal-Naquet	Suitability of the Propositional Temporal Logic to
21	W. Ackermann	Solvable Cases of the Decision Problem
22	C.-J. Seger	A Bounded Delay Race Model
23	E.A. Emerson and A.K. Mok and A.P. Sistla	Quantitative Temporal Reasoning
24	E.A. Emerson and A.K. Mok and A.P. Sistla	Quantitative Temporal Reasoning
25	A. Pnueli	How Vital is Liveness?
26	Burch J.R. and McMillan K.L. and Clarke E.M. and	Sequential Circuit Verification Using Symbolic Model
27	Z. Chaochen and C.A.R Hoare and A.P. Ravn	A Calculus of Durations
28	M. Abadi and L. Lamport	The Existence of Refinement Mappings
29	M. Abadi and L. Lamport	The Existence of Refinement Mappings
30	M. Abadi and Z. Manna	Nonclausal Temporal Deduction
31	R. Alur and T.A. Henzinger	A Really Temporal Logic
32	Il Moon and Powers G.J. and Burch J.R. and Clarke E.M.	Automatic Verification of Sequential Control Systems Using
33	E.A. Emerson	Temporal and Modal Logic
34	van Emde Boas P.	Machine Models ans Simulation
35	D.S. Johnson	A Catalog of Complexity Classes
36	E. Chang	Compositional Verification of Reactive and Real-Time Systems
37	E. Chang and Z. Manna and A. Pnueli	Compositional Verification of Real-Time Systems
38	W. Thomas	Automata on Infinite Objects
39	N.H. Margolus	Physics and Computation
40	O. Maler	Hybrid Systems and Real-World Computations
41	van Glabbeek R.J.	The Linear Time -- Branching Time Spectrum
42	van Glabbeek R.J.	A Complete Axiomatization for Branching Bisimulation
43	J.C.M. Baeten and J.A. Bergstra	Discrete Time Process Algebra
44	J.U. Skakkebaek and A.P. Ravn and H. Rischel and Z. Chaochen	Specification of Embedded Real-Time Systems
45	K.M. Hansen and A.P. Ravn and H. Rischel	Specifying and Verifying Requirements of Real-Time
46	K.M. Hansen and A.P. Ravn and H. Rischel	Specifying and Verifying Requirements of Real-Time
47	R. Gerth and R. Kuiper and J. Segers	Interface Refinement in Reactive Systems
48	J. Gunawardena	Periodic Behaviour in Times Systems with AND OR
49	R. Milner	Operational and Algebraic Semantics of Concurrent Processes
50	H. Sipma	CS 352 Notes
51	de Nicola R. and M.C.B. Hennessy	Testing Equivalence for Processes
52	Harper R. and Honsell F. and Plotkin G.	A Framework for Defining Logics
53	C.A. Gunter and D.S. Scott	Semantic Domains
54	J.C. Mitchell	Type Systems for Programming Languages
55	M.J. Fischer and R.E. Ladner	Propositional Dynamic Logic of Regular Programs
56	H. Barringer and R. Kuiper and A. Pnueli	A Really Abstract Concurrent Model and its Temporal
57	A. Pnueli and L. Zuck	In and Out of Temporal Logic
58	N. Lynch	Simulation Techniques for Proving Properties of
59	L. Lamport	The Temporal Logic of Actions
60	L. Lamport	Hybrid Systems in TLA+
61	L. Lamport	The Temporal Logic of Actions
62	A. Benveniste	Data-flow Synchronous Languages
63	J. Zwiers	Partial Order Based Design of Concurrent Systems
64	E.M. Clarke	Verification Tools for Finite-State Concurrent Systems
65	J.A. Brzozowski and Seger C.-J	A Characterization of Ternary Simulation of Gate Networks
66	Seger C.-J and J.A. Brzozowski	An Optimistic Ternary Simulation of Gate Races
67	Morin L. and Li H.F.	Design of Synchronisers: a Review
68	Kleeman L. and Cantoni A.	Metastable Behavior in Digital Systems
69	Nootbaar K. and Spehn R.W. and Tyler E.	Minimizing the Effect of Metastability in BiCMOS
70	R. Alur and T.A. Henzinger and M.Y. Vardi	Parametric real-time reasoning
71	M.R. Hansen and Z. Chaochen and J. Staunstrup	A Real-Time Duration Semantics for Circuits
72	K.M. Chandy	Reasoning about Continuous Systems
73	Z. Chaochen and A.P. Ravn and M.R. Hansen	An Extended Duration Calculus for Hybrid Real-Time Systems
74	Z. Liu and A.P. Ravn and E.V. S\orensen and Z. Chaochen	Towards a Calculus of System Dependability
75	T.A. Henzinger	The Temporal Specification and Verification of Real-time
76	X. Nicollin and J. Sifakis and S. Yovine	Compiling Real-Time Specifications into Extended Automata
77	X. Nicollin and J. Sifakis and S. Yovine	From ATP to Timed Graphs and Hybrid Systems
78	X. Nicollin and J. Sifakis	The Algebra of Timed Processes ATP: Theory and Application
79	X. Nicollin and J. Sifakis	An Overview and Synthesis on Timed Process Algebras
80	X. Nicollin and A. Olivero and J. Sifakis and S. Yovine	An Approach to the Description and Analysis of
81	A.P. Ravn and H. Rischel	Requirements Capture for Embeded Real-Time Systems
82	K.R. Apt and De Roever W.P.	A Proof System for Communicating Sequential Processes
83	W. Ackermann	Solvable Cases of the Decision Problem
84	Z. Ying	Modeling and Reasoning about Robotic Systems and Behaviors:
85	W. Thomas	Logical Specifications of Infinite Computations
86	Y. Kesten and A. Pnueli	TLR: Having Your Next and Eating it Too
87	A. Pnueli	System Specification and Refinement in Temporal Logic
88	T. Rokicki	Representing and Modeling Circuits
89	T. Rokicki	Geometric Approaches to State Space Evaluation of
90	D. Harel	Statecharts: A Visual Formalism for Complex Systems
91	McGuire H. and Z. Manna and R. Waldinger	A Deductive System for Temporal Logic
92	Jayadev Misra	Powerlist: A Structure for Parallel Recursion
93	R.H. Thomason	Modal Logic and Metaphysics
94	R.H. Thomason	Some Completeness Results for Modal Predicate Calculi
95	J. Hintikka	Existential Presuppositions and Uniqueness Presuppositions
96	J. Rushby	Critical System Properties: Survey and Taxonomy
97	P.M. Melliar-Smith	Extending Interval Logic to Real-Time Systems
98	R.L.Schwartz and P.M. Melliar-Smith and F.H. Vogt	An Interval Logic for Higher-Level Temporal Reasoning
99	J.R. Burch	Trace Algebra for Automatic Verification of Real-Time
100	D.E. Long	Model Checking Abstraction and Compositional Verification
101	Z. Manna and R. Waldinger	Fundamentals of Deductive Program Synthesis
102	Z. Manna and P. Wolper	Synthesis of Communicating Processes from Temporal
103	R. Alur	Techniques for Automatic Verification of Real-time Systems
104	Mart\'\in Abadi and Leslie Lamport	Decomposing Specifications of Concurrent Systems
105	M. Abadi and L. Lamport	Conjoining Specifications
106	D. Gallin	Intensional and Higher-Order Modal Logic
107	Z. Manna and P. Wolper	Synthesis of Communicating Processes from Temporal
108	P.L. Wolper	Synthesis of Communicating Processes from Temporal
109	J.W. Garson
110	M. Abadi	Temporal-Logic Theorem Proving
111	E. Bencivenga	Intuitionistic Logic
112	Van Dalen D.
113	T. Henzinger and Z. Manna and A. Pnueli	Temporal Proof Methodologies for Timed Transition Systems
114	T. Henzinger and Z. Manna and A. Pnueli	An Interleaving Model for Real Time
115	L. Lamport	What Good is Temporal Logic?
116	Z. Manna and A. Pnueli	The Temporal Logic of Reactive and Concurrent
117	Z. Manna and A. Pnueli	Temporal Verification of Reactive Systems: Safety
118	R. Koymans	Specifying Real-Time Properties With Metric Temporal Logic
119	R. Hojati and V. Singhal and R.K. Brayton	Edge-Streett/Edge-Rabin Automata Environment for Formal
120	R. Hojati and R.K. Brayton	An Environment for Formal Verification Based On
121	R. Hojati and R.K. Brayton and R.P. Kurshan	BDD-Based Debugging Of Designs Using Language Containment
122	Berkeley CAD group in Verification	Revisiting Blif-MV An Intermediate format For Verification and
123	A. Aziz and F. Balarin and R.K. Brayton and S.-T. Cheng	HSIS: A BDD-Based Environment for Formal Verification
124	The Berkeley Verifiers	PIF: a Property Interchange Format for Verification Using
125	A.U. Shankar	An Introduction to Assertional Reasoning for
126	L. Lamport	Verification and Specification of Concurrent Programs
127	N. Dershowitz and Y.-J. Lee	Logical Debugging
128	Y.-K. Tsay and R.L. Bagrodia	Deducing Fairness Properties for UNITY Programs:
129	L.C. Paulson	Isabelle: The Next 700 Theorem Provers
130	N. Dershowitz and U.S. Reddy	Deductive and Inductive Synthesis of Equational Programs
131	Z. Manna and A. Pnueli	Temporal Verification Diagrams
132	R. Harper	Introduction to Standard ML
133	Z. Manna and M. Paltrinieri and R. Waldinger	Deductive Synthesis of Concurrent Construction Plans
134	Z. Manna and M. Paltrinieri and R. Waldinger	Deductive Synthesis of Concurrent Construction Plans
135	Z. Manna and M. Paltrinieri and R. Waldinger	Temporal Planning
136	Z. Manna and R. Waldinger	The Deductive Synthesis of Imperative sc LISP Programs
137	Z. Manna and R. Waldinger	How to Clear a Block: a Theory of Plans
138	B. Jonsson and Z. Manna and R. Waldinger	Towards Deductive Syntehsis of Data-flow Networks
139	Z. Manna and R.J. Waldinger	A Deductive Approach to Program Synthesis
140	R.W. Floyd	Assigning Meanings to Programs
141	Y. Kesten and Z. Manna and H. McGuire and A. Pnueli	A Decision Algorithm for Full Propositional Temporal Logic
142	M. Blum and R.W. Floyd and V. Pratt and R.L. Rivest	Time Bounds for Selection
143	R.W. Floyd	An Algorithm for Coding Efficient Arithmetic Operations
144	R.W. Floyd	The Paradigms of Programming
145	Z. Manna and R. Waldinger	Deductive Synthesis of the Unification Algorithm
146	Z. Manna and A. Pnueli	Verifying Hybrid Systems
147	N.J. Cutland	Computability: an Introduction to Recursive Function Theory
148	R. Goldblatt	Logics of Time and Computation
149	H.R. Lewis and C.H. Papadimitriou	Elements of the Theory of Computation
150	H. Rogers	Theory of Recursive Functions and Effective Computability
151	F. Kr\oger	On the Interpretability of Arithmetic in Temporal Logic
152	A. Szalas and L. Holenderski	Incompleteness of First-Order Temporal Logic with Until
153	A. Szalas	Concerning the semantic Consequence Relation in
154	A. Szalas	A Complete Axiomatic Characterization of First-Order
155	A. Szalas	Arithmetical Axiomatization of First-Order
156	A. Szalas	On Strictly Arithmetical Completeness in Logics of
157	D.M. Gabbay and I.M. Hodkinson	An Axiomatization of the Temporal Logic with Until
158	R. Alur and T. Feder and T.A. Henzinger	The Benefits of Relaxing Punctuality
159	D.M. Gabbay and V.B. Shehtman	Undecidability of Modal and Intermediate
160	B. Moszkowski	Some Very Compositional Temporal Properties
161	H.B. Enderton	A Mathematical Introduction to Logic
162	M. Fitting	Proof Methods for Modal and Intuitionistic Logic
163	M. Abadi and Z. Manna	Nonclausal Deduction in First-Order Temporal Logic
164	Z. Manna and R. Waldinger	Problematic Features of Programming Languages:
165	Y. Auffray and P. Enjalbert	Modal Theorem Proving: An Equational Viewpoint
166	D. Perrin	Finite Automata
167	G.E. Hughes and M.J. Cresswell	An Introduction to Modal Logic
168	R. Goldblatt	Mathematics of Modality
169	G.S. Boolos and R.C. Jeffrey	Computability and Logic
170	S.C. Kleene	Introduction to Metamathematics
171	B.F. Chellas	Modal Logic: an Introduction
172	Aida Pliu\vskevi\vcien\.e	Gentzen-Type Calculi for Modal Logic S4 with Barcan
173	Regimantas Pliu\vskevi\vcius	Logical Foundation for Logic Programming Based on
174	P. Jackson and H. Reichgelt	A General Proof Method for Modal Predicate Logic
175	N.S. Bj\orner	On Formally Undecidable Propositions of Duration
176	C. Stirling	Modal and Temporal Logics
177	M. Ben-Ari
178	F. Kroeger	Temporal Logic of Programs
179	Z. Manna and A. Pnueli	Verification of Concurrent Programs:
180	G. Corsi	Quantified Modal Logic: An Introduction
181	A. Pnueli	The Temporal Logic of Programs
182	M.R. Hansen and Z. Chaochen	Semantics and Completeness of Duration Calculus
183	J.P. Burgess	Correspondence Theory
184	van Benthem J.
185	J.P. Burgess	Axioms for Tense Logic I. ``Since'' and ``Until''
186	J.P. Burgess	Axioms for Tense Logic II. Time periods
187	G. Lolli	Introduzione alla logica formale
188	K.R. Apt and E.-R. Olderog	Verification of Sequential and Concurrent Programs
189	G. Mints	A Short Introduction to Modal Logic
190	S. Kripke	Basic Modal Logic
191	R.A. Bull and K. Segerberg
192	J.A.W. Kamp	Tense Logic and the Theory of Order
193	A.U. Shankar	Reasoning Assertionally about Real-Time Systems
194	Y. Kesten and Z. Manna and A. Pnueli	Temporal Verification of Simulation and Refinement
195	Z. Manna and A. Pnueli	An Exercise in the Verification of Multi-Process
196	Z. Manna and A. Pnueli	Tools and Rules for the Practicing Verifier
197	M. Nagayama C. Talcott	An NQTHM Mechanization of An Exercise in the
198	M. fisher	A Normal Form for First-Order Temporal Formulae
199	M.U. S\orensen and O.E. Hansen and H.H.	Combining Temporal Specification Techniques
200	S. Owre and N. Shankar and J.M. Rushby	The PVS Specification Language (Beta Release)
201	S. Owre and N. Shankar and J.M. Rushby	User Guide for the PVS Specification and
202	S. Owre and N. Shankar and J.M. Rushby	The PVS Proof Checker: A Reference Manual (Beta Release)
203	S. Owre and N. Shankar and J.M. Rushby	A Tutorial on Specification and Verification Using
204	M. Abadi and L. Lamport and P. Wolper	Realizable and Unrealizable Concurrent Program
205	J.R. Burch and D.L. Dill	Automatic Verification of Pipelined Microprocessor Control
206	van Benthem J. and J. Bergstra	Logic of Transition Systems
207	van Benthem J. and van Eijck J. and Steblestova V.	Modal Logic Transition Systems and Processes
208	K.J. J\ullig
209	R. Koymans	Specifying Message Passing and Time-Critical Systems
210	D. Harel	Semantic Automata
211	van Benthem J.
212	N.S. Bj\orner	Minimal Typing Derivations
213	S. Feferman	Weyl Vindicated: Das Kontinuum 70 Years Later
214	S. Feferman	The Development of Programs for the Foundations of
215	K.L. McMillan	Symbolic Model Checking
216	E.M. Clarke and Grumberg O. and Hiraishi H. and
217	D. Sharp and P. Harrison and J. Darlington	Synthesis of a Message-Passing Algorithm for
218	L. Ness	L.0: A Truly Concurrent Executable Temporal Logic
219	J. Cantrell	Futurebus+ Cache Coherence
220	V. Pratt	Action Logic and Pure Induction
221	D.L. Dill	Trace Theory for Automatic Hierarchical Verification
222	A.J. Martin	The Design of a Self-Timed Circuit for Distributed
223	E.P. Gribomont and D. Rossetto	CAVEAT: Technique and Tool for Computer Aided
224	M.R. Hansen and P.K. Pandya and Z. Chaochen	Finite Divergence
225	W. Zhang	Verification of XYZ/SE Programs
226	W. Zhang	Implementation of XYZ/VERI II
227	W. Zhang	Verification of XYZ/SE Programs
228	S.T. Cheng	Synthesizing FSMs from Verilog Programs
229	S.T Cheng and R.K. Brayton	Compiling Verilog into Automata
230	S. Buva\vc and V. Buva\vc and I.A. Mason	Metamathematics of Contexts
231	Z. Manna and A. Anuchitanukul and N. Bj\orner and	STeP: The Stanford Temporal Prover
232	N. Shankar	A Lazy Approach to Compositional Verification
233	L. Lamport and S. Merz	Specifying and Verifying FAult-Tolerant Systems
234	M. Fujita and S. Kono	Synthesis of Controllers from Interval Temporal Logic
235	S. Kono	Automatic Verification of Interval Temporal Logic
236	S. Kono	A Combination of Clausal and Non Clausal Temporal
237	A. Nowatzyk	Formal Verification in a Multiprocessor Design
238	S.M. German	Verifying the Absence of Common Runtime Errors in
239	S.M. German	Automating Proofs of the Absence of Common Runtime Errors
240	S.. GErman and B. Wegbreit	A Synthesizer of Inductie Assertions
241	B.A. Trakhtenbrot	Compositional Proofs for Networks of Processes
242	D. Craigen and S. Gerhart and T. Ralston	An International Survey of Industrial Application of
243	D.L. Dill and E.M. Clarke	Automatic Verification of Asynchronous Circuits Using
244	D.E. Thomas and P. Moorby	The Verilog Hardware Description Language
245	R. de Nicola A. Fantechi S. Gnesi and G.Ristori	An Action-Based Framework for Verifying Logical and
246	C.N. Ip and D.L. Dill	Better Verification through Symmetry
247	K.A. Bartlett and R.A. Scantlebury and P.T. Wilson	A Note on Reliable Full-Duplex Transmission over
248	van Benthem J.	Beyond Accessibility
249	P. Abdulla and B. Jonsson	Verifying Programs with Unreliable Channels
250	I. Walukiewicz	On Completeness of the $mu$-Calculus
251	A. Bouajjani and R. Echahed and J. Sifakis	On Model Checking for Real-Time Properties with Durations
252	B.K. Szymanski and J.M. Vidal	Automatic Verification of a Class of Symmetric
253	D.D. Gajski and L. Ramachandran and P. Fung and	Towards Achieving an 100-Hour Design Cycle: A Test Case
254	D.D. Gajski and F. Vahid and S. Narajan	SpecCharts: A VHDL Front-End for Embedded Systems
255	C.L. Heitmeyer and R.D. Jeffords and B.G. Labaw	Comparing Different Approaches for Specifying and
256	R.D. Jeffords	Optimal Bounds for the Old Utility Property for the
257	T.A. Henzinger and P.W. Kopke	Verification Methods for the Divergent Runs of
258	De Nicola R. and A. Fantechi and S. Gnesi and G. Ristori	An Action-Based Framework for Verifying Logical and
259	A. Fantechi and S. Gnesi and G. Ristori	Compositionality and Bisimulation: A Negative
260	R. Alur and C. Courcoubetis	Model-Checking in Dense Real-Time
261	A. Anuchitanukul and Z. Manna	Diferential BDDs
262	W. Ji and Y. Xinyao and Z. Chaochen	Refinement of Digital Dynamic Systems
263	Y. Xinyao and W. Ji and Z. Chaochen and P.K. Pandya	Formal Design of Hybrid Systems
264	Z. Yuhua and Z. Chaochen	A Formal Proof of the Deadline Driven Scheduler
265	Y. Huiqun and P.K. Pandya and S. Yongqiang	A Calculus for Hybrid Sampled Data Systems
266	R. Alur and T.A. Henzinger	Real-Time Systems Discrete Systems + Clock Variables
267	Norris Ip C. and D.L. Dill	Efficient Verification of Symmetric Concurrent Systems
268	D. Katiyar and D. Luckham and J. Mitchell	A Type System for Prototyping Languages
269	H. Garavel and J. Sifakis	Compilation and Verification of LOTOS Programs
270	A. Fantechi and S. Gnesi and G. Ristori	Compositional Logical Semantics and Lotos
271	S. Safra	On the Complexity of $omega$-Automata
272	S. Safra and M.Y. Vardi	On $omega$-Automata and Temporal Logic
273	J.A. Bergstra and J.W. Klop	An Introduction to Process Algebra
274	R.S. Streett	Propositional Dynamic Logic of Looping and Converse
275	M.O. Rabin	Automata on Infinite Objects and Church's Problem
276	de Alfaro L. and Z. Manna	Verification in Continuous Time by Discrete Reasoning
277	de Alfaro L. and Z. Manna	Compositional Verification of Reactive and Real-Time Systems
278	E. Chang
279	D.L. Dill and A.J. Hu and W. Wong-Toi	Checking for Language Inclusion Using Simulation Preorder
280	S.S. Lam and A.U. Shankar	Protocol Verification via Projections
281	N.A. Lynch and M.R. Tuttle	Hierarchical Correctness Proofs for Distributed Algorithms
282	A. Pnueli
283	J.H. Gallier	Logic for Computer Science
284	E.A. Emerson and C.L. Lei	Modalities for Model Checking: Branching Time Strikes Back
285	O. Lichtenstein and A. Pnueli	Checking That Finite State Concurrent Programs
286	E.A. Emerson and A.P. Sistla	Deciding Branching Time Logic
287	M.Y. Vardi and P. Wolper	Automata Theoretic Techniques for Modal Logics of Programs
288	M.Y. Vardi and P. Wolper	Automata Theoretic Techniques for
289	R. Alur and C. Courcoubetis and D.L. Dill	Model-Checking for Real-Time Systems
290	E.M. Clarke and E.A. Emerson	Design and Synthesis of Synchronization Skeletons Using
291	M. Ben-Ari and A. Pnueli and Z. Manna	The Temporal Logic of Branching Time
292	E.A. Emerson and J.Y. Halpern	``Sometimes'' and ``Not Never'' Revisited:
293	O. Maler and A. Pnueli	Tight Bounds on the Complexity of Cascaded
294	E.M. Clarke and E.A. Emerson and A.P. Sistla	Automatic Verification of Finite State Concurrent
295	I.A. Browne and Z. Manna and H.B. Sipma	Generalized Verification Diagrams
296	P. Blackburn and de Rijke M.	Zooming In Zooming Out
297	de Rijke M.	A Lindstrom Theorem for Modal Logic
298	P. Blackburn and de Rijke M. and Y. Venema	The Algebra of Modal Logic
299	de Rijke M.	The Logic of Pierce Algebras
300	P. Blackburn and de Rijke M.	Why Combine Logics?
301	de Rijke M.	Modal Model Theory
302	de Rijke M.	Extending Modal Logic
303	D. Dam and O. Grumberg and R. Gerth	Abstract Interpretation of Reactive Systems:
304	S. Katz and Z. Manna	Logical Analysis of Programs
305	S. Campos and E. Clarke and W. Marrero and M. Minea	Computing Quantitative Charateristics of Finite-State
306	E.W. Dijkstra and C.S. Scholten	Predicate Calculus and Program Semantics
307	A. Nowatzyk	Formal Verification in a Multiprocessor Design
308	N. Halbwachs	Synchronous Programming of Reactive Systems
309	J.C. Kunz and Y. Jin and R.E. Levitt and S.-D. Lin	The Intelligent Real-Time Maintenance Management
310	J. Rushby	Formal Specification and Verification for
311	J. Staunstrup and N. Mellergaard	Synchronized Transitions
312	Y. Kesten and A. Pnueli	A Complete Proof System for QPTL*
313	M.Y. Vardi and P. Wolper	Automata-Theoretic Techniques for
314	E.M. Clarke and M.C. Browne and E.A. Emerson and	Using Temporal Logic for Automatic Verification of
315	E.M. Clarke and I.A. Draghicescu and R.P. Kurshan	A unified approach for showing language inclusion
316	M.Y. Vardi	Nontraditional Applications of Automata Theory
317	G. Bhat and R. Cleaveland and O. Grumberg	Efficient On-the-Fly Model Checking for CTL*
318	M.Y. Vardi	On the Complexity of Modular Model Checking
319	O. Kupferman and A. Pnueli	Once and For All
320	O. Grumberg and D.E. Long	Model Checking and Modular Verification
321	A.R. Cavalli and Farina del Cerro L.	A Decision Method for Linear Temporal Logic
322	A. Pnueli	In transition for Global to Modular Temporal
323	Gerth R.	Foundations of Compositional Program Refinement-Safety
324	Kurshan R.P.	Analysis of discrete event coordination
325	R. Alur and D. Dill	The Theory of Timed Automata
326	L. Fix and O. Grumberg	Verification of Temporal Properties
327	O. Maler and A. Pnueli	On the Cascaded Decomposition of Automata
328	H.B. Sipma and T.E. Uribe and Z. Manna	Deductive Model Checking
329	M. Carpentier and A.E. Hadri and G. Padiou	A UNITY-Based Algorithm Design Assistant
330	X. Nicollin and J. Sifakis and S. Yovine	Compiling Real-Time Specifications into Extended
331	X. Nicollin and J. Sifakis and S. Yovine	From ATP to Timed Graphs and Hybrid Systems
332	X. Nicollin and J. Sifakis	The Algebra of Timed Processes ATP: Theory and
333	X. Nicollin and J. Sifakis	An Overview and Synthesis on Timed Process Algebras
334	X. Nicollin and A. Olivero and J. Sifakis and S. Yovine	An Approach to the Description and Analysis of Hybrid
335	N. Bj\orner and A. Browne and E. Chang	STeP: The Stanford Temporal Prover (Educational
336	O. Kupferman	Model Checking for Branching-Time Temporal Logics
337	Aho and Hopcroft and Ullman	Data Structures and Algorithms
338	S. Sastry and G. Meyer and C. Tomlin and	Hybrid Control in Air Traffic Management Systems
339	Intel	Formal Verification of a Sequential Multiplier via
340	C. Heitmeyer and N. Lynch	The Generalized Railroad Crossing: A Case Study in
341	C.L. Heitmeyer and R.D. Jeffords and B.G. Labaw	Comparing Different Approaches for Specifying and
342	F. Andersen and K.D. Petersen and J.S. Pettersson	A Graphical Tool for Proving UNITY Progress
343	T.A. Henzinger and P.W. Kopke and A. Puri and P. Varaiya	What's Decidable about Hybrid Automata
344	A. Anuchitanukul and Z. Manna	Differential BDDs
345	C.-F. Yu and V.D. Gligor	A Formal Specification and Verification Method for
346	J. McLean	A General Theory of Composition for a Class of
347	G. Lowe	SPLICE/AS: A Case Study in Using CSP to Detect
348	T.Y.C. Woo and S.S. Lam	Verifying Authentication Protocols: Methodology and
349	T.Y.C. Woo and S.S. Lam	A Semantic Model for Authentication Protocols
350	M. Burrows and M. Abadi and R. Needham	A Logic of Authentication
351	N. Heintze and J.D. Tygar	A Model for Secure Protocols and Their Compositions
352	D. Bolignano	An Approach to the Formal Verification of
353	G.J. Holzmann and O. Kupferman	Not checking for Closure under Stuttering
354	O. Kupferman and M.Y. Vardi	Module Checking
355	O. Kupferman and M.Y. Vardi	Module Checking Revisited
356	O. Kupferman and M.Y. Vardi	Modular model checking
357	O. Kupferman and M.Y. Vardi	Robust satisfaction
358	O. Kupferman and M.Y. Vardi	Verification of Fair Transition Systems
359	O. Kupferman and S. Safra and M.Y. Vardi	Relating Word and Tree Automata
360	J.F. Groote and F. Vaandrager	An Efficient Algorithm for Branching Bisimulation and
361	J.F. Groote and F. Vaandrager	An Efficient Algorithm for Branching Bisimulation and
362	R. Alur and D. Dill	Automata For Modeling Real-Time Systems
363	A. Kapur and T.A. Henzinger and Z. Manna and A. Pnueli	Proving Safety Properties of Hybrid Systems
364	E.A. Emerson and J. Srinivasan	Branching Time Temporal Logic
365	M. Koutny	Axiom System Induced by CTL* Logic
366	C. Stirling	Comparing Linear and Branching Time Temporal Logics
367	E.M. Clarke and I.A. Draghicescu	Expressibility Results for Linear-Time and Branching-Time
368	R. Gotzhein	Specifying Communication Services with Temporal
369	E.A. Emerson	Real-Time and the Mu-Calculus
370	M. Dam	CTL* and ECTL* as Fragments of the Modal
371	Z. Manna and A. Pnueli	Clocked Transition Systems
372	Y. Kesten and Z. Manna and A. Pnueli	Verifying Clocked Transition Systems
373	O. Maler and A. Pnueli and J. Sifakis	On the Synthesis of Discrete Controllers for Timed
374	de Alfaro L.	Logica Temporale e Sistemi in Tempo Reale
375	J.E. Hopcroft	An $n log n$ Algorithm for Minimizing States in a
376	de Alfaro L. and Z. Manna	Temporal Verification by Diagram Transformations
377	de Alfaro L. and Manna Z.	Temporal Verification by Diagram Transformations
378	R. Alur and C. Courcoubebetis and	The Algorithmic Analysis of Hybrid Systems
379	L. Lamport	TLA in pictures
380	W. Tomas	Languages Automata and Logic
381	G. Gawlick and R. Segala and J.	Liveness in Timed and Untimed Systems
382	R. Segala and G. Gawlick and	Liveness in Timed and Untimed Systems
383	D. Lehmann and A. Pnueli and J. Stavi	Impartiality Justice and Fairness: the Ethics of
384	N.A. Lynch and H. Attiya	Using Mappings to Prove Timing Properties
385	Barbara D. and Garcia-Molina H.	The Demarcation Protocol: a Technique for Maintaining Linear
386	D. Cohen-Or and E. Rich and U. Lerner and V. Shenkar	A Real-Time Photo-Realistic Visual Flythrough
387	D. Lesens and N. Halbwachs and P. Raymond	Automatic Verification of Parametrized
388	S. Safra	Exponential Determinization for $omega$-Automata
389	D. Lehmann and A. Pnueli and J. Stavi	Impartiality Justice and Fairness:
390	de Alfaro L. and A. Kapur and Z. Manna	Hybrid Diagrams: A Deductive-Algorithmic Approach
391	de Alfaro L. and A.R. Meo	Codes for Second and Third Order GH-ARQ Schemes
392	de Alfaro L.	Determination of Automorphic Codes
393	A. Browne and de Alfaro L. and Manna Z. and	Diagram-Based Formalisms for the Verification of
394	Z. Manna and N. Bj\orner and	STeP: The Stanford Temporal Prover
395	de Alfaro L. and Manna Z. and H.B. Sipma and	Visual Verification of Reactive Systems
396	Prat Bastai A. and de Alfaro L.	Molecole ed Energia
397	de Alfaro L.	Modem per Canali ad Alto Tasso di Errore:
398	de Alfaro L.	Logica Temporale e Sistemi in Tempo Reale
399	N.S. Bj\orner and U. Lerner and Z. Manna	Deductive Verification of Parameterized
400	J.R. Burch and E.M. Clarke and K.L. McMillan and	Symbolic model checking: $10^20$ states and beyond
401	E.M. Clarke and O. Grumberg and D.E. Long	Model Checking and Abstraction
402	E.M. Clarke and O. Grumberg and D.E. Long	Model Checking and Abstraction
403	E.M. Clarke and O. Gr\umberg	Avoiding the State Explosion Problem in
404	R. Milner	A Calculus of Communicating Systems
405	R. Milner	Calculi for Synchrony and Asynchrony
406	R. Milner	An algebraic definition of simulation between programs
407	E. Clarke and O. Grumberg and D. Long	Model Checking
408	E.M. Clarke and J.R. Burch and D.E. Long and	Automatic Verification of Sequential Circuit Design
409	Francez N.	Fairness
410	K.R. Apt and N. Francez and Katz S.	Appraising Fairness in Languages for Distributed Programming
411	J.P. Queille and J. Sifakis	Fairness and Related Properties in Transition Systems
412	E. Clarke and M. Fujita and X. Zhao	Multi-Terminal Binary Decision Diagrams and Hybrid
413	R. McNaughton	Testing and Generating Infinite Sequences by a Finite
414	D. Scott and C. Strachey	Towards a Mathematical Semantics for Computer Languages
415	R. Alur and C. Courcoubetis and D. Dill	Model-Checking for Real-Time Systems
416	D.E. Muller P.E. Schupp	Simulating Alternating Tree Automata by
417	J.A. Bergstra and J.W. Klop	Process Algebra for Synchronous Communication
418	L. Lamport	Proving the Correctness of Multiprocessor Programs
419	R. Alur and D.L. Dill	A Theory of Timed Automata
420	N. Bj\orner and A. Browne and Z. Manna	Automatic Generation of Invariants and Intermediate
421	M.Y. Vardi and P. Wolper	An Automata-Theoretic Approach to Automatic Program
422	de Alfaro L. and A. Kapur and Z. Manna	Hybrid Diagrams: A Deductive-Algorithmic Approach
423	A. Bouajjani and R. Robbana	Verifying $omega$-Regular Properties for a Subclass
424	A. Bouajjani and Y. Lakhnech	Logics vs. Automata: The Hybrid Case
425	A. Bouajjani and Y. Lakhnech and R. Robbana	From Duration Calculus to Hybrid Automata
426	W. Thomas	On the Synthesis of Strategies in Infinite Games
427	T.A. Henzinger and S. Qadeer and S.K. Rajamani and	An Assume-Guarantee Rule for Checking Simulation
428	K.L. McMillan	A Compositional Rule for Hardware Design Refinement
429	R. Alur and T.A. Henzinger	Reactive Modules
430	L. Lamport	Specifying Concurrent Program Modules
431	E.W. Stark	A Proof Technique for Rely/Guarantee Properties
432	E.M. Clarke and D.E. Long and K.L. McMillan	Compositional Model Checking
433	R. Alur and T.A. Henzinger and F.Y.C. Mang and	Mocha: Modularity in Model Checking
434	H.R. Andersen	Partial Model Checking
435	R. Alur and T.A. Henzinger and O. Kupferman	Alternating-time temporal logic
436	R.P. Kurshan	Computer-aided Verification of Coordinating Processes:
437	G.J. Holzman	Design and Validation of Computer Protocols
438	R. Brayton and G. Hachtel and	VIS: A system for Verification and Synthesis
439	S. Graf and H. Sa\\i di	Verifying Invariants Using Theorem Proving
440	S. Graf and H. Sa\\i di	Construction of Abstract State Graphs With PVS
441	D. Dams	Abstract Interpretation and Partition Refinement for
442	P. Cousot and R. Cousot	Abstract Interpretation: A Unified Lattice Model for
443	R. Alur and T.A. Henzinger and O. Kupferman	Alternating-time temporal logic
444	M.R. Garey and D.S. Johnson	Computers and Intractability: A Guide to the
445	E. Asarin and O. Maler and A. Pnueli and J. Sifakis	Controller Synthesis for Timed Automata
446	E. Asarin and O. Maler and A. Pnueli	Symbolic Controller Synthesis for Discrete and Timed
447	R. Alur and T.A. Henzinger and O. Kupferman and M.Y. Vardi	Alternating Refinement Relations
448	R. Alur and de Alfaro L. and T.A. Henzinger and	Automating Modular Verification
449	T.A. Henzinger and O. Kupferman and S.K. Rajamani	Fair simulation
450	T.A. Henzinger and S. Qadeer and S.K. Rajamani and	An assume-guarantee rule for checking simulation
451	R. Alur and T.A. Henzinger	Modularity for timed and hybrid systems
452	J.P. Queille and J. Sifakis	Specification and Verification of Concurrent Systems
453	N.A. Lynch	Distributed Algorithms
454	C.A.R. Hoare	Communicating Sequential Processes
455	C.A.R. Hoare	Communicating Sequential Processes
456	A. Pnueli and R. Rosner	On the synthesis of a reactive module
457	P.J.G. Ramadge and W.M. Wonham	The Control of Discrete Event Systems
458	E.A. Emerson and C.S. Jutla	Tree Automata Mu-Calculus and Determinacy
459	Y. Gurevich and L. Harrington	Trees Automata and Games
460	T.A. Henzinger	It's about time: real-time logics reviewed
461	R.E. Bryant	Graph-Based Algorithms for Boolean Function
462	K.M. Chandy and J. Misra	Parallel Program Design: A Foundation
463	T.A. Henzinger and X. Liu and S. Qadeer and S.K. Rajamani	Formal specification and verification of a dataflow processor
464	R. McNaughton	Infinite Games Played on Finite Graphs
465	N. Klarlund
466	A.W. Mostowski	Regular Expressions for Infinite Trees and a
467	S. Krishnan and A. Puri and R. Brayton and P. Varaiya	Rabin Index Chain Automata and
468	H. Lescow and T. Wilke	On Polynomial-Size Programs Winning Finite-State Games
469	J.R. B\uchi and L.H. Landweber	Solving Sequential Conditions by Finite-State Strategies
470	N. Buhrke and H. Lescow and J. V\oge	Strategy Construction in Infinite Games
471	D.L. Dill	Trace Theory for Automatic Hierarchical Verification of
472	F. Balarin and M. Chiodo and P. Giusto and H. Hsieh and	Hardware-Software Co-Design of Embedded Systems:
473	Biere A. and Cimatti A. and Clarke E. and Zhu Y.	Symbolic Model Checking Without BDDs
474	A. Biere and A. Cimatti and E. M. Clarke and	Symbolic Model Checking using SAT procedures instead
475	T.A. Henzinger and S. Qadeer and S.K. Rajamani	You assume we guarantee: methodology and case studies
476	T.A. Henzinger and O. Kupferman and S. Qadeer	From em pre/historic to em post/modern symbolic model
477	M. Tiemann	The CORBA Reference Guide : Understanding the Common
478	A. Pope	CORBA Fundamentals and Programming
479	J. Siegel
480	R. Barden and S. Stepney and D. Cooper	Z in Practice
481	M. Imperato	An Introduction to Z
482	A. Diller	Z: An Introduction to Formal Methods
483	J.C. Mitchell	Foundations for Programming Languages
484	B. Meyer	Object-Oriented Software Construction
485	P. Chan	The Java Class Libraries
486	F. Kuhns and C. O'Ryan and D.C. Schmidt and	The Design and Performance of a Pluggable Protocols
487	C.D. Gill and D.L. Levine and D.C. Schmid	The Design and Performance of a Real-Time CORBA
488	Z. Manna et al.	STeP: Deductive-Algorithmic Verification of
489	D. Clarke and I. Lee and H. Xie	VERSA: A Tool for the Specification and Analysis of
490	QNX Software Systems Ltd.
491	F. Balarin and M. Chiodo and P. Giusto and H. Hsieh	Hardware-Software Co-Design of Embedded Systems: The
492	R. Alur and T.A. Henzinger	Real-time logics: complexity and expressiveness
493	T.A. Henzinger and X. Nicollin and J. Sifakis and S. Yovine	Symbolic model checking for real-time systems
494	J.L. Peterson and A. Silberschatz	Operating System Concepts
495	A. Blass and Y. Gurevich	Henkin Quantifiers and Complete Problems
496	L. Henkin	Some Remarks on Infinitely Long Formulas
497	W. Walkoe	Finite Partially-Ordered Quantification
498	D. Lehman and S. Shelah	Reasoning with Time and Chance
499	R. Alur and C. Courcoubetis and D. Dill	Verifying Automata Specifications of Probabilistic
500	Oxford University Timed CSP Group	Timed CSP: Theory and Practice
501	R. Gotzhein	Specifying Communication Services with Temporal
502	E.M. Clarke and I.A. Draghicescu	Expressibility Results for Linear-Time and Branching-Time
503	C. Stirling	Comparing Linear and Branching Time Temporal Logics
504	S. Hart and M. Sharir and A. Pnueli	Termination of Probabilistic Concurrent Programs
505	D. Kozen	Semantic of Probabilistic Programs
506	A. Pnueli	On the Extremely Fair Treatment of Probabilistic
507	D. Kozen	Results on the propositional $mu$-calculus
508	D. Kozen	A Probabilistic PDL
509	Y.A. Feldman	A Decidable Propositional Probabilistic Dynamic Logic
510	Y.A. Feldman and D. Harel	A Probabilistic Dynamic Logic
511	J.H. Reif	Logic for Probabilistic Programming
512	R. Fagin and J.Y. Halpern and N. Megiddo	A Logic for Reasoning about Probabilities
513	A. Pnueli and L.D. Zuck	Probabilistic Verification
514	J.C.M. Baeten and J.A. Bergstra and S.A. Smolka	Axiomatizing Probabilistic Processes:
515	K.G. Larsen and A. Skou	Compositional Verification of Probabilistic Processes
516	L. Christoff and I. Christoff	Efficient Algorithms for Verification of
517	M.O. Rabin	Probabilistic Automata
518	K.G. Larsen and A. Skou	Bisimulation Through Probabilistic Testing
519	B. Jonsson and K.G. Larsen	Specification and Refinement of Probabilistic Processes
520	C. Courcoubetis and M. Yannakakis	Verifying Temporal Properties of Finite-State
521	M.Y. Vardi	Automatic Verification of Probabilistic Concurrent
522	van Glabbeek R. and Smolka S.A. and	Reactive Generative and Stratified Models of Probabilistic
523	van Glabbeek R. and Smolka S.A. and	Reactive Generative and Stratified Models of Probabilistic
524	D. Freedman	Markov Chains
525	R. Alur and C. Courcoubetis and M. Yannakakis	Distinguishing Tests for Nondeterministic and
526	Clarke E.M. and Emerson E.A.	Synthesis of Synchronization Skeletons for Branching
527	R. Fagin and J.Y. Halpern	Reasoning about Knowledge and Probability
528	M. Abadi and J.Y. Halpern	Decidability and Expressiveness for First-Order
529	S. Hart and M. Sharir	Probabilistic Temporal Logic for Finite and Bounded
530	Hart S. and Sharir M.	Probabilistic Propositional Temporal Logics
531	A. Pnueli and L. Zuck	Probabilistic Verification by Tableaux
532	E.A. Emerson and J.Y. Halpern	Sometimes and Not Never Revisited: On
533	R. Alur and C. Courcoubetis and D.L. Dill	Model-Checking for Probabilistic Real-Time Systems
534	S. Hart and M. Sharir and A. Pnueli	Verification of Probabilistic Programs
535	S. Krauss and D. Lehmann	Decision Procedures for Time and Chance
536	J.G. Kemeny and J.L. Snell and A.W. Knapp	Denumerable Markov Chains
537	H. Hansson and B. Jonsson	A Framework for Reasoning about Time and Reliability
538	H. Hansson and B. Jonsson	A Logic for Reasoning about Time and Probability
539	H. Hansson	Time and Probability in Formal Design of
540	H. Hansson
541	A. Aziz and V. Singhal and F. Balarin and	It Usually Works: The Temporal Logic of Stochastic Systems
542	A. Schrijver	Theory of Linear and Integer Programming
543	A. Bianco and de Alfaro L.	Model Checking of Probabilistic and Nondeterministic
544	J.R. Rao	Reasoning about Probabilistic Parallel Programs
545	N.J. Nilsson	Probabilistic Logic
546	C. Courcoubetis and M. Yannakakis	The Complexity of Probabilistic Verification
547	C. Courcoubetis and M. Yannakakis	Markov Decision Processes and Regular Events
548	B. Jonsson and C. Ho-Stuart and Y. Wang	Testing and Refinement for Nondeterministic and
549	R. Segala and N.A. Lynch	Probabilistic Simulations for Probabilistic Processes
550	R. Segala and N.A. Lynch	Probabilistic Simulations for Probabilistic Processes
551	C. Derman	Finite State Markovian Decision Processes
552	M.L. Puterman	Markov Decision Processes
553	R. Segala	Modeling and Verification of Randomized Distributed
554	R. Gorrieri and F. Corradini and M. Roccetti	Performance Preorder: Ordering Processes with
555	C. Baier and M. Kwiatkowska	Model Checking for a Probabilistic Branching time
556	C. Baier and M. Kwiatkowska	Model Checking for a Probabilistic Branching time
557	de Alfaro L.	Formal Verification of Performance and Reliability of
558	D. Beauquier and A. Slissenko	Polytime Model Checking for Timed Probabilistic
559	D. Beauquier and D. Burago and A. Slissenko	On the Complexity of Finite Memory Strategies for
560	R. Segala	A Compositional Trace-Based Semantics for
561	N. Lynch and I. Saias and R. Segala	Proving Time Bounds for Randomized Distributed
562	A. Pogosyants and R. Segala	Formal Verification of Timed Properties of Randomized
563	M.L. Littman and T.L. Dean and Pack Kaelbling L.	On the Complexity of Solving Markov Decision Problems
564	K.W. Ross and R. Varadarajan	A Sample Path Theory for Time-Average Markov Decision
565	C.H. Papadimitriou and J.N. Tsitsiklis	The Complexity of Markov Decision Processes
566	R. Baldick	A Unified Approach to Polynomially Solvable Cases of
567	Melekopoglou M. and Condon A.	On the Complexity of the Policy Improvement Algorithm
568	D.P. Bertsekas and J.N. Tsitsiklis	An Analysis of Stochastic Shortest Path Problems
569	D. Burago and de Rougemont M. and A. Slissenko	On the Complexity of Partially Observed Markov
570	de Alfaro L.	Temporal Logics for the Specification of Performance
571	E.V. Denardo	Computing a Bias-Optimal Policy in a Discrete-Time
572	D.P. Bertsekas	Dynamic Programming
573	D.P. Bertsekas	Dynamic Programming and Optimal Control
574	D. Williams	Probability With Martingales
575	G. Ciardo and R. German and C. Lindermann	A Characterization of the Stochastic Process
576	G. Franceschinis and R.R. Muntz	Computing Bounds for the Performance Indices of
577	J. Campos and J.M. Colom and H. Jungnitz and M. Silva	Approximate Throughput Computation of Stochastic
578	R.J. Boucherie	A Characterization of Independence for Competing
579	M.A. Holliday and M.K. Vernon	A Generalized Petri Net Model for Performance Analysis
580	H. Howard	Dynamic Programming and Markov Processes
581	D. Blackwell	Discrete Dynamic Programming
582	E.V. Denardo and B. Fox	Multichain Markov Renewal Programs
583	S. Karlin and H.M. Taylor	A First Course in Stochastic Processes
584	R.E. Bellman	Dynamic Programming
585	R.E. Bellman	The Theory of Dynamic Programming
586	R.E. Bellman	Applied Dynamic Programming
587	S. Karlin	The Structure of Dynamic Programming Models
588	R. Howard	Dynamic Probabilistic Systems
589	R. Howard	Dynamic Probabilistic Systems: Semi-Markov and
590	L.E. Dubins and L.J. Savage	How to Gamble if You Must: Inequalities for
591	D. Blackwell RIFARECONTROLLARE	Discounted Dynamic Programming
592	D. Lehmann and M. Rabin	On the Advantage of Free Choice: a Symmetrical and
593	A. Hordijk and L.C.M. Kallenberg	Linear Programming and Markov Decision Chains
594	A. Hordijk and L.C.M. Kallenberg	Constrained Undiscounted Stochastic Dynamic Programming
595	D.P. Heyman and M.J. Sobel	Stochastic Models in Operations Research
596	D.P. Heyman and M.J. Sobel	Stochastic Models in Operations Research
597	W.S. Jewell	Markov-Renewal Programming I: Formulation Finite
598	S.M. Ross	Average Cost Semi-Markov Decision Processes
599	S.M. Ross	Applied Probability Models with Optimization Applications
600	P.J. Schweitzer	Iterative Solution of the Functional Equations of
601	H.C. Tijms	Stochastic Modelling and Analysis a Computational
602	A.F. Veinott	Discrete Dynamic Programming With Sensitive
603	R.A. Howard	Semi-Markovian Decision Problems
604	De Cani J.S.	A Dynamic Programming Algorithm for Embedded Markov
605	A. Jensen	Markov Chains As an Aid to the Study of Markov Processes
606	C. Baier and M. Kwiatkowska and M. Ryan and	Symbolic Model Checking for Probabilistic Processes
607	M. Huth and M. Kwiatkowska	Quantitative Analysis and Model Checking
608	C. Baier	Polynomial Time Algorithms for Testing
609	J. Hillston	A Compositional Approach to Performance Modelling
610	J. Hillston	Compositional Markovian Modelling Using a
611	S. Gilmore and J. Hillston	The PEPA Workbench: A Tool to Support a
612	J.K. Muppala and K.S. Trivedi	Composite Performance and Availability Analysis
613	G. Ciardo and J.K. Muppala and K.S. Trivedi	On the Solution of GSPN Reward Models
614	W.H. Sanders and J.F. Meyer	Reduced Base Model Construction Methods for
615	A.F. Veinott	Personal Communication
616	C. Baier and H. Hermanns	Weak Bisimulation for Fully Probabilistic Processes
617	B. Delyon and O. Maler	On the Effects of Noise and Speed on Computation
618	A.F. Veinott	Markov Decision Chains
619	O. Maler	A Decomposition Theorem for Probabilistic Transition
620	B. Jonsson and Y. Wang	Compositional Testing Preorders for Probabilistic Processes
621	N.A. Lynch and M. Tuttle	Hierarcical Correctness Proofs for Distributed
622	S.-H. Wu and S.A. Smolka and E.W. Stark	Composition and Behaviors of Probabilistic I/O
623	S. Yuen and R. Cleaveland and Z. Dayar and S.A. Smolka	Fully Abstract Characterizations of Testing Preorders for
624	T.E.S. Raghavan and S.H. Tijs and O.J. Vrieze	On Stochastic Games with Additive Reward and
625	A.J. Hoffman and R.M. Karp	On Nonterminating Stochastic Games
626	T.E.S. Raghavan and J.A. Filar	Algorithms for Stochastic Games --- A Survey
627	L.S. Shapley	Stochastic Games
628	G. Balbo	On the Success of Stochastic Petri Nets
629	M.K. Molloy	On the Integration of Delay and Throughput Measure In
630	S. Natkin	Les Reseaux de Petri Stochastiques et leur
631	F.J.W. Symons	Introduction to Numerical Petri Nets
632	Ajmone Marsan M. and G. Balbo and G. Conte	A Class of Generalized Stochastic Petri Nets
633	J.K. Muppala and K.S. Trivedi	Composite Performance and Availability Analysis Using
634	J.F. Meyer and A. Movaghar and W.H. Sanders	Stochastic Activity Networks: Structure Behavior
635	White C.C. III and H.K. Eldeib	Markov Decision Processes with Imprecise Transition
636	K.S. Trivedi	Probability and Statistics with Reliability Queuing
637	W. Feller	An Introduction to Probability Theory and Its Applications
638	L. Breiman	Probability
639	Y. Azar and A.Z. Broder and A.R. Karlin and	Biased Random Walks
640	K.D. Heitmann	Temporal Logic applied to Reliability Modelling of
641	X.-R. Cao and X.-M. Yuan and L. Qiu	A Single Sample Path-Based Performance Sensitivity
642	H. Baruh and T. Altiok	Analytical Perturbations in Markov Chains
643	Cocozza-Thivent C. and Roussignol M.	Stability of Recurrence of a Markov Chain Under a
644	De Nicola R. and M. Hennessy	Testing Equivalences for Processes
645	S. Hart and M. Sharir	Concurrent Probabilistic Programs or: How to
646	S. Hart and M. Sharir and A. Pnueli	Termination of Probabilistic Concurrent Programs
647	I. Christoff	A Method for Verification of Trace and Test Equivalence
648	C.-C. Jou and S.A. Smolka	Equivalences Congruences and Complete
649	A. Giacalone and C. Jou and S.A. Smolka	Algebraic Reasoning for Probabilistic Concurrent
650	M.K. Molloy	Performance Analysis Using Stochastic Petri Nets
651	Y. Wang and K.G. Larsen	Testing Probabilistic and Nondeterministic Processes
652	R. Cleaveland and S.A. Smolka and A. Zwarico	Testing Preorders for Probabilistic Processes
653	K.G. Larsen and A. Skou
654	H.A. Hansson and B. Jonsson	A Calculus for Communicating Systems With Time and
655	M. Bernardo and L. Donatiello and R. Gorrieri	Modeling and Analyzing Concurrent Systems with MPA
656	M. Bernardo and L. Donatiello and R. Gorrieri	Integrated Analysis of Concurrent Distributed Systems using
657	M. Bernardo and R. Gorrieri	Extended Markovian Process Algebra
658	Bernardo M. and Busi N. and Gorrieri R.	A Distributed Semantics for EMPA Based on Stochastic
659	X.J. Chen and F. Corradini and R. Gorrieri	A Study on the Specification and Verification of
660	Bernardo M. and Donatiello L. and Gorrieri R.	Giving a Net Semantics to Markovian Process Algebra
661	H. Hermanns and U. Herzog and V. Mertsiotakis	Exploiting Stochastic Process Algebra Achievements
662	H.N. G\otz and U. Herzog and M. Rettelbach	Multiprocessor and Distributed System Design: the
663	P. Buchholz	Markovian Process Algebra: Composition and Equivalence
664	S. Donatelli and M. Ribaudo and J. Hillston	A Comparison of Performance Evaluation Process
665	Ajmone Marsan M. and G. Balbo and G. Conte and	Modelling with Generalized Stochastic Petri Nets
666	M. Ribaudo	Stochastic Petri Net Semantics for Stochastic
667	C. Morgan and A. McIver and K. Seidel	Probabilistic Predicate Transformers
668	N. Lynch	Proving Performance Properties (even Probabilistic Ones)
669	B. Bloom and A.R. meyer	A Remark on Bisimulation between Probabilisti Processes
670	C. Derman	Stable Sequential Control Rules and Markov Chains
671	C. Derman	On Sequential Decisions and Markov Chains
672	C. Derman	On Sequential Control Processes
673	C. Derman and R. Strauch	A Note on Memoryless Rules for Controlling
674	R. Strauch and A.F. Veinott	A Property of Sequential Control Processes
675	A.F. Veinott	On Finding Optimal Policies in Discrete Dynamic
676	L. Ramshaw	Formalizing the Analysis of Algorithms
677	He J. and McIver A.K. and Seidel K.	Probabilistic Models for the Guarded Command
678	R.E. Strauch	Negative Dynamic Programming
679	R. Segala	Testing Probabilistic Automata
680	R. Gorrieri and M. Roccetti and E. Stancampiano
681	R. Gorrieri and M. Roccetti	Towards Performance Evaluation in Process Algebras
682	M. Bernardo and L. Donatiello and R. Gorrieri	MPA: a Stochastic Process Algebra
683	M. Bernardo and L. Donatiello and R. Gorrieri	Operational GSPN Semantics of MPA
684	J.L. Doob	Measure Theory
685	de Alfaro L.	Formal Verification of Probabilistic Systems
686	de Alfaro L.	Formal Verification of Probabilistic Systems
687	Iyer P. and Narasimha M.	Probabilistic Lossy Channel Systems
688	C. Baier and M.Z. Kwiatkowska	Automatic Verification of Liveness Properties of
689	H. Mine and Y. Tabata	Linear Programming and Continuous Markovian
690	A. Federgruen and H.C. Tijms	The Optimality Equation in Average Cost
691	de Alfaro L.	How to Specify and Verify the Long-Run Average
692	Liu Z. and Ravn A.P. and Sorensen E.V. and Zhou C.C.	A Probabilistic Duration Calculus
693	W.J. Stuart	Introduction to the Numerical Solution of Markov Chains
694	L.H. Landweber	Decision Problems for $omega$--Automata
695	D. Ferrari	Recursive Repeated Games with Absorbing States
696	J. Flesch and F. Thuijsman and O.J. Vrieze	The Complexity of Stochastic Games
697	A. Condon
698	J.-Y. Cai and A. Condon and R.J. Lipton	Playing Games of Incomplete Information
699	A. Condon and R.E. Ladner	Probabilistic Game Automata
700	A. Condon	Space-Bounded Probabilistic Game Automata
701	H.J. Kushner and S.G. Chamberlain	Finite State Stochastic Games: Existence Theorems
702	P. Secchi	Stationary Strategies for Recursive Games
703	J.H. Eaton and L.A. Zadeh	Optimal Pursuit Strategies in Discrete-State
704	H. Everett	Recursive Games
705	P.R. Kumar and T.H. Shiau	Existence of Value and Randomized Strategies in
706	M. Bernardo	An Algebra-Based Method to Associate Rewards with
707	G. Clark	Formalising the Specification of Rewards with PEPA
708	R. Isaacs	Differential Games
709	von Neumann J.	Zur Theorie der Gesellschaftsspiele
710	O.J. Vrieze and S.H. Tijs and T.E.S. Raghavan and	A Finite Algorithm for the Switching Controller
711	T. Ba\csar and G.J. Olsder	Dynamic Noncooperative Game Theory
712	A. Maitra and J. Sudderth	An Operator Solution of Stochastic Games
713	D. Gillette	Stochastic Games with Zero Stop Probabilities
714	M. Stern	On Stochastic Games with Limiting Average Payoff
715	J.A. Filar and T.E.S. Raghavan	A Matrix Game Solution of the Single-Controller
716	J.A. Filar	Ordered Field Property for Stochastic Games when the
717	O.J. Vrieze and S.H. Tijs and T.E.S. Raghavan	A Finite Algorithm for the Switching Controller
718	M.J. Sobel	Myopic Solutions of Markov Decision Processes
719	T. Parthasarathy and S.H. Tijs and O.J. Vrieze	Stochastic Games with State Independent Transitions and
720	T.E.S. Raghavan and S.H. Tijs and O.J. Vrieze	On Stochastic Games with Additive Reward and
721	U. Zwick and M. Paterson	The Complexity of Mean Payoff Games on Graphs
722	J. Filar and K. Vrieze	Competitive Markov Decision Processes
723	F. Thuijsman and O.J. Vrieze	The Bad Match a Total Reward Stochastic Game
724	C. Beeri	On the membership problem for functional and
725	R. Cleaveland and B. Steffen	A Linear-Time Model-Checking Algorithm for the
726	C. Baier and M. Kwiatkowska	On the Verification of Qualitative Properties of
727	M. Kwiatkowska	Survey of Fairness Notions
728	de Alfaro L. and T.A. Henzinger and O. Kupferman	Concurrent Reachability Games
729	de Alfaro L.	Stochastic Transition Systems
730	R. Alur and T.A. Henzinger	Finitary Fairness
731	de Alfaro L. and T.A. Henzinger and O. Kupferman	Concurrent Reachability Games
732	M. Vardi	Infinite games against nature
733	D.P. Bertsekas and J.N. Tsitsiklis	Neuro-Dynamic Programming
734	M.Z. Kwiatkowska and G. Norman and D. Parker and R. Segala	Symbolic Model Checking of Concurrent Probabilistic
735	D.P. Bertsekas	Nonlinear Programming
736	J.H. Reif	The Compexity of Two-Player Games of Incomplete
737	de Alfaro L.	From Fairness to Chance
738	de Alfaro L.	The Verification of Probabilistic Systems Under Memoryless
739	M. Kwiatkowska and G. Norman and D. Parker	Personal communication
740	M. Bozga and O. Maler	On the Representation of Probabilities over Structured
741	de Alfaro L.	Computing Minimum and Maximum
742	C. Baier	On Algorithmic Verification Methods for Probabilistic
743	E.W. Stark and S.A. Smolka	Compositional Analysis of Expected Delays in Networks of
744	Kleinrock L.	Queuing Theory
745	M. Kwiatkowska and G. Norman and R. Segala and	Automatic Verification of Real-Time Systems with
746	C. Baier and J.P. Katoen and H. Hermanns	Symbolic Model Checking of Continuous-Time Markov Chains
747	G. Gottlob and N. Leone and H. Veith	Second Order Logic and the Weak Exponential Hierarchies
748	A.K. Chandra and D.C. Kozen and L.J. Stockmeyer	Alternation
749	J. Rumbaugh and G. Booch and I. Jacobson	The UML Reference Guide
750	R. Alur and T.A. Henzinger	Local Liveness for Compositional Modeling of Fair
751	L. de Alfaro and T.A. Henzinger and F.Y.C. Mang	Detecting Errors Before Reaching Them
752	J.A. Bergstra and J.W. Klop	Algebra of Communicating Processes with Abstraction
753	M. Hennessy	Algebraic Theory of Processes
754	R. Milner	Communication and Concurrency
755	E. Clarke and K. McMillan and S. Campos and	Symbolic Model Checking
756	N. Halbwachs and P. Caspi and P. Raymond and D. Pilaud	The Synchronous Dataflow Programming Language Lustre
757	P. Caspi and D. Pilaud and N. Halbwachs and J. Plaice	Lustre: a Declarative Language for Programming
758	G. Berry	The Synchronous Language ESTEREL
759	G. Berry
760	G. Berry and G. Gonthier	The Synchronous Programming Language ESTEREL:
761	le Guernic P.	SIGNAL --- A Data Flow-Oriented Language for Signal Processing
762	L. de Alfaro and M. Kwiatkowska and G. Norman and	Symbolic Model Checking of Concurrent Probabilistic
763	D.A. Martin	An extension of Borel determinacy
764	D.A. Martin	The determinacy of Blackwell games
765	D. Ornstein	On the Existence of Stationary Optimal Strategies
766	D.P. Bertsekas and S.E. Shreve	Existence of Optimal Stationary Policies in Deterministic
767	L. de Alfaro and T.A. Henzinger	Concurrent Omega-Regular Games
768	G. Owen	Game Theory
769	J. von Neumann and O. Morgenstern	Theory of games and economic behavior
770	T.A. Henzinger and R. Majumdar	A classification of symbolic transition systems
771	E.A. Emerson and C.S. Jutla and A.P. Sistla	On model checking for fragments of $mu$-calculus
772	A. McIver	Reasoning About Efficiency Within a Probabilitic
773	T.A. Henzinger	The Theory of Hybrid Automata
774	R. Bloem and H.N. Gabow and F. Somenzi	An Algorithm for Strongly Connected Component
775	G. Bhat and R. Cleaveland	Efficient Model Checking via the Equational $mu$-Calculus
776	IXActa Visual Software	Ixsite Web Analyzer
777	Link Alarm Inc.	Link Alarm
778	NetMechanic Inc.	HTML Toolbox
779	Tilman Hausherr	Link Sleuth
780	InContext	Web Analyzer 2.0
781	Watchfire Co.	Linkbot
782	Biggbyte Software Inc.	InfoLink
783	Electronic Software Publishing Co.	LinkScan
784	Internet Software Services	Theseus
785	DACPro Computer Solutions	WebTester
786	Voget Selbach Enterprises GmbH	Link Tester
787	C. Musciano and B. Kennedy	HTML: The Definitive Guide
788	D. Raggett and A. Le Hors and I. Jacobs	HTML 4.01 Specification
789	F.Y.C. Mang	Personal Communication
790	R. Fielding and J. Gettys and J.C. Mogul and	Hypertext Transfer Protocol --- HTTP/1.1
791	J.R. Burch and E.M. Clarke and D.E. Long	Symbolic Model Checking with Partitioned Transition
792	A. Tarski	A Lattice-Theoretical Fixpoint Theorem and Its Applications
793	E.M. Clarke and O. Grumberg and D.A. Peled	Model Checking
794	Aurel A. Lazar and Ariel Orda and Dimitrios E. Pendarakis	Virtual path bandwidth allocation in multiuser
795	Yannis A. Korilis and Aurel A. Lazar and Ariel Orda	Deciding Bisimilarity is P-Complete
796	J. Balcazar and J. Gabarro and M. Santha
797	E.A. Lee and Yuhong Xiong	System-Level Types for Component-Based Design
798	D. Jackson	Enforcing Design Constraints with Object Logic
799	N. Leveson	System Safety and Computers
800	D.M. Yellin and R.E. Strom	Protocol Specifications and Component Adapters
801	R. Allen and D. Garland	Formalizing Architectural Conection
802	T.A. Henzinger and B. Horowitz and R. Majumdar	Rectangular Hybrid Games
803	M. Kwiatkowska and G. Norman and J. Sproston	Symbolic Computation of Maximal Probabilistic Reachability
804	P. Iyer and M. Narasimha	Probabilistic Lossy Channel Systems
805	M. Kwiatkowska and G. Norman and R. Segala and J. Sproston	Verifying Quantitative Properties of Continuous
806	M. Kwiatkowska and G. Norman and R. Segala and J. Sproston	Automatic Verification of Real-Time Systems with
807	L. Ljung and T. Glad	Modeling of Dynamic Systems
808	T. S\oderstr\om and P. Stoica	System Identification
809	G.E.P. Box and G.M. Jenkins and G.C. Reinsel	Time Series Analysis: Forecasting and Control
810	L. Ljung	System Identification Toolbox 5
811	T.A. Henzinger and B. Horowitz and Meyer Kirsch C.	Embedded Control Systems Development with Giotto
812	T.A. Henzinger and B. Horowitz and Meyer Kirsch C.	Giotto: A Time-Triggered Language for Embedded
813	T.J. Koo	Hybrid System Design and Embedded Controller
814	T.J. Koo	Hierarchical System Architecture for Multi-Agent
815	T. J. Koo and G.J. Pappas and S. Sastry	Multi-Modal Control of Systems with Constraints
816	A. Balluchi and Di Benedetto M. and C. Pinello	Hybrid Control for Automotive Engine Management: The
817	J. Lygeros and D.N. Godbole and S. Sastry	A Game Theoretic Approach to Hybrid System Design
818	J. Lygeros and C. Tomlin and S. Sastry	Controllers for Reachability Specifications for
819	J.D. Hamilton	Time Series Analysis
820	J.D. Hamilton	A New Approach to the Economic Analysis of
821	J.D. Hamilton	Analysis of Time Series Subject to Changes in Regime
822	A. Ang and G. Bekaert	Regime Switches in Interest Rate
823	S.F. Gray	Modeling the Conditional Distribution of Intereset
824	S.J. Cecchetti and P. Lam and N.C. Mark	The Equity Premium and the Risk-Free Rate: matching
825	R. Garcia	Asymptotic Null Distribution of the Likelihood Ratio
826	The Mathworks	Real Time Workshop
827	Wind River Systems	VxWorks Programmer's Guide 5.4
828	T.A. Henzinger and J.-F. Raskin and P.-Y. Schobbens	The regular real-time languages
829	S. Yovine	Kronos: A Verification Tool for Real-Time Systems
830	M. Bozga and C. Daws and O. Maler and A. Olivero	Kronos: a Model-Checking Tool for Real-Time Systems
831	C. Daws and A. Olivero and S. Tripakis and S. Yovine	The took KRONOS
832	J. Bengtsson and K.G. Larsen and F. Larsson and	UPPAAL --- A Tool Suite for Automatic Verification
833	G. Buttazzo	Hard Real-Time Computing Systems: Predictable
834	H. Kopetz	Real-Time Systems: Design Principles for Distributed
835	L. de Alfaro and R. Alur and R. Grosu and	Mocha: A Model Checking Tool that Exploits Design
836	I. Chang and C.G. Tiao and C. Chen	Estimation of Time Series Parameters in the Presence
837	A.G. Bruce and R.D. Martin	Leave-$k$-out Diagnostics for Time Series
838	R.D. Martin and V.J. Yohai	Influence Functionals for Time Series
839	R.S. Tsay	Time Series Model Specification in the Presence of
840	J.R. Jackson	Scheduling a Production Line to Minimize Maximum
841	W. Horn	Some Simple Scheduling Algorithms
842	M.L. Dertouzos	Control Robotics: The Procedural Control of
843	C.L. Liu and J.W. Layland	Scheduling Algorithms for Multiprogramming in a
844	M.L. Noga	LegOS
845	L. de Alfaro and T.A. Henzinger and R. Majumdar	Symbolic Algorithms for Infinite-State Games
846	L. de Alfaro and R. Majumdar	Quantitative Solution of Omega-Regular Games
847	L. de Alfaro and T.A. Henzinger and F.Y.C. Mang	The Control of Synchronous Systems
848	L. de Alfaro and T.A. Henzinger and F.Y.C. Mang	The Control of Synchronous Systems Part II
849	J. Misra and K.M. Chandy	Proofs of networks of processes
850	R. Alur and T.A. Henzinger	Reactive Modules
851	L. de Alfaro and T.A. Henzinger and R. Jhala	Compositional Methods for Probabilistic Systems
852	D. L. Detlefs and Rustan M. Leino K. and G. Nelson	Extended Static Checking
853	E.A. Lee	Overview of the Ptolemy Project
854	E.A. Lee	What's Ahead for Embedded Software?
855	W. Tan and A. Zakhor	Video Multicast using Layered FEC and Scalable
856	W. Tan and A. Zakhor	Multicast Transmission of Scalable Video using
857	S. McCanne and S. Floyd	ns --- Network Simulator
858	E.J. Hannan	Time Series Analysis
859	E.J. Hannan and M. Deistler	The Statistical Theory of Linear Systems
860	L. de Alfaro and T.A. Henzinger and R. Majumdar	From Verification to Control: Dynamic Programs for
861	R.O. Duda and P.E. Hart	Pattern Classification and Scene Analysis
862	L. de Alfaro and T.A. Henzinger	Interface Automata
863	L. de Alfaro and T.A. Henzinger	Interface Theories for Component-Based Design
864	C.A.R. Hoare	An Axiomatic Basis for Computer Programming
865	S. Owicki and D. Gries	An Axiomatic Proof Technique for Parallel Programs
866	W. Reisig	Petri Nets: an Introduction
867	V. Pratt	Anatomy of the Pentium Bug
868	D.L. Dill	The Murphi Verification System
869	G.J. Holzmann
870	P. Kurshan	Computer-Aided Verification of Coordinating
871	P. Godefroid	Model Checking for Programming Languages using VeriSoft
872	T. Ball and S.K. Rajamani	Automatically Validating Temporal Safety Properties
873	J. Corbett and M. Dwyer and J. Hatcliff	Bandera: Extracting Finite-state Models from Java Source Code
874	K. Butts and D. bostic and A. Chutinan and J. Cook	Usage Scenarios for an Automated Model Compiler
875	de Alfaro L. and T.A. Henzinger and R. Majumdar	From Verification to Control: Dynamic Programs
876	M.Y. Vardi and P. Wolper	Reasoning about infinite computations
877	A. Baugnard and J.-M. J\'ez\'equel and N. Plouzeau	Making Components Contract Aware
878	R.B. Findler and M. Latendresse and M. Felleisen	Behavioral Contracts and Behavioral Subtyping
879	R.C. Holt and J.R. Cordy	The Turing Programming Language
880	D.C. Luckam and von Henke F.	An Overview of Anna a Specification Language for Ada
881	D.L. Parnas	A Technique for Software Module Specification with
882	D.S. Rosenblum	A Practical Approach to Programming with Assertions
883	Robert Allen and David Garlan	A Formal Basis for Architectural Connection
884	Roy H. Campbell and A. Nico Haberman	The Specification of Process Synchronization by Path
885	C.A. Gunter	Semantics of Programming Languages
886	R. Milner and J. Parrow and D. Walker	A calculus of Mobile Processes
887	S. Abramsky	Games in the Semantics of Programming Languages
888	S. Abramsky and K. Honda and G. McCusker	A Fully Abstract Game Semantics for General
889	S. Abramsky	Semantics of Interaction
890	Abramsky S. and Jagadeesan R. and Malacaria P.	Full Abstraction for PCF
891	Abramsky S. and Gay S. and Nagarajan R.	A type-theoretic approach to deadlock-freedom
892	A. Fehnker	Scheduling a steel plant with timed automata
893	Y. Abdedda\\im and O. Maler	Job-Shop Scheduling using Timed Automata
894	Wang Yi	Real-Time Behaviour of Asynchronous Agents
895	O. Maler and A. Pnueli and J. Sifakis	On the Synthesis of Discrete Controllers for Timed
896	E. Asarin and O. Maler and A.Pnueli and J. Sifakis	Controller Synthesis for Timed Automata
897	T.A. Henzinger and B. Horowitz and R. Majumdar	Rectangular Hybrid Games
898	de Alfaro L. and T.A. Henzinger and R. Majumdar	Symbolic Algorithms for Infinite-State Games
899	S.K. Rajamani and J. Rehof	A Behavioral Module System for the Pi-Calculus
900	S. Chaki and S.K. Rajamani and J. Rehof	Types as Models: Model Checking Message-Passing Programs
901	ITU-T recommendation Z.120	Message Sequence Charts
902	E. Rudolph and P. Graubmann and J. Gabowski	Tutorial on Message Sequence Charts
903	M. Merritt and F. Modugno and M. Tuttle	Time Constrained Automata
904	I. Walukiewicz	Pushdown processes: Games and model checking
905	A. Chakrabarti	Using Interface Automata for Component-Based Design
906	E. Gamma and R. Helm and R. Johnson and	Design Patterns
907	S. Abramsky	Semantics of Interaction
908	A. Chakrabarti and de Alfaro L. and T.A. Henzinger	Synchronous and Bidirectional Component Interfaces
909	A. Chakrabarti and de Alfaro L. and T.A. Henzinger	Interface Compatibility Checking for Software Modules
910	de Alfaro L. and T.A. Henzinger and M. Stoelinga	Timed Interfaces
911	de Alfaro L. and T.A. Henzinger and	Convertibility Verification and Converter Synthesis:
912	Mike Jones	What really happened on Mars Rover Pathfinder
913	I. Lee and A. Philippou and O. Sokolksy	Process Algeberaic Modeling and Analysis of
914	I. Lee and A. Philippou and O. Sokolksy	Formal Modeling and Analysis of Power-Aware Real-Time
915	I. Lee and J.-Y. Choi and H.-H. Kwak and	A Family of Resource-Bound Real-Time Process
916	M. N\'u\~nez and I. Rodr\'\igez	PAMR: A process algebra for the management of resources in
917	Y. Abdedda\ \i m and O. Maler	Job-Shop Scheduling using Timed Automata
918	Y. Abdedda\ \i m and O. Maler	Preemptive Job-Shop Scheduling using Stopwatch
919	G. Necula and S. McPeak and W. Weimer and R. To and	CIL: Infrastructure for C Program Analysis and
920	T.A. Henzinger and R. Jhala and R. Majumdar and	Temporal-Safety Proofs for Systems Code
921	T.A. Henzinger and R. Jhala and R. Majumdar and	Lazy Abstraction
922	G. Gullekson	Designing for Concurrency and Distribution with

SNo.	Books and Reports
1	rex
2	Hybrid Systems
3	POPL91
4	Workshop on Hybrid Systems
5	Proceedings of LICS'92
6	Hybrid Systems
7	Proc. Conf. Logics of Programs
8	The 25th Anniversary of INRIA
9	rex
10	LICS90
11	Formal Techniques in Real-Time and
12	LICS90
13	Logic Algebra and Computation
14	Real Time: Theory in Practice
15	rex
16	ICALP92
17	stacs92
18	1989 IEEE International Conference on
19	Workshop on Automatic Verification of
20	Proceedings of Concur'92
21	Proc. of the 27th ACM/IEEE Design Automation Conference
22	LICS88
23	Proc. of the Logic of Programs Conf.
24	FOCS89
25	Handbook of Theoretical Computer Science
26	Handbook of Theoretical Computer Science
27	Handbook of Theoretical Computer Science
28	lics94
29	Handbook of Theoretical Computer Science
30	Applications of Process Algebra
31	Proceedings of Concur'92
32	Proceedings of Concur'92
33	Handbook of Theoretical Computer Science
34	Handbook of Theoretical Computer Science
35	Handbook of Theoretical Computer Science
36	POPL86
37	rex93
38	Hybrid Systems
39	rex93
40	rex93
41	rex93
42	Proceedings of the 25th Annual Symposium on
43	Hybrid Systems
44	rex
45	cav91
46	Proc. Workshop on Theory of Hybrid Systems
47	IMACS SYMPOSIUM MCTS
48	CS351 Notes on Complexity Theory
49	Foundations of Software Technology and
50	Hand of Philosophical Logic
51	The Logical Way of Doing Things
52	Philosophical Problems in Logic
53	Philosophical Problems in Logic
54	Temporal Logic in Specification
55	podc83
56	Quantification in Modal Logic
57	Handbook of Philosophical Logic
58	Free Logics
59	Handbook of Philosophical Logic
60	Handbook of Philosophical Logic
61	5th Jerusalem Conference on Information Technology
62	Proc. IFIP 9th World Congress
63	cav93
64	HSIS
65	cade88
66	TACS 94
67	First International Conference on AI Planning Systems
68	6th Natl. Conf. on Artif. Intell.
69	lics86
70	cav93
71	Hybrid Systems
72	podc91
73	Handbook of Theoretical Computer Science
74	First and Second Russian Conference on Logic
75	First and Second Russian Conference on Logic
76	AAAI 88. Seventh National Conference on Artificial
77	Handbook of Logic in Computer Science
78	Mathematical Logic for Computer Science
79	Foundations of Computer Science IV
80	FOCS77
81	rex
82	Basic Tense Logic
83	Handbook of Philosophical Logic
84	Handbook of Philosophical Logic
85	A Completeness Proof in Modal Logic
86	Handbook of Philosophical Logic
87	rex93
88	Beauty is Our Business (a Birthday Salute to
89	Canergie Mellon University Computer Science:
90	ICALP89
91	Applying Formal Software Techniques
92	Dynamic Logic
93	Handbook of Philosophical Logic
94	Temi e prospettive della
95	Verification of the Futurebus+ Cache Coherence Protocol
96	11th IFIP WG10.2 International Conference on
97	Chapel Hill Conference on Very Large Scale Integration
98	Proceedings of the Third International Symposium
99	HardwareC --- A Language for Hardware Design
100	popl78
101	1985 Chapter Hill Conference on VLSI
102	Computer Networks
103	11th IFIP WG10.2
104	Diamonds and Defaults
105	lics93
106	lics93
107	lics93
108	Proceedings 13th World Computer Congress IFIP'9444
109	Esprit Project 6021 -- REACT: Building Correct
110	Protocol Specification Testing and Verification
111	Protocol Specification Testing and Verification
112	focs88
113	stoc89
114	Applications of Process Algebra
115	Continuous Verification by Discrete Reasoning
116	amast
117	cav91
118	podc87
119	IEEE Standard for Futurebus+ ---
120	IEEE Standard for Futurebus+ ---
121	Development of Hybrid Systems
122	Proceedings of the Third
123	popl85
124	popl85
125	stoc84
126	stoc84
127	lics90
128	Proc. Workshop on Logic of Programs
129	focs90
130	popl83
131	fsttcs
132	lics95
133	Logics and Models of Concurrent Systems
134	tacs94
135	lics95
136	lics95
137	lics95
138	Logics and Models of Concurrent Systems
139	rex90
140	rex90
141	rex91
142	cav96
143	rex91
144	cav91
145	Proc. Workshop on theory of Hybrid systems
146	Proc. of IEEE Real-Time Systems Symposium
147	Higher-Order Logic Theorem Proving and Its
148	stoc95
149	lics88
150	Proc. 8th Conference on Computer Aided
151	Computer Aided Verification Proc. 9th Int.
152	Proc. Compositionality Workshop
153	Proc. 10th Conferance on Concurrency Theory
154	icalp90
155	icalp90
156	icalp90
157	ftrtft94
158	Linear Time Branching Time and Partial order in
159	Temporal Logic in Specification Proceedings
160	Linear Time Branching Time and Partial Order in
161	Protocol Specification Testing and Verification X.
162	Real Time: Theory in Practice
163	CAAP '92. 17th Colloquium on Trees in Algebra and
164	Logic and Software Workshop
165	Hybrid Systems III
166	Theory of Machines and Computations
167	cav96
168	icalp94
169	icalp81
170	Advances in Database Technology -- EDBT'92: 3rd
171	POPL
172	stoc
173	icalp81
174	stacs97
175	Proc. of the International Conference on Digital
176	Workshop on Visual Reasoning International
177	Proc. of TAPSOFT: Theory and Practice of
178	Proc. of TACAS: Tools and Algorithms for the
179	Intl. Conf. on Temporal Logic
180	lics90
181	popl92
182	podc87
183	Second International Joint Conference on Artificial
184	Proc. of the Int. Summer School on Deductive
185	lics90
186	LICS86
187	stacs97
188	CAV95
189	Hybrid Systems Workshop DIMACS'95
190	cav95
191	stacs95
192	Proceedings of the Second International
193	cav97
194	lics96
195	Proc. of 5th Conference on Foundations of
196	lics89
197	cav98
198	lics95
199	focs97
200	cav96
201	cav96
202	cav97
203	popl77
204	Proceedings of the 38th Annual Symposium on
205	concur97
206	CONCUR 99: Concurrency Theory
207	CONCUR 97: Concurrency Theory
208	FMCAD 98: Formal Methods in Computer-aided Design
209	concur97
210	Proc. 5th International Symposium on
211	Proceedings of the 16th Annual Symposium on
212	focs91
213	stoc82
214	concur98
215	Proceedings of the International Conference on
216	Progress Measures Immediate Determinacy and a Subset
217	lics92
218	Computation Theory
219	cav95
220	cav95
221	TACAS 96
222	Berkeley Wireless Research Center
223	Proc. of TACAS: Tools and Algorithms for the
224	Design Automation Conference (DAC'99)
225	CAV 98: Computer-aided Verification
226	CAV 98: Computer-aided Verification
227	EL/IX: Unifying APIs for Linux and Post-PC
228	Proceedings of the IFIP Sixth International
229	8th International Conference on Computer-Aided
230	QNX Operating System: System Architecture
231	Infinitistic Methods
232	Real Time: Theory in Practice
233	Real Time: Theory in Practice
234	Protocol Specification Testing and Verification X.
235	Linear Time Branching Time and Partial Order in
236	Temporal Logic in Specification Proceedings
237	popl82
238	focs79
239	stoc83
240	stoc83
241	stoc83
242	stoc82
243	stoc80
244	concur92
245	concur92
246	cav91
247	popl89
248	lics91
249	focs88
250	focs85
251	lics90
252	stoc95
253	Logic of Programs: Workshop
254	stoc84
255	lics86
256	popl85
257	icalp91
258	focs83
259	Proc. of Real Time Systems Symposium
260	cav95
261	fsttcs95
262	icalp90
263	ftrtft94
264	concur94
265	MFCS'95
266	Math. Found. of Comp. Sci.
267	concur95
268	Proc. of Symp. on Principles of Distributed Computing
269	Proc. of Symp. on Principles of Distributed Computing
270	Uncertainty in Artificial Intelligence.
271	Proc. of the 26th Conference of Decision and Control
272	stacs
273	popl81
274	Intern. Stat. Inst.
275	icalp97
276	lics97
277	cav
278	Second Int. Work. on Numerical Solution of
279	7th Int. Conf. on Modelling Techniques and Tools
280	Computer Performance Evaluation:
281	cav
282	lics95
283	podc87
284	concur94
285	concur94
286	pnpm95
287	Fifth Int. Conf. on Modelling Techniques and
288	Int. Workshop on Timed Petri Nets
289	stoc92
290	Symp. on Formal Techniques in Real-Time and
291	Proc. of the International Workshop on Petri Nets and
292	Proc. of International Workshop on Process
293	Proc. Intl. Workshop on Automatic Verificaton
294	concur90
295	Proc. IFIP~TC2 Working Conference on
296	Protocol Specification Testing and Verification XII
297	icalp92
298	Bisimulation Through Probabilistic Testing
299	Proc. of IEEE Symp. on Real-Time Systems
300	Proc. of 2nd Workshop on Process Algebras and
301	Proc. of 7th IFIP Int. Conf. on Formal
302	concur96
303	amast
304	pnpm95
305	pnpm97
306	PERFORMANCE'93
307	papm94
308	pnpm95
309	pnpm95
310	concur96
311	A Theory of Processes with Durational Actions
312	amast
313	Proc. of TAPSOFT'97: Theory and Practice of
314	podc97
315	lics98
316	Proc. of the Second Intl. Workshop on Responsive
317	Computer Systems Performance Evaluation
318	Contributions to the Theory of Games III
319	icalp97
320	papm96
321	Contributions to the Theory of Games III
322	Selected Topics in OR and Mathematical Economics
323	cav
324	concur98
325	lics94
326	focs98
327	Proceedings of Workshop on Probabilistic Methods
328	Computer Aided Verification
329	concur99
330	lics98
331	ARTS 99
332	CONCUR 99
333	MFCS 95: Mathematical Foundations of Compuer
334	cav95
335	cav00
336	cav96
337	popl87
338	rex93
339	The Foundations of Esterel
340	Proof Language and Interaction: Essays in Honour
341	TACAS: Tools and Algorithms for the
342	lics00
343	STACS00: Theoretical Aspects of Computer Science
344	CAV 93: Computer-aided Verification
345	Proc. of PROBMIV
346	lics96
347	Proceedings of the Fourth International
348	lics96
349	VLSI 91
350	Achieving network optima using Stackelberg routing
351	Static Analysis Sumposium
352	Proc. of the 16th International Conference on
353	concur99
354	concur01
355	Proc. of TAPSOFT 97
356	concur00
357	arts99
358	To appear in Proc. of LCTES 01: ACM SIGPLAN
359	Proceedings of the First International
360	IEEE Conference on Decision and Control
361	IEEE Conference on Decision and Control
362	Proc. of HSCC 98: First Intl. Workshop
363	Hybrid Systems III
364	icalp98
365	cav98
366	Hybrid Systems III
367	Proc. of the 4th DIMACS Workshop on Verification
368	ICSE 01: Proceedings of the 23rd
369	concur01
370	stoc01
371	concur00
372	concur01
373	concur01
374	Packet Video Workshop
375	The ns Manual (formerly ns Notes and Documentation)
376	lics01
377	Proceedings of the Joint PAPM-PROBMIV 2001 Workshop
378	Proceedings of the 8th European Software
379	emsoft01
380	Theory and Practice of Software Development (TAPSOFT)
381	cav96
382	The Spin Model Checker
383	popl97
384	SPIN 2001 Workshop on Model Checking of Software
385	Proceedings of the 22nd International Conference
386	Proceedings of the First International
387	lics01
388	Proc. of the Joint 8th European Software
389	Operating Systems
390	Proc. of the 11th Amsterdam Colloquium
391	lics98
392	TACS'97: Theoretical Aspects of Computer
393	Proceedings of the 13th International Conference
394	concur90
395	stacs95
396	Proc. IFAC Symposium on System Structure and Control
397	concur99
398	concur01
399	Proc. SAS 01 Static Analysis Symposium
400	popl02
401	concur91
402	Trees in Algebra and Programming -- CAAP'96
403	cav02
404	cav02
405	Proceedings of the Second International
406	Proceedings of the International Conference on
407	Synthesis with incomplete informatio
408	2nd International Conference on Temporal Logic
409	Proc. of the 22nd IEEE/IEE Workshop on
410	Proc. of the 21st International Conference on
411	Proc. FORTE'01
412	CAV 01: Proc. of 13th Conf. on Computer Aided
413	Proc. of TACAS: Tools and Algorithms for the
414	cav02
415	Proceedings of the 29th Annual Symposium on