FMSP 2000: Portland, Oregon, USA

• David L. Dill:
  Model checking Java programs. 1
  
• Willem Visser, Seungjoon Park, John Penix:
  Using predicate abstraction to reduce object-oriented programs for model checking. 3-182
  
• Robert J. Hall:
  Specification, validation, and synthesis of email agent controllers: A case study in function rich reactive system design. 13-23
  
• Myla Archer, Constance L. Heitmeyer, Elvinia Riccobene:
  Using TAME to prove invariants of automata models: Two case studies. 25-36
  
• W. B. Martin, P. D. White, W. Mark Vanfleet:
  Government, industry, and academia: Teaming to design high confidence information security applications. 37-47
  
• Cindy Kong, Perry Alexander, Darryl D. Dieckman:
  Formal modeling of active network nodes using PVS. 49-59
  
• Karthikeyan Bhargavan, Carl A. Gunter, Davor Obradovic:
  Fault origin adjudication. 61-71
  
• Douglas R. Smith:
  Software synthesis and applications (abstract only). 73
  
• Nancy G. Leveson:
  Completeness in formal specification language design for process-control systems. 75-87
  
• Ernst-Rüdiger Olderog, Anders P. Ravn:
  Completeness in formal specification language design for process-control systems. 89-100
  
• Nils Klarlund, Anders Møller, Michael I. Schwartzbach:
  DSD: A schema language for XML. 101-111