Formal Methods in System Design, Volume 30

Volume 30, Number 1, February 2007

• Constance L. Heitmeyer, Jean-Pierre Talpin:
  Guest editorial. 1-3
  
• Edmund M. Clarke, Himanshu Jain, Daniel Kroening:
  Verification of SpecC using predicate abstraction. 5-28
  
• Cagkan Erbas, Andy D. Pimentel, Selin Cerav-Erbas:
  Static priority scheduling of event-triggered real-time embedded systems. 29-47
  
• Cagkan Erbas, Andy D. Pimentel, Selin Cerav-Erbas:
  Static priority scheduling of event-triggered real-time embedded systems. 49
  
• Tobias Schüle, Klaus Schneider:
  Bounded model checking of infinite state systems. 51-81
  

Volume 30, Number 2, April 2007

• Haiyan Xiong, Paul Curzon, Sofiène Tahar, Ann Blandford:
  Providing a formal linkage between MDG and HOL. 83-116
  
• L. Feng, W. Murray Wonham, P. S. Thiagarajan:
  Designing communicating transaction processes by supervisory control theory. 117-141
  
• Victor Khomenko, Maciej Koutny:
  Verification of bounded Petri nets using integer programming. 143-176
  

Volume 30, Number 3, June 2007

• Andrew Butterfield, Juan Bicarregui, Alvaro Arenas:
  Foreword: Selected papers from the ninth international workshop on formal methods for industrial critical systems (FMICS 04), Linz, Austria. 177-178
  
• Martin Fränzle, Christian Herde:
  HySAT: An efficient proof engine for bounded model checking of hybrid systems. 179-198
  
• Yunja Choi:
  From NuSMV to SPIN: Experiences with model checking flight guidance systems. 199-216
  
• Akram Idani, Yves Ledru:
  Object oriented concepts identification from formal B specifications. 217-232
  
• Christophe Ponsard, Philippe Massonet, Jean-François Molderez, André Rifaut, Axel van Lamsweerde, Hung Tran Van:
  Early verification and validation of mission critical systems. 233-247
  
• Miguel Valero Espada, Jaco van de Pol:
  An abstract interpretation toolkit for µCRL. 249-273