Table of Contents

• Static Analysis of Concurrent Programs Using Ordinary Differential EquationsZuohua Ding. 1-35 [doi]
• The PlusCal Algorithm LanguageLeslie Lamport. 36-60 [doi]
• The Secret Art of Computer ProgrammingAnnabelle McIver. 61-78 [doi]
• Verification, Testing and StatisticsSriram K. Rajamani. 79 [doi]
• ::::nu::::-Types for Effects and Freshness AnalysisMassimo Bartoletti, Pierpaolo Degano, Gian Luigi Ferrari, Roberto Zunino. 80-95 [doi]
• A First-Order Policy Language for History-Based Transaction MonitoringAndreas Bauer 0002, Rajeev Goré, Alwen Tiu. 96-111 [doi]
• Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-CompleteNikola Benes, Jan Kretínský, Kim Guldstrand Larsen, Jirí Srba. 112-126 [doi]
• Transmission Protocols for Instruction StreamsJan A. Bergstra, C. A. Middelburg. 127-139 [doi]
• A Deadlock-Free Semantics for Shared Memory ConcurrencyGérard Boudol. 140-154 [doi]
• On the Expressiveness of Forwarding in Higher-Order CommunicationCinzia Di Giusto, Jorge A. Pérez, Gianluigi Zavattaro. 155-169 [doi]
• On the Hairpin Completion of Regular LanguagesVolker Diekert, Steffen Kopecki, Victor Mitrana. 170-184 [doi]
• Context-Free Languages of Countable WordsZoltán Ésik, Szabolcs Iván. 185-199 [doi]
• Automatic Conflict Detection on ContractsStephen Fenech, Gordon J. Pace, Gerardo Schneider. 200-214 [doi]
• A Sound Observational Semantics for Modal Transition SystemsDario Fischbein, Víctor A. Braberman, Sebastián Uchitel. 215-230 [doi]
• Regular Expressions with Numerical Constraints and Automata with CountersDag Hovland. 231-245 [doi]
• On the Relative Expressive Power of Contextual Grammars with Maximal and Depth-First DerivationsLakshmanan Kuppusamy, Kamala Krithivasan. 246-260 [doi]
• Integration Testing from Structured First-Order Specifications via Deduction ModuloDelphine Longuet, Marc Aiguier. 261-276 [doi]
• A Minimized Assumption Generation Method for Component-Based Software VerificationPham Ngoc Hung, Toshiaki Aoki, Takuya Katayama. 277-291 [doi]
• A Formal Approach to Heuristically Test Restorable SystemsPablo Rabanal, Ismael Rodríguez, Fernando Rubio. 292-306 [doi]
• Constrained Reachability of Process Rewrite SystemsTayssir Touili. 307-321 [doi]
• Input-Output Model ProgramsMargus Veanes, Nikolaj Bjørner. 322-335 [doi]
• IMITATOR: A Tool for Synthesizing Constraints on Timing Bounds of Timed AutomataÉtienne André. 336-342 [doi]
• GSPeeDI - A Verification Tool for Generalized Polygonal Hybrid SystemsHallstein Asheim Hansen, Gerardo Schneider. 343-348 [doi]
• Hierarchical Graph Rewriting as a Unifying Tool for Analyzing and Understanding Nondeterministic SystemsKazunori Ueda, Takayuki Ayano, Taisuke Hori, Hiroki Iwasawa, Seiji Ogawa. 349-355 [doi]