Program Chairs: Doron A. Peled Department of Computer Science The University of Warwick Coventry, CV4 7AL, UK doron@dcs.warwick.ac.uk Moshe Y. Vardi Department of Comp. Science Rice University 6100 S. Main St. Houston, TX 77005 Phone: +1-713-348-5977 vardi@cs.rice.edu Program Committee: Rajeev Alur, UPenn Dines Bjorner, Tech. Univ. DK Gregor v. Bochmann, Univ. Ottawa Tommaso Bolognesi, IEI, Italy Ed Brinksma, Univ. Twente Ana Cavalli, INT, France Samuel Chanson, Hong Kong Univ. Piotr Dembinski, IPI-PAN, Poland Hubert Garavel, Inria Stefania Gnesi, CNR - IEI, Italy Gerard Holzmann, Bell Labs, USA Alan J. Hu, UBC, Canada Claude Jard, IRISA - CNRS, France Guy Leduc, Univ. Liege David Lee, Bell Labs, China Insup Lee, UPenn Stefan Leue, Univ. Freiburg Luigi Logrippo, Univ. Quebec a Hull Sjouke Mauw, Tech. Univ. Eindhoven Ken McMillan, Cadence, USA Mathew J. Morley, Verisity, USA Anca Muscholl, Univ. Paris 7 Elie Najm, ENST, France Doron Peled, Univ. Texas, Austin Alex Petrenko, CRIM, Canada Scott Smolka, SUNY Stony Brook Richard Tenney, Univ. Mass. Ken Turner, Univ. Stirling Moshe Vardi, Rice Univ. Son T. Vuong, Univ. BC, Mihalis Yannakakis, Avaya Labs, USA Steering Committee Gregor v. Bochmann, Univ. Ottawa Ed Brinksma, Univ. Twente Stanislaw Budkowski, INT, France Guy Leduc, Univ. Liege Elie Najm, ENST, France Richard Tenney, Univ. Mass. Ken Turner, Univ. Stirling

The IFIP TC6 WG 6.1 Joint International Conference on Formal Techniques for Networked and Distributed Systems (FORTE) is focused on formal methods for communication protocols. FORTE is the new name of the joint FORTE/PSTV meeting, which has combined Monday Nov 11th Tutorials day 9:00- 9:50 (Chair: M.Y. Vardi) Invited Tutorial: Ed Clarke: Symbolic Model Checking 10:00-10:50 (Chair: M.Y. Vardi) Invited Tutorial: Ed Clarke: Symbolic Model Checking 10:50-11:20 Coffee Break 11:20-12:10 (Chair: D.A. Peled) Invited Tutorial: Elaine Weyuker: Software Testing Basics I 12:15-14:00 Lunch 14:00-14:50 (Chair: D.A. Peled) Invited Tutorial: Elaine Weyuker: Software Testing Basics II 14:50-15:20 Coffee Break 15:20-16:10 (Chair: M.Y. Vardi) Invited Tutorial: Dave B. Johnson: Routing in Mobile and Wireless 16:20-17:10 (Chair: M.Y. Vardi) Invited Tutorial: Dave B. Johnson: Routing in Mobile and Wireless Data Networks. 17:30-19:30 Reception Tuesday Nov 12th 9:00-10:00 (Chair: D.A. Peled) Invited talk: Butler Lampson: Formal Methods for Design--How to Understand Your System Before (or After) You Build It. 10:00-10:30 Coffee Break 10:30-12:00 Modeling (Chair: T. Bolognesi) Encoding PAMR into (timed) EFSMs Authors: Manuel Nunez, Ismael Rodriguez Submodule construction for specifications with input assumptions and output guarantees Authors: G.V. Bochmann Congruent Weak Conformance, a Partial Order among Processes Authors: Ronald Brower, Kenneth Stevens 12:00-13:30 Lunch 13:30-14:30 (Chair: D.A. Peled) Invited talk: Elaine Weyuker: The Role of Prediction in Producing Dependable Software 14:30-15:00 Coffee Break 15:00-15:45 Tools and Posters (Chair: C. Jard) Tool: Innovative Verification Techniques Used in the Implementation of a Third-Generation 1.1GHz 64b Microprocessor Authors: Victor Melamed, Harry Stuimer, David Wilkins, Lawrence Chang, Fred Lowe, Kevin Normoyle, George Konstantinidis, Sutikshan Bhutani Tool: Mechanical Translation of I/O Automaton Specifications into First-Order Logic Authors: Andrej Bogdanov, Stephen Garland, Nancy Lynch Poster: Verification of Event-Based Synchronization of SpecC Description Using Difference Decision Diagrams Authors: Thanyapat Sakunkonchak, Masahiro Fujita Poster: A Distributed Partial Order Reduction Algorithm Authors: Robert Palmer 16:00-17:30 Testing (Chair: E. Weyuker) Protocol Techniques for Testing Radiotherapy Accelerators Authors: Kenneth Turner, Bing Qian System Test Synthesis from UML Models of Distributed Software Authors: Simon Pickin, Claude Jard, Yves Le Traon, Thierry Jeron, Jean-Marc Jezequel, Alain Le Guennec Formal Test Purposes and The Validity of Test Cases Authors: Stephan Tobies, Peter Deussen 17:30-18:30 Tool Demo and Poster Presentation (Chair: M. Vardi) 19:00-21:00 Program and Steering Committees Dinner Wednesday Nov 13th 09:00-10:00 (Chair: D.A. Peled) Invited talk: Ed Clarke: Counterexample Guided Abstraction Refinement using SAT. 10:00-10:30 Coffee Break 10:30-12:00 Reliable Services (Chair: G. Leduc) Use of Logic to describe Enhanced Communications Services Authors: Stephan Reiff-Marganiec, Kenneth Turner A Formal Venture into Reliable Multicast Territory Authors: Carolos Livadas, Nancy Lynch Modelling SIP Services Authors: Kenneth Turner 12:00-13:30 Lunch 13:30-14:30 (Chair: M.Y. Vardi) Invited talk: David Harel: Can Behavioral Requirements Be Executed? (And Why Would We Want to Do So?) 14:30-15:00 Coffee Break 15:00-16:30 Protocol Verification (Chair: E.M. Clarke) Verifying reliable data transmission over UMTS radio interface with High Level Petri Nets Authors: Teemu Tynjala, Sari Leppanen, Vesa Luukkala Verifying Randomized Byzantine Agreement Authors: Marta Kwiatkowska , Gethin Norman Automatic SAT-Compilation of Protocol Insecurity Problems via Reduction to Planning Authors: Alessandro Armando, Luca Compagna 16:45-18:15 Model Checking (Chair: A. Petrenko) Visual Specifications for Modular Reasoning about Asynchronous Systems Authors: Nina Amla, E Allen Emerson, Kedar Namjoshi, Richard Trefler Bounded Model Checking for Timed Systems Authors: Gilles Audemard, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani Symmetric Symbolic Safety-Analysis of Concurrent Software with Pointer Data Structures Authors: Farn Wang, Karsten Schmidt 18:30-21:30 Cocktail Hour and Conference Banquet After-dinner talk: Dan Wallach: Adventures in Copy Protection Research Thursday Nov 14th 9:00-10:00 (Chair: M.Y. Vardi) Invited talk: David Harel: An Algorithmic Approach for Formalizing and Acheiving Odor Communication and Synthesis. 10:00-10:30 Coffee Break 10:30-12:00 Modeling (G. Bochman) C Wolf -- A tool for extracting models from C Programs Authors: Daniel DuVarney, Purush Iyer NTIF: a General Symbolic Model for Communicating Sequential Processes with Data Authors: Hubert Garavel, Frederic Lang Building tools for LOTOS Symbolic Semantics in Maude Authors: Alberto Verdejo 12:00-13:30 Lunch 13:30-15:30 Model checking (Chair: K. Turner) A Compositional Sweep-Line State Space Exploration Method Authors: Lars Kristensen, Thomas Mailund From States to Transitions: Improving Translation of LTL Formulae to Buchi automata Authors: Dimitra Giannakopoulou, Flavio Lerda A Nested Depth First Search Algorithm for Model Checking with Symmetry Reduction Authors: Dragan Bosnacki On combining the Persistent Set Method with the Covering Step Graph Method Authors: Pierre-Olivier Ribet, Francois Vernadat, Bernard Berthomieu