CAV'98 Advance Program

• Subject: CAV'98 Advance Program
• From: Alan Hu <ajh@cs.ubc.ca>
• Date: Sat, 18 Apr 1998 16:43:27 -0700 (PDT)

(Apologies in advance for the multiple copies you may receive.  This
was sent to multiple mailing lists with overlapping subscribers, so there
is no way to prevent that.  If you receive duplicate copies or an incorrectly
addressed copy emailed directly to you (not through another mail list),
please let me know, and I'll try to fix the problem.  --Alan Hu, ajh@cs.ubc.ca)

				ADVANCE PROGRAM
				    CAV'98
	    International Conference on Computer-Aided Verification
			     June 28 - July 2, 1998
	       University of British Columbia, Vancouver, Canada

This conference is the tenth 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
practical verification tools and the algorithms and techniques that are
needed for their implementation.

For information, registration, and accommodations, please see:
	http://www.cs.ubc.ca/conferences/CAV98/index.html

This schedule is tentative and may change.

Sunday, June 28, 1998

	9:00-10:30
	Tutorial Session 1:
	"Model Checking for Beginners:  A Tutorial Introduction to
		Finite-State Verification"
		Bob Kurshan (Bell Labs), Ken McMillan (Cadence Berkeley Labs)
	
	Break

	11:00-12:30
	Tutorial Session 2:
	Continuation of Tutorial Session 1

	Lunch

	2:00-3:30
	Tutorial Session 3:
	"Synchronous Programming of Reactive Systems"
		Nicolas Halbwachs (VERIMAG)

	Break

	4:00-5:30
	Tutorial Session 4:
	"Ten Years of Partial Order Reductions"
		Doron Peled (Bell Labs)

Monday, June 29, 1998

	8:30-10:00
	Invited Session 1A:  Industrial Application of Theorem Proving
	"Ongoing Commercial Applications of the ACL2 Theorem Prover"
		J Strother Moore (Univ. Texas Austin)
	"Transforming the Theorem Prover into a Digital Design Tool:
	 From Concept Car to Off-Road Vehicle"
		David Hardin, Matthew Wilding, David Greve (Rockwell Collins)
	"A Role for Theorem Proving in Multi-Processor Design"
		Albert Camilleri (Hewlett-Packard)
	
	Break

	10:30-12:00
	Invited Session 1B:  Industrial Application of Theorem Proving (cont'd)
	"A Formal Experience at Secure Computing Corporation"
		John Hoffman, Charlie Payne (Secure Computing)
	"Formal Methods in an Industrial Environment"
		Jorge Cuellar (Siemens)
	Discussion

	Lunch

	1:15-3:15
	Session 1C:  Microprocessor Verification
	"Formal Verification of Out-of-Order Execution Using
		Incremental Flushing"
		J. U. Skakkebaek, R. B. Jones, D. L. Dill
	"Verification of an Implementation of Tomasulo's Algorithm
		by Compositional Model Checking"
		K. L. McMillan
	"Decomposing the Proof of Correctness of Pipelined Microprocessors"
		R. Hosabettu, M. Srivas, G. Gopalakrishnan
	"Processor Verification with Precise Exceptions and
		Speculative Execution"
		J. Sawada, W. A. Hunt

	Break

	3:45-5:15
	Session 1D:  Combatting State Explosion
	"Symmetry Reductions in Model Checking"
		E. M. Clarke, E. A. Emerson, S. Jha, A. P. Sistla
	"Structural Symmetry and Model Checking"
		G. S. Manku, R. Hojati, R. K. Brayton
	"Using Magnetic Disk Instead of Main Memory in the
		Murphi Verifier"
		U. Stern, D. L. Dill

	Mini-Break

	5:30-6:10
	Session 1E:  Tool Presentations
	"XEVE, an Esterel Verification Environment"
		A. Bouali
	"InVeSt:  A tool for the Verification of Invariants"
		S. Bensalem, Y. Lakhnech, S. Owre

	6:15-7:30
	Demos and Hors d'Oeuvres

Tuesday, June 30, 1998

	8:30-9:45
	Session 2A:  Invited Speaker -- Gerard J. Holzmann (Bell Labs)
	"On Checking Model Checkers"

	Break

	10:15-11:45
	Session 2B:  Model Checking
	"On-the-Fly Model Checking of RCTL Formulas"
		I. Beer, S. Ben-David, A. Landver
	"From Pre-historic to Post-modern Symbolic Model Checking"
		T. A. Henzinger, O. Kupferman, S. Qadeer
	"Model Checking LTL Using Net Unfoldings"
		F. Wallner

	Lunch

	1:00-2:30
	Session 2C:  Decision Diagrams
	"Model Checking for a First-Order Temporal Logic Using
		Multiway Decision Graphs"
		Y. Xu, E. Cerny, X. Song, F. Corella, O. Ait Mohamed
	"On the Limitations of Ordered Representations of Functions"
		J. S. Thathachar
	"BDD Based Procedures for a Theory of Equality with
		Uninterpreted Functions"
		A. Goel, K. Sajid, H. Zhou, A. Aziz, V. Singhal

	Break

	3:00-5:00
	Session 2D:  Invited Tutorial -- Verification of Security Protocols
	"Finite State Analysis of Security Protocols"
		John. C. Mitchell
	"Integrating Proof-based and Model-checking Techniques for
		the Formal Verification of Cryptographic Protocols"
		Dominique Bolignano
	
	Mini-Break

	5:15-6:15
	Session 2E:  Tool Presentations
	"Verifying Mobile Processes in the HAL Environment"
		G. Ferrari, S. Gnesi, U. Montanari, M. Pistore, G. Ristori
	"MONA 1.x:  New Techniques for WS1S and WS2S"
		J. Elgaard, N. Klarlund, A. Moller
	"MOCHA:  Modularity in Model Checking"
		R. Alur, T. Henzinger, F. Mang, S. Qadeer,
		S. Rajamani, S. Tasiran

	6:15-7:30
	Demos and Hors d'Oeuvres

Wednesday, July 1, 1998

	8:30-9:45
	Session 3A:  Invited Speaker -- Pierre Wolper (University of Liege)
	"Verifying Systems with Infinite but Regular State Spaces"
		Pierre Wolper, Bernard Boigelot

	Break

	10:15-11:45
	Session 3B:  Extended Finite-State Machines
	"Computing Reachable Control States of Systems Modeled with
		Uninterpreted Functions and Infinite Memory"
		A. J. Isles, R. Hojati, R. K. Brayton
	"Multiple Counters Automata, Safety Analysis,
		and Presburger Arithmetic"
		H. Comon, Y. Jurski
	"A Comparison of Presburger Engines for EFSM Reachability"
		T. R. Shiple, J. H. Kukula, R. K. Ranjan

	Lunch

	1:00-3:00
	Session 3C:  Abstraction and Refinement
	"Generating Finite-State Abstractions of Reactive Systems Using
		Decision Procedures"
		M. A. Colon, T. E. Uribe
	"On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels"
		P. A. Abdulla, A. Bouajjani, B. Jonsson
	"Computing Abstractions of Infinite State Systems Compositionally
		and Automatically"
		S. Bensalem, Y. Lakhnech, S. Owre
	"Normed Simulations"
		D. Griffioen, F. Vaandrager

	Break

	3:30-5:00
	Session 3D:  Formal Methods and Software Systems
	"An Experiment in Parallelizing an Application Using Formal Methods"
		R. Couturier, D. Mery
	"Efficient Symbolic Detection of Global Properties in
		Distributed Systems"
		S. D. Stoller, Y. A. Liu
	"A Machine-Checked Proof of the Optimality of a Real-Time
		Scheduling Policy"
		M. Wilding

	Mini-Break

	5:10-5:50
	Session 3E:  Tool Presentations
	"The SCR Toolset for Specifying and Analyzing Software Requirements"
		C. Heitmeyer, J. Kirby, B. Labaw, R. Bharadwaj
	"A Toolset for Message Sequence Charts"
		D. Peled

	6:00-7:15
	Demos and Drinks

	7:30-?
	Salmon BBQ Banquet

Thursday, July 2, 1998

	8:30-9:45
	Session 4A:  Invited Speaker -- Carl Seger (Intel)
	"Combining Theorem Proving and Model Checking:  How Much
		Theorem Proving Is Needed?"

	Break

	10:15-11:45
	Session 4B:  Partial Order
	"A General Approach to Partial Order Reductions in
		Symbolic Verification"
		P. A. Abdulla, B. Jonsson, M. Kindahl, D. Peled
	"Correctness of the Concurrent Approach to Symbolic Verification
		of Interleaved Models"
		F. Balarin
	"Verification of Timed Systems Using POSETS"
		W. Belluomini, C. J. Myers

	Lunch

	1:00-3:00
	Session 4C:  Case Studies
	"Mechanising BAN Kerberos by the Inductive Method"
		G. Bella, L. C. Paulson
	"Protocol Verification in Nuprl"
		A. P. Felty, D. J. Howe, F. A. Stomp
	"You Assume, We Guarantee:  Methodology and Case Studies"
		T. A. Henzinger, S. Qadeer, S. K. Rajamani
	"Verification of a Parameterized Bus Arbitration Protocol"
		E. A. Emerson, K. S. Namjoshi

	Break

	3:30-5:00
	Session 4D:  Hardware Verification
	"The `Test Model-Checking' Approach to the Verification of
		Formal Memory Models of Multiprocessors"
		R. Nalumasu, R. Ghughal, A. Mokkedem, G. Gopalakrishnan
	"Design Constraints in Symbolic Model Checking"
		M. Kaufmann, A. Martin, C. Pixley
	"Verification of Floating-Point Adders"
		Y.-A. Chen, R. E. Bryant

	Mini-Break

	5:15-6:15
	Session 4E:  Tool Presentations
	"Real-Time Verification of STATEMATE Designs"
		U. Brockmeyer, G. Wittich
	"Optikron:  a tool suite for enhancing model-checking
		of real-time systems"
		C. Daws
	"Kronos:  a model-checking tool for real-time systems"
		M. Bozga, C. Daws, O. Maler, A. Olivero,
		S. Tripakis, S. Yovine

	6:15-7:30	Demos and Hors d'Oeuvres

	End of Conference

• Prev: CFP INAP98
• Next: FSTTCS 98, Second Call for Papers (ASCII)
• Index: AMAST Mail 1998