Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 13 Apr 1995 18:18:21 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA203569333; Thu, 13 Apr 1995 10:08:53 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA203519328; Thu, 13 Apr 1995 10:08:48 -0600 Received: from vm1.ulg.ac.be (vm1.ulg.ac.be [139.165.32.1]) by dworshak.cs.uidaho.edu (8.6.10/1.0) with SMTP id JAA16028 for ; Thu, 13 Apr 1995 09:07:03 -0700 Received: from ia6.montefiore.ulg.ac.be by vm1.ulg.ac.be (IBM VM SMTP V2R2) with TCP; Thu, 13 Apr 95 18:06:45 +0200 Original-Received: from pw@localhost by ia6.montefiore.ulg.ac.be (8.6.10/ULG-7.5) id SAA01534 for info-hol@cs.uidaho.edu at Thu, 13 Apr 1995 18:06:58 +0200 PP-warning: Illegal Received field on preceding line Date: Thu, 13 Apr 1995 18:06:58 +0200 From: pw@montefiore.ulg.ac.be (Pierre Wolper) Message-Id: <199504131606.SAA01534@ia6.montefiore.ulg.ac.be> To: info-hol@cs.uidaho.edu Subject: CAV 95 Program and Call for participation PRELIMINARY ANNOUNCEMENT CONFERENCE ON COMPUTER-AIDED VERIFICATION (CAV '95) Liege, BELGIUM July 3 - July 5, 1995 This announcement and other information about the conference and Belgium is available through the www at http://www.montefiore.ulg.ac.be/cav95.html ------------------------------------------------------------------------------ GENERAL INFORMATION The Seventh Conference on Computer-Aided Verification will be held July 3-5 in Liege, BELGIUM. The CAV conference series is dedicated to the advancement of the theory and practice of computer-assisted formal verification. It is centered around the theme that computer assistance is essential for a wider use of verification techniques, but covers all styles of verification approaches and a variety of application areas. CAV 95 is sponsored by the Belgian National Fund for Scientific Research (F.N.R.S.) and the government of the "Communaute Francaise de Belgique". It is organised by the University of Liege in cooperation with the A.I.M. (Association des Ingenieurs de l'Institut Montefiore). TOOLS and APPLICATIONS: Equipment will be made available for the demonstration of verification tools. Posters about tools and applications are invited (send mail to cav95@montefiore.ulg.ac.be). LOCATION: Liege is a thousand-year-old city with a historical centre and numerous monuments, churches and museums. The conference will be held in the Conference Center (Palais des Congres) of Liege: Esplanade de l'Europe, 2, B-4020 LIEGE (Belgium) Tel.: + 32 41 43.01.44 Fax: + 32 41 43.20.85 TRAVEL: Liege is located one hundred kilometres east of Brussels and is easily reachable. By air: travellers arrive at Brussels National Airport; shuttle trains (Airport City Express) operate every 20 min. between the airport and the Central station of Brussels from where direct trains to Liege can be taken every hour at least between 6:00 to 24:00. By train: numerous international trains are routed via Liege, Guillemins station. By road: Liege is directly linked to the European motorway network through several motorways. Car parking facilities are available beneath the Conference Center and in the immediate vicinity. The Conference Center (Palais des Congres) is situated on the right bank of the River Meuse, a 20 minutes walk from the town centre. It is linked to the Guillemins railway station (route 17) and to the town centre (routes 26, 28, 31) by a regular bus service. REGISTRATION: Please complete the attached reservation form and either email, fax, or physically mail it with payment to the appropriate address. The registration desk will be open in the Conference Center from 7:00pm until 8:30pm on Sunday July 2nd, and during the conference. ACCOMMODATION: Liege offers a variety of hotels. Special rates have been negociated for attendees in the following hotels. All prices (per night) include breakfast, service and taxes. single double Holiday Inn**** 3.000 BEF 4.100 BEF Hotel Ibis** 2.150 BEF 2.500 BEF Hotel de l'Univers** 1.950 BEF 2.550 BEF Hotel Bedford*** 2.500 BEF 3.250 BEF The Holiday Inn is adjacent to the Conference Center and is the most convenient. The Hotel Ibis is located downtown (2.5 km from the Conference Center); it is modern and central. The Hotel de l'Univers is in front of the Guillemins railway station (2 km from the Congress Hall) it has been recently renovated. The Hotel Bedford is located along the Meuse river on the north side of the city (5 km from the Conference Center); its location is less convenient, but it is a new hotel and offers an excellent price/quality ratio. A limited number of rooms are being held for participants. Reservation will be handled on a first-come first-served basis. Early reservation is advisable. It is important to guarantee reservations with a credit card number to be indicated on the registration form. MEALS and SOCIAL PROGRAMME: A reception will be organised in the Hotel Holiday Inn (next to the Conference Center) on the evening of July 2nd from 7:30pm until 9:30pm. Lunches will be provided on the conference premises and a conference banquet will be organized on the evening of Tuesday July 4th. Liege offers a wide variety of restaurants. CLIMATE: The average weather in Belgium in July is quite pleasant (daytime temperatures around 20-25 degrees Celcius and reasonably low probability of rain). The range of possible weathers is however rather large: from cloudy and moderately cool with (or without) rain, through sunny and pleasant, to hot and humid. PROCEEDINGS: The conference proceedings will be published by Springer-Verlag in the LNCS series and will be available at the conference. PROGRAM COMMITTEE: P. Wolper, University of Liege (Chair); R. Alur, AT&T Bell Labs, USA R. Brayton, U. of California, Berkeley, USA; C. Courcoubetis, U. of Crete & ICS-FORTH, Greece; W. Damm, C. v. Ossietzki U., Oldenburg, Germany; R. de Simone, INRIA, Sophia-Antipolis, France; R. Devillers, Free U. of Brussels, Belgium; E. Allen Emerson, U. of Texas, USA; S. Garland, MIT, USA; O. Grumberg, Technion, Israel; N. Halbwachs, VERIMAG, France; T. Henzinger, Cornell U., USA; R. Koymans, Philips Res. Labs, The Netherlands; G. Leduc, U. of Liege, Belgium; K. McMillan, Cadence Berkeley Labs, USA; J. Parrow, SICS, Sweden; N. Shankar, SRI International, USA; F. Somenzi, U. of Colorado, Boulder, USA; B. Steffen, U. of Passau, Germany; P. Varaiya, U. of California, Berkeley, USA; M. Vardi, Rice U., USA; T. Yoneda, Tokyo Inst. of Technology, Japan. STEERING COMMITTEE: Edmund Clarke, Carnegie Mellon U., USA; Robert Kurshan, AT&T Bell Labs, USA; Amir Pnueli, Weizmannn Institute, Israel; Joseph Sifakis, VERIMAG, France. FURTHER INFORMATION: Through the WWW at http://www.montefiore.ulg.ac.be/cav95.html or by sending email to cav95@montefiore.ulg.ac.be". ---------------------------------------------------------------- REGISTRATION FEES The registration fees are the following (1 US$ = 29 BEF, 1 ECU = 37 BEF): Registration and Registration and payment received payment received by June 12 1995 after June 12 1995 Regular Registration* 9.500 BEF 11.000 BEF (July 3-5) Student Registration** 5.000 BEF 6.000 BEF (July 3-5) Additional Banquet 2.000 BEF 2.200 BEF Ticket *Includes proceedings, reception, lunches, coffee breaks and conference banquet. **Includes everything except the banquet. The conference fees may be paid by - Credit card (Visa or Master Card/Eurocard) - Eurocheque drawn in Belgian Francs - Bank transfer to Generale de Banque: account No 240-0435733-13 of AIM-CAV95 (be sure to clearly state your name and address) ====================================================================== REGISTRATION FORM AND PROCEDURE If you are paying by credit card or bank transfer, you may return the registration form by electronic mail or by fax. If you are paying by Eurocheque, you should return your registration form and cheque by physical mail. All CAV 95 registration correspondance should be sent to: A.I.M. CAV 95 Rue Saint Gilles, 31 B-4000 LIEGE 1 (Belgium) Phone: + 32 41 222.946 Fax: + 32 41 222.388 Email: cav95-registration@montefiore.ulg.ac.be Name: _____________________________________________________ Affiliation: ______________________________________________ Address: __________________________________________________ ___________________________________________________________ Country: __________________________________________________ Phone: _______________________ Fax: _______________________ (please include country and city code) Email: ____________________________________________________ Do you have any special dietary requirements? ____________ Item Price Amount Regular advanced registration: 9.500 BEF ______ BEF Late registration: 11.000 BEF ______ BEF Student registration: 5.000 BEF ______ BEF Late Student registration 6.000 BEF ______ BEF Extra banquet tickets 2.000 BEF each ______ BEF Late extra banquet tickets 2.200 BEF each ______ BEF TOTAL ______ BEF - Check enclosed [ ] - Payment by Bank transfer [ ] - Payment by Credit card [ ] VISA [ ] or Eurocard/MasterCard [ ]? Name of card holder ______________________ Card number _______________________________ Expiration date ______ daytime telephone _________________ ---------------------------------------------------------------------- HOTEL RESERVATION FORM Name: _____________________________________________________ Affiliation: ______________________________________________ Type of room(single/double):________ Number of nights: __________ Hotel choice (please number 1st choice 1, 2nd choice 2, ...): Holiday Inn**** ______ Hotel Ibis** ______ Hotel de l'Univers** ______ Hotel Bedford*** ______ Arrival date ___________ time __________ Departure date ___________ time __________ In order to guarantee your accommodation, please indicate the references of your credit card: Eurocard/Master Card [ ] VISA [ ] American Express [ ] Name of card holder _______________________ Card number _______________________________ Expiration date ______ daytime telephone _________________ ====================================================================== PROGRAM This is a preliminary version of the program. Changes might have to be made. Sunday July 2nd REGISTRATION: 19:00 - 20:30 Hotel Holiday Inn RECEPTION: 19:30 - 21:30 Salle des quatre Saisons, Hotel Holiday Inn. ---------------------------------------------------------------------- Monday July 3rd Palais des Congres - Salle Rogier REGISTRATION: 8:30 - 17:30 Session 1: 9:00 - 10:00 Chair: K. McMillan Invited Talk: R. Bryant, Carnegie-Mellon University. "Multipliers and Dividers: Insights on Arithmetic Circuit Verification" BREAK 10:00 - 10:30 Session 2: 10:30 - 12:30 Chair: F. Somenzi 10:30 - 11:00 "Global REbuilding of OBDD's - Tunnelling Memory Requirement Maxima" Jochen Bern, Christoph Meinel and Anna Slobodova, FB IV Informatik, Univ. Trier 11:00 - 11:30 "Generating BDD models for process algebra terms" Ashvin Dsouza and Bard Bloom, Dept. of Computer Science, Cornell U. 11:30 - 12:00 "Hardware Verification using Monadic Second-Order Logic" David A. Basin, Max-Planck-Instituet fuer Informatik, and Nils Klarlund, BRICS, Univ. of AArhus 12:00 - 12:30 "Verifying Safety Properties of a Class of Infinite-State Distributed Algorithms". Bengt Jonsson and Lars Kempe, Uppsala Univ. LUNCH: 12:30 - 14:00 Session 3: 14:00 - 15:30 Chair: O. Grumberg 14:00 - 14:30 "Model checking for infinite state systems using data abstraction, assumption-commitment style reasoning and theorem proving" Juergen Dingel, Carnegie Mellon Univ., and Thomas Filkorn, Siemens AG 14:30 - 15:00 "CAVEAT : technique and tool for Computer Aided VErification and Transformation" E. Pascal Gribomont and Didier Rossetto, Univ. of Liege 15:00 - 15:30 "An Integration of Model-Checking with Automated Proof Checking" S. Rajan, N. Shankar and M.K. Srivas, SRI International BREAK: 15:30 - 16:00 Session 4: 16:00 - 17:30 Chair: N. Halbwachs 16:00 - 16:30 "Automatic Datapath Abstraction in Hardware Systems" Ramin Hojati and Robert K. Brayton, Berkeley 16:30 - 17:00 "Toupie = mu-calculus + constraints" Antoine Rauzy, LABRI, Univ. Bordeaux I. 17:00 - 17:30 "Safety Property Verification of Esterel Programs and Applications to Telecommunications Software" Lalita Jategaonkar Jagadeesan, AT&T Bell Laboratories, Carlos Puchol, Univ. of Texas at Austin and James E. Von Olnhausen, AT&T Bell Laboratories END OF DAY ---------------------------------------------------------------------- Tuesday July 4th Palais des Congres - Salle Rogier REGISTRATION: 8:30 - 18:00 Session 1: 9:00 - 10:00 Chair: M. Vardi Invited Tutorial: E. Allen Emerson, University of Texas, Austin "Methods for Mu-calculus Model Checking" BREAK 10:00 - 10:30 Session 2: 10:30 - 12:30 Chair: C. Courcoubetis 10:30 - 11:00 "Efficient checking of behavioural relations and modal assertions using fixed-point inversion" Henrik Reif Andersen, Techn. Univ. of Denmark, and Bart Vergauwen, KUL 11:00 - 11:30 "It Usually Works: The Temporal Logic of Stochastic Systems" Adnan Aziz, Vigyan Singhal, Felice Balarin, Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli, Berkeley 11:30 - 12:00 "Local liveness for compositional modeling of fair reactive systems" Rajeev Alur, AT&T Bell Lab. and Thomas A. Henzinger, Cornell U. 12:00 - 12:30 "Trace theoretic verification of asynchronous circuits using unfoldings" K. L. McMillan, Cadence Design Systems LUNCH: 12:30 - 14:00 Session 3: 14:00 - 15:30 Chair: R. Alur 14:00 - 14:30 "From Duration Calculus to Linear Hybrid Automata" Ahmed Bouadjjani, VERIMAG, Yassine Lakhnech, U. Kiel, and Riadh Robbana, VERIMAG 14:30 - 15:00 "Local Model Checking for Real-Time Systems" Oleg V. Sokolsky and Scott A. Smolka, SUNY at Stony Brook 15:00 - 15:30 "Algorithmic Analysis of Nonlinear Hybrid Systems" Thomas A. Henzinger and Pei-Hsin Ho, Cornell Univ. BREAK: 15:30 - 16:00 Session 4: 16:00 - 18:30 Chair: A. Pnueli 16:00 - 16:30 "On polynomial-size programs winning finite-state games" Helmut Lescow, Christian-Albrechts-Universitaet Kiel 16:30 - 17:00 "The Rabin Index and Chain automata, with applications to automata and games" Sriram C. Krishnan, Anuj Puri, Robert K. Brayton, and Pravin P. Varaiya, Berkeley 17:00 - 17:30 "An Automata-Theoretic Approach to Fair Realizability and Synthesis" Moshe Y. Vardi, Rice Univ. 17:30 - 18:00 "Supervisory Control of Finite State Machines" A. Aziz, Dpt. of EECS, U. of California, Berkeley F. Balarin, Cadence Berkeley Labs M. D. DiBenedetto, Univ. di Roma "La Sapienza" R. Brayton, Dpt. of EECS, U. of California, Berkeley A. Saldanha, Cadence Berkeley Labs A. Sangiovanni-Vincentelli, Dpt. of EECS, U. of California, Berkeley 19:30 DEPARTURE FOR BANQUET (by bus) ---------------------------------------------------------------------- Wednesday July 5th Palais des Congres - Salle Rogier REGISTRATION: 8:30 - 17:30 Session 1: 9:00 - 10:00 Chair: J. Sifakis Invited Talk: P. Cousot, Ecole Normale Superieure, Paris. "Compositional and Inductive Semantic Definitions in Fixpoint, Equational, Constraint, Closure-condition, Rule-based and Game-Theoretic Form" BREAK 10:00 - 10:30 Session 2: 10:30 - 12:30 Chair: Ed Clarke 10:30 - 11:00 "Utilizing symmetry when model checking under fairness assumptions: an automata-theoretic approach" E. A. Emerson, Univ. of Texas at Austin, and A. P. Sistla, Univ. of Illinois at Chicago 11:00 - 11:30 "Augmenting branching temporal logics with existential quantification over atomic propositions" Orna Kupferman (Bernholtz), Dept. of Computer Science, the Technion, Haifa 11:30 - 12:00 "Modelling Asynchrony with a Synchronous Model" R.P. Kurshan, M. Merritt, AT&T Bell Labs, A. Orda, The Technion, S.R. Sachs, Berkeley. 12:00 - 12:30 "On the model checking problem for branching time logics and Basic Parallel Processes" Astrid Kiehn and Javier Esparza, Technische Universitaet Muenchen LUNCH: 12:30 - 14:00 Session 3: 14:00 - 15:30 Chair: G. Leduc 14:00 - 14:30 "Using Formal Verification/Analysis Methods on the Critical Path in System Design: A Case Study" Asgeir Th. Eiriksson, Silicon Graphics Inc., and Ken L. McMillan, Cadence Berkeley Labs. 14:30 - 15:00 "Automated analysis of an audio control protocol" Pei-Hsin Ho and Howard Wong-Toi, Cornell Univ. 15:00 - 15:30 "Interactively Verifying a Simple Real-time Scheduler" Colin Fidge, Peter Kearney and Mark Utting, Dept. of Computer Science University of Queensland BREAK: 15:30 - 16:00 Session 4: 16:00 - 17:30 Chair: T. Henzinger 16:00 - 16:30 "Verification of real-time systems by successive over and under approximation" David Dill, Stanford Univ. and Howard Wong-Toi, Cornell Univ. 16:30 - 17:00 "Efficient Timing Analysis of a Class of Petri Nets" Henrik Hulgaard and Steven M. Burns, Univ. of Washington, Seattle 17:00 - 17:30 "Verifying omega-Regular Properties for Subclasses of Linear Hybrid Systems" Ahmed Bouajjani and Riadh Robbana, VERIMAG END OF CONFERENCE