5. TACAS 1999: Amsterdam, The Netherlands (Part of ETAPS 1999)

Invited Contribution

• Jeff Kramer, Jeff Magee:
  Modelling for Mere Mortals. 1-18
  

Real-Time

• Pao-Ann Hsiung, Farn Wang, Yue-Sun Kuo:
  Scheduling System Verification. 19-33
  
• Minsoo Ryu, Seongsoo Hong:
  A Period Assignment Algorithm for Real-Time System Design. 34-43
  
• Mark K. Gardner, Jane W.-S. Liu:
  Analyzing Stochastic Fixed-Priority Real-Time Systems. 44-58
  
• Stavros Tripakis:
  Timed Diagnostics for Reachability Properties. 59-73
  

Case Studies

• Yifei Dong, Xiaoqun Du, Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka, Oleg Sokolsky, Eugene W. Stark, David Scott Warren:
  Fighting Livelock in the i-Protocol: A Comparative Study of Verification Tools. 74-88
  
• Cornelia Pusch:
  Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL. 89-103
  
• Christoph Kreitz:
  Automated Fast-Track Reconfiguration of Group Communication Systems. 104-118
  
• Jason Hickey, Nancy A. Lynch, Robbert van Renesse:
  Specifications and Proofs for Ensemble Layers. 119-133
  

Compositionality and Abstraction

• Anne Bergeron, Jean-Christophe Manzoni:
  An Automated Analysis of Ping-Pong Interactions in E-mail Services. 134-147
  
• Davide Marchignoli, Fabio Martinelli:
  Automatic Verification of Cryptographic Protocols through Compositional Analysis Techniques. 148-162
  
• Gerd Behrmann, Kim Guldstrand Larsen, Henrik Reif Andersen, Henrik Hulgaard, Jørn Lind-Nielsen:
  Verification of Hierarchical State/Event Systems Using Reusability and Compositionality. 163-177
  
• Vlad Rusu, Eli Singerman:
  On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction. 178-192
  

Symbolic Analysis

• Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Yunshan Zhu:
  Symbolic Model Checking without BDDs. 193-207
  
• Parosh Aziz Abdulla, Aurore Annichini, Ahmed Bouajjani:
  Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol. 208-222
  
• Giorgio Delzanno, Andreas Podelski:
  Model Checking in CLP. 223-239
  
• Keijo Heljanko:
  Using Logic Programs with Stable Model Semantics to Solve Deadlock and Reachability Problems for 1-Safe Petri Nets. 240-254
  

Process Algebra

• Ugo Montanari, Marco Pistore:
  Finite State Verification for the Asynchronous pi-Calculus. 255-269
  
• Twan Basten, Jozef Hooman:
  Process Algebra in PVS. 270-284
  
• Daniel Hirschkoff:
  On the Benefits of Using the Up-To Techniques for Bisimulation Verification. 285-299
  
• Zhoujun Li, Huowang Chen:
  Computing Strong/Weak Bisimulation Equivalences and Observation Congruence for Value-Passing Processes. 300-314
  

Frameworks for System Construction and Analysis

• Hakim Kahlouche, César Viho, Massimo Zendri:
  Hardware Testing Using a Communication Protocol Conformance Testing Tool. 315-329
  
• Christoph Kern, Tarik Ono-Tesfaye, Mark R. Greenstreet:
  A Light-Weight Framework for Hardware Verification. 330-344
  
• David Lorge Parnas, Dennis K. Peters:
  An Easily Extensible Toolset for Tabular Mathematical Expressions. 345-359
  
• Jens Knoop:
  From DFA-Frameworks to DFA-Generators: A Unifying Multiparadigm Approach. 360-374
  

Tool Descriptions

• David Spelt, Susan Even:
  A Theorem Prover-Based Analysis Tool for Object-Oriented Databases. 375-389
  
• Anatoly G. Bakhmurov, A. P. Kapitonova, Ruslan L. Smeliansky:
  DYANA: An Environment for Embedded System Design and Analysis. 390-404
  
• Elsa L. Gunter, Doron Peled:
  Path Exploration Tool. 405-419
  
• Peter Buchholz, Peter Kemper:
  Modular State Level Analysis of Distributed Systems Techniques and Tool Support. 420-434
  
• Perdita Stevens:
  Some Issues in the Software Engineering of Verification Tools. 435-438
  
• Volker Braun, Jürgen Kreileder, Tiziana Margaria, Bernhard Steffen:
  The ETI Online Service in Action. 439-443
  

Last update Tue May 21 18:07:01 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page