[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