From Model Checking to a Temporal Proof

ions Using SPIN . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 Marsha Chechik, Benet Devereux, Arie Gurfinkel (University of Toronto) Implementing LTL Model Checking with Net Unfoldings . . . . . . . . . . . . . . . . 37 Javier Esparza (Technische Universit¨at M¨unchen), Keijo Heljanko (Helsinki University of Technology) Directed Explicit Model Checking with HSF-SPIN . . . . . . . . . . . . . . . . . . . . . 57 Stefan Edelkamp, Alberto Lluch Lafuente, Stefan Leue (Albert-Ludwigs-Universit¨at) Addressing Dynamic Issues of Program Model Checking . . . . . . . . . . . . . . . . 80 Flavio Lerda, Willem Visser (NASA Ames Research Center) Automatically Validating Temporal Safety Properties of Interfaces . . . . . . . 103 Thomas Ball, Sriram K. Rajamani (Microsoft Research) Verification Experiments on the MASCARA Protocol . . . . . . . . . . . . . . . . . . 123 Guoping Jia, Susanne Graf (VERIMAG) Using SPIN for Feature Interaction Analysis – A ...

• Type: Conference
• Year: 2001
• Where: SPIN
• Authors: Doron Peled, Lenore D. Zuck
• Keywords: Ions Using Spin, Model Checking, Program Model Checking, SPIN 2001, Theoretical Computer Science