[Prev][Next][Index][Thread]
TACAS '99 Accepted Papers
Below, please find the list of papers that have been accepted for prese=ntation
at the 1999 Conference on Tools and Algorithms for the Construction and
Analysis of Systems (TACAS '99). TACAS '99 is a constituent of the European
Joint Symposia on Theory and Practice of Software (ETAPS '99), to be held in
Amsterdam.
For more information on the conference, please consult its URL:
http://www.csc.ncsu.edu/tacas99.
Rance Cleaveland
TACAS '99 PC Chair
-------------------------
TACAS '99 ACCEPTED PAPERS
-------------------------
Modular State Level Analysis of Distributed Systems - Techniques and
Tool Support
Peter Buchholz, Peter Kemper
Informatik IV
University of Dortmund
Germany
DYANA: An Environment for Embedded System Design and Analysis
R.L. Smeliansky, A.G. Bakhmurov, A.P. Kapitonova
Dept. of Computational Mathematics and Cybernetics
Moscow State University
Russia
Using Logic Programs with Stable Model Semantics to Solve Deadlock and
Reachability Problems for 1-Safe Petri Nets
Keijo Heljanko
Laboratory for Theoretical Computer Science
Helsinki University of Technology
Finland
On Proving Safety Properties by Integrating Static Analysis, Theorem
Proving and Abstraction
Vlad Rusu, Eli Singerman
Computer Science Laboratory
SRI International
USA
Path Exploration Tool
Elsa L. Gunter, Doron Peled
Bell Laboratories
USA
Scheduling System Verification
Pao-Ann Hsiung, Farn Wang, Yue-Sun Kuo
Institute of Information Science
Academia Sinica
Taiwan, R.O.C.
A Period Assignment Algorithm for Real-Time System Design
Minsoo Ryu, Seongsoo Hong
School of Electrical Engineering and ERC-ACI
Seoul National University
Korea
Process Algebra in PVS
Twan Basten, Jozef Hooman
Dept. of Computing Science
Eindhoven University of Technology
The Netherlands
A theorem prover-based analysis tool for object-oriented databases
David Spelt, Susan Even
Center for Telematics and Information Technology
University of Twente
The Netherlands
Automated Fast-Track Reconfiguration of Group Communication Systems
Christoph Kreitz
Dept. of Computer Science
Cornell University
USA
Proving the Soundness of a Java Bytecode Verifier Specification in
Isabelle/HOL
Cornelia Pusch
Institute fuer Informatik
Technische Universitaet Muenchen
Germany
Symbolic Model Checking without BDDs
Armin Biere, Alessandro Cimatti, Edmund Clarke, Yunshan Zhu
Computer Science Dept.
Carnegie-Mellon University
USA
On the Benefits of Using the Up To Techniques for Bisimulation
Verification
Daniel Hirschkoff
CERMICS-ENPC
INRIA
France
Specifications and Proofs for Ensemble Layers
Jason Hickey (1), Nancy Lynch (2), Robbert van Renesse (1)
(1) Dept. of Computer Science
Cornell University
USA
(2) Laboratory for Computer Science
Massachusetts Institute of Technology
USA
Ping-Pong Interactions in E-mail Services
A. Bergeron, J.C. Manzoni
LACIM
Universite' du Que'bec a` Montre'al
Canada
Hardware testing using a communication protocol conformance testing
tool
César Viho (1), Hakim Kahlouche (2) , Massimo Zendri (3)
(1) IRISA/IFSIC
University de Rennes I
France
(2) INRIA, Campus de Beaulieu
France
(3) Bull R&D
Italy
Automatic verification of cryptographic protocols through
compositional analysis techniques
Davide Marchignoli (1), Fabio Martinelli (2)
(1) Dipartimento di Informatica
Universita di Pisa
Italy
(2) Dipartimento di Matematica
Universita di Pisa
Italy
An Easily Extensible Toolset for Tabular Mathematical Expressions
Dennis K. Peters (1,2), David Lorge Parnas (2)
(1) Faculty of Engineering and Applied Sciences
Memorial University of Newfoundland
Canada
(2) Department of Computing and Software
McMaster University
Canada
A Light-Weight Framework for Hardware Verification
Christoph Kern, Tarik Ono-Tesfaye, Mark R. Greenstreet
Dept. of Computer Science
University of British Columbia
Canada
>From DFA-Frameworks to DFA-Generators: A Unifying Multiparadigm
Approach
Jens Knoop
University of Dortmund
Germany
Verification of Hierarchical State/Event Systems using Reusability and
Compositionality
Gerd Behrmann (1), Kim G. Larsen (1), Henrik R. Andersen (2),
Henrik Hulgaard (2), Jorn Lind-Nielsen (2)
(1) BRICS
Aarhus University
Denmark
(2) Department of Information Technology
Danish Technical University
Denmark
Timed Diagnostics for Reachability Properties
Stavros TRIPAKIS
Verimag
France
Analyzing Stochastic Fixed-Priority Real-Time Systems
Mark K. Gardner, Jane W.S. Liu
Department of Computer Science
University of Illinois at Urbana-Champaign
USA
Fighting Livelock in the i-Protocol: A Comparative Study of
Verification Tools
Yifei Dong, Xiaoqun Du, Y.S. Ramakrishna, C.R. Ramakrishnan, I.V.
Ramakrishnan, Scott A. Smolka, Oleg Sokolsky, Eugene W. Stark, David
S. Warren
Dept. of Computer Science
SUNY at Stony Brook
USA
Symbolic Verification of Lossy Channel Systems: Application to the
Bounded Retransmission Protocol
Parosh Abdulla (1), Aurore Annichni (2), Ahmed Bouajjani (2)
(1) Dept. of Computer Systems
Uppsala University
Sweden
(2) Verimag
France
Finite State Verification for the Asynchronous pi-Calculus
Ugo Montanari, Marco Pistore
Computer Science Department
University of Pisa
Italy
Computing Strong/Weak Bisimulation Equivalences and Observation
Congruence for Value-Passing Processes
Zhoujun Li, Huowang Chen
Dept. of Computer Science
Changsha Institute of Technology
China
Model Checking in CLP
Giorgio Delzanno, Andreas Podelski
Max-Planck-Institut fuer Informatik
Germany
--
Rance Cleaveland (rance@cs.sunysb.edu)
Tel: (516) 632-8448 (voice), (516) 632-8334 (fax)
WWW: http://www.cs.sunysb.edu/~rance
Post: Dept. of Comp. Sci., SUNY at Stony Brook, Stony Brook, NY 11794-4400