FMICS 2008: L'Aquila, Italy

Invited Presentations

• Steven P. Miller:
  Formal Methods for Critical Systems. 1
  
• Rance Cleaveland:
  Model-Based Verification of Automotive Control Software. 2
  
• Werner Damm:
  Contract-Based Analysis of Automotive and Avionics Applications: The SPEEDS Approach. 3
  

Panel

• Alessandro Fantechi, Alessio Ferrari:
  Panel Discussion on Formal Methods in Commercial Software Development Tools. 4-6
  

Research Papers

• Guy Durrieu, Hélène Waeselynck, Virginie Wiels:
  LETO - A Lustre-Based Test Oracle for Airbus Critical Systems. 7-22
  
• Virginia Papailiopoulou, Laya Madani, Lydie du Bousquet, Ioannis Parissis:
  Extending Structural Test Coverage Criteria for Lustre Programs with Multi-clock Operators. 23-36
  
• Radek Pelánek:
  Fighting State Space Explosion: Review and Evaluation. 37-52
  
• Jiri Barnat, Lubos Brim, Ivana Cerná, Milan Ceska, Jana Tumova:
  Local Quantitative LTL Model Checking. 53-68
  
• José Vander Meulen, Charles Pecheur:
  Efficient Symbolic Model Checking for Process Algebras. 69-84
  
• Bernard van Gastel, Leonard Lensink, Sjaak Smetsers, Marko C. J. D. van Eekelen:
  Reentrant Readers-Writers: A Case Study Combining Model Checking with Theorem Proving. 85-102
  
• Samuel Colin, Arnaud Lanoix, Olga Kouchnarenko, Jeanine Souquières:
  Using CSP||B Components: Application to a Platoon of Vehicles. 103-118
  
• Xiayong Hu, Mark Lawford, Alan Wassyng:
  Formal Verification of the Implementability of Timing Requirements. 119-134
  
• Christian Colombo, Gordon J. Pace, Gerardo Schneider:
  Dynamic Event-Based Runtime Monitoring of Real-Time and Contextual Properties. 135-149
  
• Jiri Barnat, Lubos Brim, Stefan Edelkamp, Damian Sulewski, Pavel Simecek:
  Can Flash Memory Help in Model Checking? 150-165
  
• Alessandro Cimatti, Marco Roveri, Angelo Susi, Stefano Tonetta:
  From Informal Requirements to Property-Driven Formal Validation. 166-181
  
• Mauricio Alba-Castro, María Alpuente, Santiago Escobar:
  Automated Certification of Non-Interference in Rewriting Logic. 182-198
  
• Erzsébet Németh, Tamás Bartha:
  Formal Verification of Safety Functions by Reinterpretation of Functional Block Based Specifications. 199-214
  
• María Alpuente, Marco A. Feliú, Christophe Joubert, Alicia Villanueva:
  Using Datalog and Boolean Equation Systems for Program Analysis. 215-231