4. TACAS 1998: Lisbon, Portugal (Part of ETAPS 1998)

Bernhard Steffen (Ed.): Tools and Algorithms for Construction and Analysis of Systems, 4th International Conference, TACAS '98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings. Lecture Notes in Computer Science 1384 Springer 1998, ISBN 3-540-64356-7

Invited Lecture

Randal E. Bryant:
Formal Verification of Pipelined Processors. 1-4

1. Model Checking

Xinxin Liu, C. R. Ramakrishnan, Scott A. Smolka:
Fully Local and Efficient Evaluation of Alternating Fixed Points (Extended Abstract). 5-19
Karen Laster, Orna Grumberg:
Modular Model Checking of Software. 20-35
Michaela Huhn, Peter Niebert, Frank Wallner:
Verification Based on Local States. 36-51
Khalil Ajami, Serge Haddad, Jean-Michel Ilié:
Exploiting Symmetry in Linear Time Temporal Logic Model Checking: One Step Beyond. 52-67

2. Design and Architecture

Hubert Garavel:
OPEN/CÆSAR: An OPen Software Architecture for Verification, Simulation, and Testing. 68-84
Perdita Stevens, Colin Stirling:
Practical Model-Checking Using Games. 85-101
Bernd Grahlmann:
Combining Finite Automata, Parallel Programs and SDL Using Petri Nets. 102-117
Hanêne Ben-Abdallah, Stefan Leue:
MESA: Support for Scenario-Based Design of Concurrent Systems. 118-135

Various Applications

Miroslav N. Velev, Randal E. Bryant:
Efficient Modeling of Memory Arrays in Symbolic Ternary Simulation. 136-150
Amir Pnueli, Michael Siegel, Eli Singerman:
Translation Validation. 151-166
Christoph Sprenger:
A Verified Model Checker for the Modal µ-calculus in Coq. 167-183
Alexander Aiken, Manuel Fähndrich, Zhendong Su:
Detecting Races in Relay Ladder Logic Programs. 184-200

4. Fielded Applications

Jørn Lind-Nielsen, Henrik Reif Andersen, Gerd Behrmann, Henrik Hulgaard, Kåre J. Kristoffersen, Kim Guldstrand Larsen:
Verification of Large State/Event Systems Using Compositionality and Dependency Analysis. 201-216
Udo Brockmeyer, Gunnar Wittich:
Tamagotchis Need Not Die - Verification of STATEMENT Design. 217-231
Thierry Cattel:
Modeling and Verification of SC++ Applications. 232-248
David James Sherman, Nicolas Magnier:
Factotum: Automatic and Systematic Sharing Support for Systems Analyzers. 249-262

5. Verification of Real-Time Systems

Luca Aceto, Augusto Burgueño, Kim Guldstrand Larsen:
Model Checking via Reachability Testing for Timed Automata. 263-280
Magnus Lindahl, Paul Pettersson, Wang Yi:
Formal Design and Analysis of a Gear Controller. 281-297
Parosh Aziz Abdulla, Bengt Jonsson:
Verifying Networks of Timed Processes (Extended Abstract). 298-312
Conrado Daws, Stavros Tripakis:
Model Checking of Real-Time Reachability Properties Using Abstractions. 313-329

6. Mixed Analysis Techniques

Rajeev Alur, Thomas A. Henzinger, Sriram K. Rajamani:
Symbolic Exploration of transition Hierarchies. 330-344
Robert P. Kurshan, Vladimir Levin, Marius Minea, Doron Peled, Hüsnü Yenigün:
Static Partial Order Reduction. 345-357
Witold Charatonik, Andreas Podelski:
Set-Based Analysis of Reactive Infinite-State Systems. 358-375
Nikolaj Bjørner, Mark C. Pichora:
Deiding Fixed and Non-fixed Size Bit-vectors. 376-392

7. Case Studies and Experience

Theo C. Ruys, Ed Brinksma:
Experience with Literate Programming in the Modelling and Validation of Systems. 393-408
Henrik Ejersbo Jensen, Nancy A. Lynch:
A Proof of Burns N-Process Mutual Exclusion Algorithm Using Abstraction. 409-423
E. Pascal Gribomont, Guy Zenner:
Automated Verification of Szymanski's Algorithm. 424-438
Franz Regensburger, Aenne Barnard:
Formal Verification of SDL Systems at the Siemens Mobile Phone Department. 439-455

Last update Thu May 23 18:02:35 2013 CET by the DBLP Team —

Data released under the ODC-BY 1.0 license — See also our legal information page