Fifth International Conference on

Tools and Algorithms for the Construction and Analysis of Systems

(TACAS '99)

20-28 March, 1999

Amsterdam, the Netherlands

A constituent of the 1999 European Joint Conferences on Theory and Practice of Software (ETAPS '99).

[ Description ] [ Submission Guidelines ] [ Organization ]

Conference Description

TACAS is a community-independent forum for researchers, developers and users interested in rigorously based tools for the construction and analysis of systems. The conference serves to bridge the gaps between different communities --- including but not limited to those devoted to formal methods, real-time, software engineering, communications protocols, hardware, theorem proving, and programming languages --- that have traditionally had little interaction but share common interests in and techniques for tool development. In particular, by providing a venue for the discussion of common problems, heuristics, algorithms, data structures and methodologies, TACAS supports tool builders in their quest to increase the utility, reliability, flexibility and efficiency of tools for building systems.

Topics covered are:

compositional verification and construction techniques;
refinement-based methodologies;
heterogeneous analysis;
theorem-proving and model checking;
analytical techniques for real-time, hybrid, probabilistic, and
safety-critical systems;
tool environments and tool architectures; and
applications and case studies.

Conference Organization

Program Committee Chair

Rance Cleaveland (co-chair)
Department of Computer Science
226 Withers Hall
North Carolina State University
Raleigh, NC 27695-8206, USA
+1 (919) 515-7862 (voice)
+1 (919) 515-7896 (fax)
rance csc ncsu edu

Steering Committee

Ed Brinksma (U. Twente)
Rance Cleaveland (N.C. State U.)
Kim G. Larsen (Aalborg U.)
Bernhard Steffen(U. Dortmund)

Program Committee

Rajeev Alur (U. Pennsylvania)
Ed Brinksma (U. Twente)
Rance Cleaveland (chair) (N.C. State U.)
Hubert Garavel (INRIA Rhône-Alpes)
Fausto Giuchiglia (U. Trento)
Mike Gordon (Cambridge U.)
Roberto Gorrieri (U. Bologna)
Jan Friso Groote (CWI)
Nicolas Halbwachs (Vérimag)
Gerard Holzmann (Bell Labs)
Kurt Jensen (Aarhus U.)
Kim G. Larsen (Aalborg U.)
Tiziana Margaria (U. Passau)
David Notkin (U. Washington)
Gregor Snelting (U. Braunschweig)

Programme

Monday March 22

8:45	Welcome
9:00	Invited tutorial Research challenges in renovation of legacy software P. Klint (CWI and Univ. Amsterdam), A. van Deursen (CWI, Amsterdam) and C. Verhoef (Univ. Amsterdam):
10.30	Coffee
11.00	P.-A. Hsiung, F. Wang, Y.-S. Kuo (Academia Sinica, Taiwan): Scheduling system verification M. Ryu, S. Hong (Seoul National University): A period assignment algorithm for real-time system design M. Gardner, J. Liu (Univ. Illinois at Urbana-Champaign): Analyzing stochastic fixed-priority real-time systems S. Tripakis (Verimag, Grenoble): Timed diagnostics for reachability properties
13.00	Lunch
14.30	Invited talk: Making Java easier to type, and easier to type G. Bracha (Sun Micro Systems, USA):
15.30	Coffee
16.00	Y. Dong, X. Du, Y. Ramakrishna, C. Ramakrishnan, I. Ramakrishnan, S. Smolka, O. Sokolsky, E. Stark, D. Warren (SUNY, Stony Brook): Fighting livelock in the i-protocol: A comparative study of verification tools C. Pusch (TU Munich): Proving the soundness of a Java bytecode verifier specification in Isabelle/HOL C. Kreitz (Cornell University): Automated fast-track reconfiguration of group communication systems J. Hickey (Cornell University), N. Lynch (MIT), R. van Renesse (Cornell University): Specifications and proofs for ensemble layers
Evening	Reception

Tuesday March 23

9:00	Invited Talk: Functional reactive programming P. Hudak (Yale University)
10:00	Coffee
10:30	A. Bergeron, J. Manzoni (Univ. Quebec): An automated analysis of ping-pong interactions D. Marchignoli (Univ. Pisa), F. Martinelli (Univ. Siena): Automatic verification of cryptographic protocols through compositional analysis techniques G. Behrmann, K. Larsen (Aalborg University), H. Andersen, H. Hulgaard, J. Lind-Nielsen (Danish Technical University): Verification of hierarchical state/event systems using reusability and compositionality V. Rusu, E. Singerman (SRI International, Menlo Park): On proving safety properties by integrating static analysis, theorem proving and abstraction
12:30	Lunch
14:00	A. Biere, A. Cimatti, E. Clarke, Y. Zhu (Carnegie-Mellon University): Symbolic model checking without BDDs P. Abdulla (Uppsala University), A. Annichni, A. Bouajjani (Verimag, Grenoble): Symbolic verification of lossy channel systems: Application to the bounded retransmission protocol G. Delzanno, A. Podelski (Max-Planck-Institut, Saarbrücken): Model checking in CLP K. Heljanko (Helsinki Univ. of Technology): Using logic programs with stable model semantics to solve deadlock and reachability problems for 1-safe Petri nets
16:00	Coffee
16:15- 18:00	Panel discussion The PITAC Reportcts
Evening	ETAPS Banquet

Wednesday March 24

9:00	Invited Talk: Security protocols and specifications M. Abadi (Compaq Systems Research Center, Palo Alto)
10:00	Coffee
10:30	V. Braun, J. Kreileder, T. Margaria, B. Steffen (Univ. Dortmund), tool demo: The ETI online service in action Panel discussion (B. Steffen, Univ. Dortmund, moderator): Software engineering and the verification tool builder
12:30	Lunch
14:30	Invited Talk Continuous engineering of information and communication infrastructure H. Weber (TU Berlin)
15:30	Coffee
1600- 18:00	U. Montanari, M. Pistore (Univ. Pisa): Finite state verification for the asynchronous pi-calculus T. Basten, J. Hooman (Eindhoven Univ. of Technology): Process algebra in PVS D. Hirschkoff (CERMICS-ENPC, INRIA): On the benefits of using the up to techniques for bisimulation verification Z. Li, H. Chen (Changsha Institute of Technology): Computing strong/weak bisimulation equivalences and observation congruence for value-passing processes
19:30	CWI Soiree

Rance Cleaveland (rance csc ncsu edu)