Automatic Verification Methods for Finite State Systems 1989: Grenoble, France

Process Algebras and Systems of Communicating Processes

• Gérard Boudol, Valérie Roy, Robert de Simone, Didier Vergamini:
  Process Calculi, from Theory to Practice: Verification Tools. 1-10
  
• Rance Cleaveland, Matthew Hennessy:
  Testing Equivalence as a Bisimulation Equivalence. 11-23
  
• Rance Cleaveland, Joachim Parrow, Bernhard Steffen:
  The Concurrency Workbench. 24-37
  
• Florence Maraninchi:
  Argonaute: Graphical Description, Semantics and Verification of Reactive Systems by Using a Process Algebra. 38-53
  
• Rocco De Nicola, Paola Inverardi, Monica Nesi:
  Using the Adxiomatic Presentation of Behavioural Equivalences for Manipulating CCS Specifications. 54-67
  
• Pierre Wolper, Vinciane Lovinfosse:
  Verifying Properties of Large Sets of Processes with Network Invariants. 68-80
  
• Ivan Christoff:
  A Method for Verification of Trace and Test Equivalence. 81-88
  
• Heiko Krumm:
  Projections of the Reachability Graph and Environment Models. 89-96
  
• Heikki Tuominen:
  Proving Properties of Elementary Net Systems with a Special-Purpose Theorem Prover. 97-104
  
• Han Zuidweg:
  Verification by Abstraction and Bisimulation. 105-116
  

Model Checking

• André Arnold:
  MEC: A System for Constructing and Analysing Transition Systems. 117-132
  
• Howard Barringer, Michael Fisher, Graham Gough:
  Fair SMG and Linear Time Model Checking. 133-150
  
• Ze'ev Shtadler, Orna Grumberg:
  Network Grammars, Communication Behaviors and Automatic Verification. 151-165
  
• Colin Stirling, David Walker:
  CCS, Liveness, and Local Model Checking in the Linear Time Mu-Calculus. 166-178
  
• Bengt Jonsson, Ahmed Hussain Khan, Joachim Parrow:
  Implementing a Model Checking Algorithm by Adapting Existing Automated Tools. 179-188
  
• Claude Jard, Thierry Jéron:
  On-Line Model Checking for Finite Linear Temporal Logic Specifications. 189-196
  

Timed Specifications

• David L. Dill:
  Timing Assumptions and Verification of Finite-State Concurrent Systems. 197-212
  
• Nicolas Halbwachs, Daniel Pilaud, Farid Ouabdesselam, A.-C. Glory:
  Specifying, Programming and Verifying Real-Time Systems Using a Synchronous Declarative Language. 213-231
  
• Kim Guldstrand Larsen:
  Modal Specifications. 232-246
  
• Jonathan S. Ostroff:
  Automated Verification of Timed Transition Models. 247-256
  
• William G. Wood:
  Temporal Logic Case Study. 257-263
  

Protocol Validation

• Sudhir Aggarwal, Daniel Barbará, Walter Cunto, M. R. Garey:
  The Complexity of Collapsing Reachability Graphs. 264-274
  
• Susanne Graf, Jean-Luc Richier, Carlos Rodriguez, Jacques Voiron:
  What are the Limits of Model Checking Methods for the Verification of Real Life Protocols? 275-285
  
• Pierre Azéma, François Vernadat, Jean Christophe Lloret:
  Requirement Analysis for Communication Protocols. 286-293
  
• Juan Quemada, Santiago Pavón, Angel Fernández:
  State Exploration by Transformation with LOLA. 294-302
  
• Maria C. Yuang, Aaron Kershenbaum:
  Parallel Protocol Verification: The Two-Phase Algorithm and Complexity Analysis. 303-316
  

Hardware Verification

• Alexandre Bronstein, Carolyn L. Talcott:
  Formal Verification of Synchronous Circuits based on String-Functional Semantics: The 7 Paillet Circuits in Boyer-Moore. 317-333
  
• Jerry R. Burch:
  Combining CTL, Trace Theory and Timing Models. 334-348
  
• Jørgen Staunstrup, Stephen J. Garland, John V. Guttag:
  Localized Verification of Circuit Descriptions. 349-364
  
• Olivier Coudert, Christian Berthet, Jean Christophe Madre:
  Verification of Synchronous Sequential Machines Based on Symbolic Execution. 365-373
  
• Ganesh Gopalakrishnan, Narayana Mani, Venkatesh Akella:
  Parallel Composition of Lockstep Synchronous Processes for Hardware Validation: Divide-and-Conquer Composition. 374-382
  

Last update Wed Feb 15 04:55:06 2012 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page