Electronic Notes in Theoretical Computer Science, Volume 55

Volume 55, Number 1, 2001

• Jean Goubault-Larrecq:
  Preface.
  
• Roberto M. Amadio:
  On the symbolic reduction of processes with cryptographic functions.
  
• Michaël Rusinowitch:
  The practice of cryptographic protocol verification.
  
• Rafael Accorsi, David A. Basin, Luca Viganò:
  Towards an awareness-based semantics for security protocol analysis.
  
• Kamel Adi, Mourad Debbabi:
  Abstract interpretation for proving secrecy properties in security protocols.
  
• Luigia Carlucci Aiello, Fabio Massacci:
  Attacking fair-exchange protocols: parallel models vs trace models.
  
• Peter Selinger:
  Models for an adversary-centric protocol logic.
  
• Ramaswamy Ramanujam, S. P. Suresh:
  Information based reasoning about security protocols.
  

Volume 55, Number 2, 2001

• Klaus Havelund, Grigore Rosu:
  Preface.
  
• Detlef Bartetzko, Clemens Fischer, Michael Möller, Heike Wehrheim:
  Jass - Java with Assertions.
  
• Mireille Ducassé, Erwan Jahier:
  Efficient Automated Trace Analysis: Examples with Morphine.
  
• Surrendra Dudani, Joao Geada, Grzegorz Jakacki, Daniel Vainer:
  Dynamic Assertions Using TXP.
  
• Bernd Finkbeiner, Henny Sipma:
  Checking Finite Traces using Alternating Automata.
  
• Ann Q. Gates, Steve Roach, Oscar Mondragon, Nelly Delgado:
  DynaMICs: Comprehensive Support for Run-Time Monitoring.
  
• Marc Geilen:
  On the Construction of Monitors for Temporal Logic Properties.
  
• Klaus Havelund, Grigore Rosu:
  Monitoring Java Programs with Java PathExplorer.
  
• Moonjoo Kim, Sampath Kannan, Insup Lee, Oleg Sokolsky, Mahesh Viswanathan:
  Java-MaC: a Run-time Assurance Tool for Java Programs.
  
• David Kortenkamp, Tod Milam, Reid G. Simmons, Joaquín Lopez Fernández:
  Collecting and Analyzing Data from Distributed Control Programs.
  
• Jeremy W. Nimmer, Michael D. Ernst:
  Static verification of dynamically detected program invariants: Integrating Daikon and ESC/Java.
  
• Stavros Tripakis, Sergio Yovine:
  Timing Analysis and Code Generation of Vehicle Control Software using Taxys.
  

Volume 55, Number 3, 2001

• Scott D. Stoller, Willem Visser:
  Preface.
  
• Cindy Eisner:
  Model checking the garbage collection mechanism of SMV.
  
• Frank Huch:
  Model checking Erlang programs - abstracting the context-free structure.
  
• Sarfraz Khurshid, Darko Marinov:
  Checking Java implementation of a naming architecture using Testera.
  
• Stefan Edelkamp, Alberto Lluch-Lafuente, Stefan Leue:
  Trail-directed model checking.
  
• Timm Schäfer, Alexander Knapp, Stephan Merz:
  Model checking UML state machines and collaborations.
  
• Marius Bozga, Susanne Graf, Laurent Mounier:
  Automated validation of distributed software using the IF environment.
  
• Kirsten Winter:
  Model checking with abstract types.