6. TACAS 2000: Berlin, Germany (Part of ETAPS 2000)

@proceedings{DBLP:conf/tacas/2000,
  editor    = {Susanne Graf and
               Michael I. Schwartzbach},
  title     = {Tools and Algorithms for Construction and Analysis of Systems,
               6th International Conference, TACAS 2000, Held as Part of the
               European Joint Conferences on the Theory and Practice of Software,
               ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000, Proceedings},
  booktitle = {TACAS},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1785},
  year      = {2000},
  isbn      = {3-540-67282-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Invited Contribution

• Pierre Wolper, Bernard Boigelot:
  On the Construction of Automata from Linear Arithmetic Constraints. 1-19
  

Software and Formal Methods Tools

• Yuhong Xiong, Edward A. Lee:
  An Extensible Type System for Component-Based Design. 20-37
  
• David Aspinall:
  Proof General: A Generic Tool for Proof Development. 38-42
  
• Michael Goedicke, Bettina Enders, Torsten Meyer, Gabriele Taentzer:
  ViewPoint-Oriented Software Development: Tool Support for Integrating Multiple Perspectives by Distributed Graph Transformation. 43-47
  

Formal Methods Tools

• Peter Braun, Heiko Lötzbeyer, Bernhard Schätz, Oscar Slotosch:
  Consistent Integration of Formal Methods. 48-62
  
• Jörg Meyer, Arnd Poetzsch-Heffter:
  An Architecture for Interactive Program Provers. 63-77
  
• Louise A. Dennis, Graham Collins, Michael Norrish, Richard J. Boulton, Konrad Slind, Graham Robinson, Michael J. C. Gordon, Thomas F. Melham:
  The PROSPER Toolkit. 78-92
  
• Till Mossakowski:
  CASL: From Semantics to Tools. 93-108
  

Timed and Hybrid Systems

• Sébastien Bornot, Gregor Gößler, Joseph Sifakis:
  On the Construction of Live Timed Systems. 109-126
  
• Fredrik Larsson, Paul Pettersson, Wang Yi:
  On Memory-Block Traversal Problems in Model-Checking Timed-Systems. 127-141
  
• Thomas A. Henzinger, Rupak Majumdar:
  Symbolic Model Checking for Rectangular Hybrid Systems. 142-156
  
• Farn Wang:
  Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems. 157-171
  

Infinite and Parameterized Systems

• Abhik Roychoudhury, K. Narayan Kumar, C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka:
  Verification of Parameterized Systems Using Logic Program Transformations. 172-187
  
• Kai Baukus, Saddek Bensalem, Yassine Lakhnech, Karsten Stahl:
  Abstracting WS1S Systems to Verify Parameterized Networks. 188-203
  
• Jean-Paul Bodeveix, Mamoun Filali:
  FMona: A Tool for Expressing Validation Techniques over Infinite State Systems. 204-219
  
• Bengt Jonsson, Marcus Nilsson:
  Transitive Closures of Regular Relations for Verifying Infinite-State Systems. 220-234
  

Diagnostic and Test Generation

• Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu:
  Using Static Analysis to Improve Automatic Test Generation. 235-250
  
• Radu Mateescu:
  Efficient Diagnostic Generation for Boolean Equation Systems. 251-265
  

Efficient Model-Checking

• Jean-Pierre Krimm, Laurent Mounier:
  Compositional State Space Generation with Partial Order Reductions for Asynchronous Communicating Systems. 266-282
  
• Juhana Helovuo, Antti Valmari:
  Checking for CFFD-Preorder with Tester Processes. 283-298
  
• Thomas A. Henzinger, Sriram K. Rajamani:
  Fair Bisimulation. 299-314
  
• Karsten Schmidt:
  Integrating Low Level Symmetries into Reachability Analysis. 315-330
  

Model-Checking Tools

• Giuseppe Del Castillo, Kirsten Winter:
  Model Checking Support for the ASM High-Level Language. 331-346
  
• Holger Hermanns, Joost-Pieter Katoen, Joachim Meyer-Kayser, Markus Siegle:
  A Markov Chain Model Checker. 347-362
  
• Dragan Bosnacki, Dennis Dams, Leszek Holenderski, Natalia Sidorova:
  Model Checking SDL with Spin. 363-377
  
• Ramesh Bharadwaj, Steve Sims:
  Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking. 378-394
  

Symbolic Model-Checking

• Luca de Alfaro, Marta Z. Kwiatkowska, Gethin Norman, David Parker, Roberto Segala:
  Symbolic Model Checking of Probabilistic Processes Using MTBDDs and the Kronecker Representation. 395-410
  
• Parosh Aziz Abdulla, Per Bjesse, Niklas Eén:
  Symbolic Reachability Analysis Based on SAT-Solvers. 411-425
  
• Giorgio Delzanno, Jean-François Raskin:
  Symbolic Representation of Upward-Closed Sets. 426-440
  
• Tevfik Bultan:
  BDD vs. Constraint-Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent Systems. 441-455
  

Visual Tools

• Magnus Niemann, Roswitha Bardohl:
  Tool-Based Specification of Visual Languages and Graphic Editors. 456-470
  
• Moataz Kamel, Stefan Leue:
  VIP: A Visual Editor and Compiler for v-Promela. 471-486
  

Verification of Critical Systems

• Tamarah Arons, Amir Pnueli:
  A Comparison of Two Verification Methods for Speculative Instruction Execution. 487-502
  
• Edmund M. Clarke, Somesh Jha, Wilfredo R. Marrero:
  Partial Order Reductions for Security Protocol Verification. 503-518
  
• Massimo Benerecetti, Fausto Giunchiglia:
  Model Checking Security Protocols Using a Logic of Belief. 519-534
  
• Stefania Gnesi, Diego Latella, Gabriele Lenzini, C. Abbaneo, Arturo M. Amendola, P. Marmo:
  A Formal Specification and Validation of a Critical System in Presence of Byzantine Errors. 535-549