Abstract is missing.
- Extended static checkingK. Rustan M. Leino. 1-2
- From lattices to practical formal hardware verificationCarl-Johan H. Seger. 3-4
- Programming with tabling in XSBDavid Scott Warren. 5-6
- Verifying electronic control unit: today and tomorrowWerner Damm. 7-8
- Teaching calculational logicDavid Gries. 9-10
- Types for treesFranco Barbanera, Mariangiola Dezani-Ciancaglini, Fer-Jan de Vries. 11-29
- Structures for lazy semanticsO. Bastonero, Alberto Pravato, Simona Ronchi Della Rocca. 30-48
- A proof theory of asynchronously communicating sequential processesFrank S. de Boer, Nissim Francez, M. van Hulst, Frank A. Stomp. 49-67
- Bisimulations in the join-calculusMichele Boreale, Cédric Fournet, Cosimo Laneve. 68-86
- Using state space exploration and a natural deduction style message derivation engine to verify security protocolsEdmund M. Clarke, Somesh Jha, Wilfredo R. Marrero. 87-106
- Programming language semantics in foundational type theoryKarl Crary. 107-125
- An algebraic approach to the specification of stochastic systemsPedro R. D Argenio, Joost-Pieter Katoen, Ed Brinksma. 126-147
- Refinement types for specificationEwen Denney. 148-166
- An extension of the program derivation formatA. J. M. van Gasteren, A. Bijlsma. 167-185
- Deadlines are terminationIan J. Hayes, Mark Utting. 186-204
- The design of a linearization of a concurrent data objectWim H. Hesselink. 205-224
- Final semantics for the pi-calculusFurio Honsell, Marina Lenisa, Ugo Montanari, Marco Pistore. 225-243
- Comparing CTL and PCTL on labeled Markov chainsMichael Huth, Marta Z. Kwiatkowska. 244-262
- Reactive functional programmingRichard B. Kieburtz. 263-284
- Imperative objects and mobile processesJosva Kleist, Davide Sangiorgi. 285-303
- Relating linear and branching model checkingOrna Kupferman, Moshe Y. Vardi. 304-326
- Verifying duration properties of timed transition systemsZhiming Liu, Anders P. Ravn, Xiaoshan Li. 327-345
- Towards squiggly refinement algebraDavid A. Naumann. 346-365
- Toward a theory of sequential hybrid programsParitosh K. Pandya, H.-P. Wang, Qiwen Xu. 366-384
- Test selection for object-oriented software based on formal specificationsCécile Péraire, Stéphane Barbey, Didier Buchs. 385-403
- Logical foundations for typed object-oriented languagesArnd Poetzsch-Heffter, Peter Müller. 404-423
- Verifying a self-stabilizing mutual exclusion algorithmShaz Qadeer, Natarajan Shankar. 424-443
- A combination of interval logic and linear temporal logicZ. Qiu, C. Zhou. 444-461
- A model of real-time distributed systemsAxel Wabenhorst. 462-482