crodrig@imag.imag.fr (Carlos Rodriguez) (05/07/89)
Workshop on Automatic Verification Methods for Finite State Systems Grenoble, June 12-14, 1989 Objectives This workshop is dedicated to bringing together researchers and practitioners interested in the development and use of methods, tools and theories for automatic verification of finite state systems. The goal of the workshop is the comparison of various verification methods for finite state systems, and tools to assist the application designer. Emphasis will be not only on new research results but also on the applications of existing results to real verification problems. Special sessions for demonstrations of verification tools are planned. Program Committee E.M. Clarke, A. Pnueli, J. Sifakis Local Arrangements J. Sifakis, LGI/IMAG, B.P. 53, 38041 Grenoble Cedex, France; tel. +33-76513379; e-mail: sifakis@imag.fr Sponsorship The workshop is sponsored by C-cube, the French National Project on Parallel Processing. PRELIMINARY PROGRAM Sunday, June 11 Reception, 7:30pm-9:30pm Monday, June 12 8:30-9:00 Reception, 8:30am-9:00am Session 1: Tools for Process Algebras 9:00 Process Calculi Verification Tools G. Boudol, R. de Simone (INRIA, Sophia Antipolis) 9:30 The concurrency Workbench R. Cleaveland, (Univ. of Sussex), J. Parrow, (SICS),B. Steffen, (Edinburgh) 10:00 Using Axiomatic Presentation of Behavioural Equivalences for Manipulating CCS Specifications R. De Nicola, P. Inerardi (IEI-CNR, Pisa), M. Nesi (Consorzio Pisa Riserche, Pisa) 10:30-11:00 Coffee break 11:00 Argonaute: Graphical Description, Semantics and Verification of Reactive Systems by Using a Process Algebra F. Maraninchi (LGI-IMAG, Grenoble) 11:30 Testing Equivalence as Bisimulation Equivalence R. Cleaveland, M. Hennessy, (Sussex) 12:00 Verification by Abstraction and Bisimulation H. Zuidweg (PTT Research Neher Lab., Leidschendam) 12:15 A Method for Verification of Trace and Test Equivalence I. Christoff, (Uppsala) 12:30 Proving Properties of Elementary Net Systems with a Special-Purpose Theorem Prover H. Tuominen, (Helsinki) 12:45-2:30 Lunch Session 2: Model checking 2:30 CCS, Liveness and Local Model Checking in the Linear Time Mu-Calculus C. Stirling, D. Walker, (Edinburgh) 3:00 Fair SMG and Linear Time Model Checking H. Barringer, G.D. Gough, M.D. Fisher (Manchester) 3:30 MEC: a System for Constructing and Analysing Transition Systems A. Arnold (Bordeaux) 4:00 Implementing a Model Checking Algorithm by Adapting Existing Automated Tools B. Jonsson, A. H. Khan, J. Parrow, (SICS, Stockholm) 4:15 On-Line Model-Checking for Linear Temporal Logic Specifications C. Jard, T. Jeron, (Irisa, Rennes) 4:30-6:00 Coffee break - Demonstrations Tuesday, June 13 Session 3: Protocol Validation 8:30 COSPAN: A Software System for Analysis of Coordination Z. Har'El, R. Kurshan (AT&T Bell Labs) 9:00 Algorithms for Automated Protocol Validation G.J. Holzmann (AT&T Bell Laboratories) 9:30 What are the Limits of Model Checking Methods for the Verification of Real Life Protocols? S. Graf, J-L. Richier, C. Rodriguez, J. Voiron (LGI-IMAG, Grenoble) 10:00 Experiences with Automated Verification Tools: Application to Discrete Event Systems M. Barbeau, G.V. Bochmann (Montreal) 10:30-11:00 Coffee break 11:00 State Exploration by Transformation with LOLA J. Quemada, S. Pavon, A. Fernandez, (ETSI, Madrid) 11:15 On Using PROTEAN to Verify ISO FTAM Protocols R. Lai (NEC, Melbourne), K.R. Parker (CSIRO, Melbourne), T.S. Dillon (La Trobe Univ., Melbourne) 11:30 Parallel Protocol Verification Using the Localized Approach: A two Phase Algorithm M.C. Yuang (Bell Comm. Research, Piscataway), A. Kershenbaum (Polyt. Univ. Brooklyn) 11:45 Requirement Analysis for Communication Protocols P. Azema, F. Bernadat (LAAS, Toulouse) 12:00 Panel: Protocol Validation Methods and Tools 12:30-2:00 Lunch Session 4: State Explosion Problem 2:00 Compositional Model Checking E. Clarke (CMU) 2:30 Network Grammars, Communication Behaviors and Automatic Verification Z. Shtadler, O. Grumberg, (Technion, Haifa) 3:00 Verifying Properties of Large Sets of Processes with Network Invariants P. Wolper, V. Lovinfosse (Liege) 3:30 Projections of the Reachability Graph and Environment Models, Two Approaches to Facilitate the Functional Analysis of Systems of Cooperating Finite State Machines H. Krumm, (Karlsruhe) 3:45-5:45 Coffee break -Demonstrations 5:45 Panel: The state explosion problem Wednesday, June 14 Session 5: Hardware Verification 9:00 Combining CTL, Trace Theory and Timing Models J.R. Burch (CMU) 9:30 Formal Verification of Synchronous Circuits based on String-Functional Semantics: The 7 Paillet Circuits in Boyer-Moore A. Bronstein, C. L. Talcott, (Stanford University) 10:00 Compositional Verification of VLSI Circuits J. Staunstrup, (CS Dept., Tech. Univ. of Denmark ), S. Garland, J. Guttag, (MIT) 10:30 Verification of Synchronous Sequential Machines Based on Symbolic Execution O. Coudert, C. Berthet, J-C. Madre, (Bull, Paris) 10:45 A Tool for the Parallel Composition of Finite-State Processes with Applications to Hardware Validation G.C. Gopalakrishnan (Univ. of Calgary) 11:00-11:30 Coffee break Session 6: Specification 11:30 Modal Specifications K. G. Larsen, (Aalborg) 12:00 The Inevitable Properties of Programs M.G. Gouda (Austin) 12:30 Specification of the Elevator Problem Using Temporal Logic W.G. Wood (Software Engineering Institute) 12:45-2:15 Lunch Session 7: Timed Specifications 2:15 Quantitative Temporal Reasoning E.A. Emerson, AK. Mok, J. Srinivasan (Austin), A.P. Sistla (GTE Research Lab.) 2:45 Timing Assumptions and Verification of Finite-State Concurrent Systems D.L. Dill (Stanford Univ.) 3:15 Specifying, Programming and Verifying Real-Time Systems Using a Synchronous Declarative Language N. Halbwachs, D. Pilaud, F. Ouabdesselam, A-C. Glory, (LGI-IMAG, Grenoble) 3:45 Automatic Verification of Timed Transition Systems J.S. Ostroff (York University) 4:00 Panel: Timed specifications 4:30-6:00 Coffee break - Demonstrations Social events Sunday : opening reception and cocktail at 7:30 pm Monday : concert at 7pm Tuesday: workshop banquet at 8pm Transportation Access from Paris: % By plane from Orly to Grenoble-St Geoirs airport. A shuttle goes from airport to Grenoble. % By the TGV train, from Gare de Lyon, in 3:30 hours. Access from Lyon: There are direct flights to Lyon-Satolas international airport, from many european places, and from New York. A shuttle goes from Satolas to Grenoble, for FF 100. ------------------------------------------------------------------------- Workshop on Automatic Verification Methods for Finite State Systems Grenoble, June 12-14, 1989 Registration Form (can be used as an invoice) ADR Reference: 160 89 501 Workshop secretary: ADR-LGI Please return this form before May 20 to J. Sifakis, ADR-LGI-IMAG, BP 53X, 38041 Grenoble Cedex France __________________________________________________________________________ Last name................................................................. First name................................................................ Institution .............................................................. Address................................................................... .......................................................................... .......................................................................... .......................................................................... Telephone........................................ e-mail.................. __________________________________________________________________________ Hotel reservation (prices include breakfast) Date of arrival........................................................... Date of departure......................................................... Single room Double room ___ ___ | | FF 250-FF 350 | | FF 350-FF450 --- --- A deposit of FF 300 is necessary for reservation. __________________________________________________________________________ Participation fees Participation fees include participants version of proceedings, 3 lunches, and social events. They are of FF 2,000 before May 20 and of FF 2,500 after this date. __________________________________________________________________________ Payment Send the amount including participation fees and a deposit of FF 300 for hotel room. ___ | | I am transfering the amount in French francs to --- BNP Grenoble-Berriat Account number 30 004/00 611/000 279 400 53/70 ___ | | I enclose a bank cheque made out in French francs payable to ADR --- Grenoble Cancellations postmarked not later than May 20 will receive full refund of participation fees. After May 15, 50% will de refunded. After June 1st no refund can be made. ____________________________________________________________________________ Date.................... Signature........................ Institution seal