From owner-theorynt@LISTSERV.NODAK.EDU Wed Apr 23 14:44:49 1997 Received: from CS.Stanford.EDU (CS.Stanford.EDU [171.64.64.64]) by robotics.Stanford.EDU (8.8.5/8.8.5) with ESMTP id OAA00584 for ; Wed, 23 Apr 1997 14:44:49 -0700 (PDT) Received: from listserv.nodak.edu (listserv.NoDak.edu [134.129.111.8]) by CS.Stanford.EDU (8.8.4/8.8.4) with ESMTP id OAA15139; Wed, 23 Apr 1997 14:33:53 -0700 (PDT) Received: from listserv (134.129.111.8) by listserv.nodak.edu (LSMTP for Windows NT v1.1a) with SMTP id <0.6E322CF0@listserv.nodak.edu>; Wed, 23 Apr 1997 16:21:42 -0500 Received: from LISTSERV.NODAK.EDU by LISTSERV.NODAK.EDU (LISTSERV-TCP/IP release 1.8c) with spool id 789617 for THEORYNT@LISTSERV.NODAK.EDU; Wed, 23 Apr 1997 16:21:39 -0500 Received: from listserv (134.129.111.8) by listserv.nodak.edu (LSMTP for Windows NT v1.1a) with SMTP id <0.6BC17B10@listserv.nodak.edu>; Wed, 23 Apr 1997 16:21:38 -0500 Received: from LISTSERV.NODAK.EDU by LISTSERV.NODAK.EDU (LISTSERV-TCP/IP release 1.8c) with spool id 789608 for THEORY-A@LISTSERV.NODAK.EDU; Wed, 23 Apr 1997 16:21:38 -0500 Received: from pollux.usc.edu by listserv.nodak.edu (LSMTP for Windows NT v1.1a) with SMTP id <0.6281ED50@listserv.nodak.edu>; Wed, 23 Apr 1997 16:21:23 -0500 Received: (from ierardi@localhost) by pollux.usc.edu (8.8.4/8.8.4/usc) id NAA16467 for theory-a@listserv.nodak.edu; Wed, 23 Apr 1997 13:57:46 -0700 (PDT) Approved-By: Doug Ierardi Approved-By: Theory-A - TheoryNet World-Wide Events Message-ID: <199704170721.KAA01407@CS.Technion.AC.IL> Date: Wed, 23 Apr 1997 13:57:45 PDT Reply-To: Theory-A - TheoryNet World-Wide Events , cav97@csa.CS.Technion.AC.IL Sender: TheoryNet List Comments: cc: cav97@CS.Technion.AC.IL From: cav97@csa.CS.Technion.AC.IL Subject: CAV'97 Final program Comments: To: THEORY-A@LISTSERV.NODAK.EDU To: THEORYNT@LISTSERV.NODAK.EDU X-Mozilla-Status: 0001 Content-Length: 17932 ********************************************************************* COMPUTER - AIDED VERIFICATION (CAV 97) June 22-25, 1997 Dan Carmel Hotel Haifa, Israel FINAL PROGRAM and REGISTRATION, ACCOMMODATION and TOUR RESERVATION ********************************************************************* CAV '97 is the ninth in a series dedicated to the advancement of the theory and practice of computer-assisted formal analysis methods for software and hardware systems. The conference covers the spectrum from theoretical results to concrete applications, with an emphasis on verification tools and the algorithms and techniques that are needed for their implementation. The contributed presentations of CAV '97 include 34 regular papers and 12 short presentations on tools. The program also includes 3 invited lectures and a dinner speech in honor of the recipient of the Turing award, Professor Amir Pnueli. Half a day is dedicated to invited talks by representatives from industry. The industrial part concludes with a panel on "Future Trends in Industrial Computer-Aided Verification". The conference will be opened on Saturday night, June 21, 1997 with a get together reception at the Dan Carmel Hotel. The technical program will start on Sunday morning and will proceed until Wednesday, June 25, late afternoon. For updated information see the CAV'97 home page at: http://www.cs.technion.ac.il/~cav97/cav97.html CONFERENCE PROGRAM ------------------ This is a preliminary version of the program. Changes may be made. Saturday 21.6.97 ---------------- 18:00 - 21:00 Registration 21:00 - 23:00 Reception Sunday 22.6.97 ---------------- 09:00 - 09:30 FE Marschner, Practical challenges for industrial COMPASS Design formal verification tools Automation 09:30 - 10:00 RB Hughes, Formal verification of digital systems, from Abstract Hardware ASICs to HW/SW codesign - a pragmatic approach 10:00 - 10:30 A Boralv, The Industrial Success of Verification Tools Logikkonsult NP Based on Stalmarck's Method 10:30 - 11:00 Coffee Break 11:00 - 11:30 M Rowe, Formal Verification - Applications Chrysalis Symbolic & Case Studies Design 11:30 - 12:45 Panel on "Future Trends in Industrial Computer-Aided Verification" EA Emerson, UT at Austin - moderator, B Brennan, Intel, T Henzinger, UC Berkeley, RP Kurshan, Bell Labs, C Logan, IBM, N Shankar, SRI, Y Wolfstal, IBM 12:45 - 14:00 Lunch 14:00 - 14:25 A Pardo, Automatic abstraction techniques for GD Hachtel, propositional mu-calculus model checking Uni. Colorado 14:25 - 14:50 KL McMillan, A compositional rule for hardware design Cadence Berkeley Labs. refinement 14:50 - 15:15 O Kupferman, UC Berkeley MY Vardi, Rice Uni. Module checking revisited 15:15 - 15:40 R Kaivola, Using compositional preorders in the Uni. Helsinki verification of sliding window protocol 15:40 - 16:05 Coffee Break 16:05 - 16:30 D Cyrluk, SRI Internat. An efficient decision procedure for the theory O Moller, H Reuss, of fixed-sized bit-vectors Uni. Ulm 16:30 - 16:55 S Graf, H Saidi Construction of abstract state graphs with Verimag PVS 16:55 - 17:10 H Saidi, Verimag The Invariant Checker: Automated deductive verification of reactive systems 17:10 - 17:25 B Grahlmann The PEP tool Hildesheim Uni. ------------------------------- Monday 23.6.97 -------------- 08:30 - 09:30 Invited Lecture GJ Powers, CMU Verification of a chemical process leak test procedure 09:30 - 09:55 G Kamhi, O Weissberg, Automatic datapath extraction for efficient L Fix, Z Binyamini, usage of HDD Z Shtadler, Intel 09:55 - 10:20 N Klarlund, AT&T Labs. An n log n algorithm for online BDD refinement 10:20 - 10:45 Coffee Break 10:45 - 11:10 C Baier, Uni Mannheim Weak bisimulation for fully probabilistic H Hermanns, processes Uni Erlangen 11:10 - 11:35 D Bolignano Towards a mechanization of cryptographic GIE, Dyade protocol verification 11:35 - 12:00 YS Ramakrishna, Efficient model checking using tabled CR Ramakrishnan, resolution IV Ramakrishnan, SA Smolka, T Swift, DS Warren, SUNY Brook 12:00 - 12:15 N Lindenstrauss, TermiLog: A system for checking termination Y Sagiv, A Serebrenik, of queries to logic programs Hebrew Uni 12:15 - 12:30 P Kelb, T Margaria, MOSEL: A sound and efficient tool for M2L(Str) M Mendler, C Gsottberger, Passau Uni. 12:30 - 14:00 Lunch 14:00 - 14:25 K Fisler, Rice Uni. Containment of regular languages in non-regular timing diagram languages is decidable 14:25 - 14:50 B Boigelot, L Bronne, An improved reachability analysis method for S Rassart, Uni. Liege strongly linear hybrid systems 14:50 - 15:15 M Bozga, O Maler, Some progress in the symbolic verification S Yovine, Verimag of timed automata A Pnueli, Weizmann Inst. 15:15 - 15:40 S Tasiran, RK Brayton, STARI: A case study in compositional and UC Berkeley hierarchical timing verification 15:40 - 16:05 Coffee Break 16:05 - 16:30 A Cimatti, A provably correct embedded verifier for the F Giunchiglia, certification of safety critical software P Pecchiari, IRST, B Pietra, J Profeta, D Romano, Ansalso Trasporti Spa, P Traverso, IRST B Yu, Ansalso Trasporti Spa, 16:30 - 16:55 G Barrett, A McIssac, Model checking in a microprocessor design SGS-Thomson project Microelectronics 16:55 - 17:10 S Campos, E Clarke, The Verus Tool: A quantitative approach to M Minea, CMU the formal verification of real-time systems 17:10 - 17:25 KG Larsen, Aalborg Uni. UPPAAL - Status & developments P Pettersson, W Yi, Uppsala Uni. 17:25 - 17:40 TA Henzinger, HYTECH: A model checker for hybrid systems UC Berkeley, P-H Ho, Intel, H Wong-Toi, Cadence Berkeley Labs. ----------------------------- Tuesday 24.6.97 --------------- 08:30 - 09:30 Invited Lecture D Harel, Weizmann Inst. Some thoughts on statecharts, 13 years later 09:30 - 09:55 V Gyuris, AP Sistla, On-the-fly model checking under fairness that Uni. Illinois at exploits symmetry Chicago 09:55 - 10:20 M Pandey, RE Bryant, Exploiting symmetry when verifying transistor- CMU level circuits by symbolic trajectory evaluation 10:20 - 10:45 Coffee Break 10:45 : 11:10 U Stern, DL Dill, Parallelizing the Murphi verifier Stanford Uni. 11:10 - 11:35 RH Hardin, RP Kurshan, A new heuristic for bad cycle detection Bell Labs., using BDDs SK Shukla, Uni. NY, MY Vardi, Rice Uni. 11:35 - 12:00 I Beer, S Ben-David, Efficient detection of vacuity in ACTL C Eisner, Y Rodeh, IBM formulas 12:00 - 12:25 N Immerman, Model checking and transitive closure logic Uni Massachusetts MY Vardi, Rice Uni. 12:25 - 12:40 AP Sistla, L Miliades, SMC: A symmetry based model checker for V Gyuris, Uni. verification of liveness properties Illinois at Chicago 12:40 - 12:55 A Biere, mucke - efficient mu-calculus model checking Uni Karlsruhe 12:55 - 14:15 Lunch 14:30 - Excursion and Banquet Dinner speech in honor of Amir Pnueli, the Turing Award recipient, by David Harel, Amir Pnueli: A Man for all (the Right) Reasons Weizmann Inst. ------------------------------- Wednesday 25.6.97 ----------------- 08:30 - 09:30 Invited Lecture G Berry, Ecole de Boolean and 2-adic numbers based techniques Mines de Paris for verifying synchronous designs 09:30 - 09:55 G Cece, A Finkel, Programs with quasi-stable channels are LSV, ENS effectively recognizable 09:55 - 10:20 W Chan, R Anderson, Combining constraint solving and symbolic P Beame, D Notkin, model checking for a class of systems with Uni. Washington non-linear constraints 10:20 - 10:45 Coffee Break 10:45 - 11:10 I Kokkarinen, Relaxed visibility enhances partial order Tampere Uni, reduction D Peled, Bell Labs., A Valmari, Tampere Uni. 11:10 - 11:35 R Alur, RK Brayton, Partial order reduction in symbolic state TA Henzinger, space exploration S Qadeer, SK Rajamani, UC Berkeley 11:35 - 12:00 S Melzer, S. Roemer, Deadlock checking using net unfoldings Technical Uni. Munich 12:00 - 12:15 K Varpaaniemi, prod 3.2 - An advanced tool for efficient K Heljanko, J Lilius reachability analysis Helsinki Uni. 12:15 - 12:30 P Godefroid, VeriSoft: A tool for the automatic analysis of Bell Labs. concurrent reactive software 12:30 - 14:00 Lunch 14:00 - 14:25 J Sawada, Uni Texas, Trace table based approach for pipelined WA Hunt, microprocessor verification Computational Logic Inc. 14:25 - 14:50 J Yuan, Motorola Inc. On combining formal and informal verification J Shen, J Abraham, A Aziz, Uni. Texas 14:50 - 15:15 M Velev, RE Bryant, Efficient modeling of memory arrays in A Jain, CMU symbolic simulation 15:15 - 15:30 I Beer, S Ben-David, RuleBase: Model checking at IBM C Eisner, D Geist, L Gluhovsky, T Heyman, A Landver, P Paanah, Y Rodeh, G Ronin, Y Wolfstahl, IBM 15:30 - 15:55 Coffee Break 15:55 - 16:20 T Bultan, R Gerber, Symbolic model checking of infinite state W Pugh, Uni. Maryland systems using Presburger arithmetic 16:20 - 16:45 AP Sistla, Parametrized verification of linear Uni. Illinois at networks using automata as invariants Chicago 16:45 - 17:10 Y Kesten, Intel Symbolic model checking with rich O Maler, Verimag assertional languages M Marcus, A Pnueli, E Shahar, Weizmann Inst. ------------------------- LOCATION: - -------- The conference will take place in the Dan Carmel Hotel, Haifa, Israel. GETTING THERE: - -------------- You will arrive at the Ben-Gurion International Airport which is situated near Tel-Aviv. As you leave the terminal building you will see a taxi stand with the sign "AMAL". You may share a taxi with about six other people and this will cost approximately $15. The driver will take you to your hotel. This trip may take approximately one and a half hours. If you wish to take a taxi by yourself, it may cost between $50-$60. Special transportation from Ben Gurion Airport to your hotel can be reserved on the attached Registration & Reservation Form. Participants will be met upon arrival and assisted through baggage claim and customs. Price per person: $ 57. WEATHER: - -------- The weather in Haifa in June is sunny and warm. Temperatures range between 19C - 26C (69F - 78F). Humidity is moderate and there is no rain. Light clothing, informal dress and swimming suit are recommended. VISA: - ---- Please note that citizens of most countries require a visa to enter Israel. Please make your arrangements early. CURRENCY: - --------- Israel's currency is the New Israeli Shekel (NIS). The average exchange rate (as of March 7, 1997) is 1 US dollar = 3.37 NIS. TOURS: -------- `Unitours' is the official travel agent for CAV 97 and will be offering reduced rates especially for conference participants. They will extend their services for special hotel arrangements, tours and car rentals as well as pre- and post- conference requests. Pre- and Post- Conference Tours: ---------------------------------- * Tour A - Acre, Safed, Golan Heights, one day tour, June 21 Price per person: $ 58 * Tour B - Jerusalem 2 days/2 nights, June 26-28 Day 1: Caesarea, Tel Aviv, Jaffa. Dinner and Overnight: Jerusalem Day 2: Jerusalem Old and New. Dinner and Overnight: Jerusalem Day 3: Check out of hotel or departure for tour C. Prices: Per person in a double room: $ 258. Single room: $ 339 Rates include: 2 days of guided tours, 2 nights accommodation on breakfast and dinner basis in a first class hotel in Jerusalem * Tour C - Massada and Dead Sea, 1 day/1 night, June 28-29 Day 1: Tour of Massada and Dead Sea. Dinner and Overnight: Jerusalem Day 2: Check out of hotel Prices: Per person in a double room: $ 113. Single room: $ 159. All tours will operate with a minimum of 15 participants. ********************************************************************* CAV'97 - REGISTRATION and ACCOMMODATION ********************************************************************* Dear Participant!! Below are the Registration and Accommodation Forms for CAV '97. Please fill out the forms in BLOCK LETTERS and return them by e-mail or by airmail to: The Secretariat - CAV 97 P.O. Box 3190, Tel Aviv 61031, Israel Tel: 972-3-5209999 Fax: 972-3-5239099 E-mail: cav97@unitours.co.il - ----------------------------CUT HERE ----------------------------- ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ CONFERENCE REGISTRATION FORM CAV '97 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ PARTICIPANTS: Name : ........................................................ (Surname) (First Name) Title: ....................................................... Institution: .................................................. Mailing Address: [ ]Institution [ ]Residence ................ ............................................................... City: ................ State: .....................Country: .................. Zip Code: ............ e-mail:........................... Telephone: ....................... Fax: ............................. ACCOMPANYING PERSONS: .................................................... (Surname) (First Name) .................................................... (Surname) (First Name) REGISTRATION FEE: (in US Dollars) till may 21, 1997 after May 22, 1997 [ ] Participant 350 390 [ ] Student 130 150 [ ] Accompanying Person 120 120 Fees for participants include: reception, lunches and coffee breaks, banquet and book of proceedings. Fees for students include: reception, coffee breaks and book of proceedings. Fees for accompanying persons include: all social events as listed above and a one day tour. +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ ACCOMMODATION FORM CAV '97 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Name : ........................................................ (Surname) (First Name) Mailing Address: .............................................. ............................................................... City ................. Code ............. Country ............. Telephone ..................... Fax ........................... Please reserve my hotel accommodation: Single occupancy Double occupancy Dan Carmel* [ ] US$ 118 [ ] US$ 146 sharing with ........... Shulamit ** [ ] US$ 61 [ ] US$ 76 sharing with ............ The above prices are per night. The prices include: an Israeli buffet breakfast and service charges. * Conference venue ** The hotel is located 15 min. drive from the conference venue. The number of rooms is limited. Rooms are on a first come first serve basis. Check in on ................. Check out on ................... No. of nights ................ Must be accompanied by a deposit of US$ 150 per room. ---------------------------------------------------------- CANCELATION POLICY OF ACCOMMODATION Notification must be: Postmarked 45 days or more prior to arrival - refund of deposit less US$ 30 bank charges. Postmarked 45 days or less prior to arrival - refund of deposit less one night accommodation. CANCELATION POLICY OF REGISTRATION Postmarked 21 days prior to conference: refund less US$ 30 bank charges. Thereafter - no refund will be made. ----------------------------------------- TOURS - Please reserve the following tour/s: (must be accompanied by a deposit of US$ 58 per tour, per person) Tour A (Galilee) No. of Seats_____ Tour B (Jerusalem) No. of Seats_____ Tour C (Massada) No. of Seats_____ TRANSFER Please reserve a sharing transfer airport/hotel at US$ 57 per person. No. of seats _________ PAYMENT - ------- I enclose herewith payment of US$_________________ as follows: US$ ______________________ for registration US$ ______________________ for hotel/tours/transfer MODE OF PAYMENT (1) I enclose herewith US$_______________(or equivalent) payable to: CAV/UNITOURS. Check No. ________________________Bank_______________ (2) Enclosed is a copy of my bank transfer of US$_______________ payable to CAV/UNITOURS, Acc. No. 893/403575/60 Bank Leumi Le Israel, Trumpeldor Branch (807), Tel Aviv, Israel (3) Credit Card Payment: Please charge the amount of US$____________________to my credit card: [ ] American Express [ ] Visa [ ] Master Card [ ] Diners Club Credit card number___________________________Expiration date_________ Signature____________________________ Date____________________