ICFEM 2007 Programme

Florida Atlantic University

777 Glades Road, Boca Raton, Florida 33431-0991 USA

(PDF version)

Day 1.  Wednesday November 14, 2007                                                 

08:30 – 9:30 Registration

09:30 – 10:30 Invited Talk: Jean-Raymond Abrial

         A System Development Process with Event-B and the Rodin Platform

10:30 – 11:00 Break

11:00 – 12:30 Security and Knowledge  

Integrating formal methods with system management.

Martin de Groot.

Formal Engineering of XACML Access Control Policies in VDM++.

Jeremy Bryans and John Fitzgerald.

A Verification Framework for Agent Knowledge.

Jin Song Dong, Yuzhang Feng and Ho-fung Leung.

12:30 – 14:00 Lunch

14:00 – 15:30 Embedded Systems

From Model-Based Design to Formal Verification of Adaptive Embedded Systems.

Rasmus Adler, Ina Schaefer, Tobias Schuele and Eric Vecchié.

Machine-Assisted Proof Support for Validation beyond Simulink.

Chunqing Chen, Jin Song Dong and Jun Sun.

VeSTA: a Tool to Verify the Correct Integration of a Component in a Composite Timed System.

Jacques Julliand, Mountassir Hassan and Emilie Oudot.

15:30 – 16:00 Break

16:00 – 17:30 Testing

Integrating Specification-Based Review and Testing for Detecting Errors in Programs.

Shaoying Liu.

Testing for Refinement in CSP.

Ana Cavalcanti and Marie-Claude Gaudel.

Reducing Test Sequence Length Using Invertible Sequences.

Lihua Duan and Jessica Chen.

18:30 – 19:30  Reception

Day 2.  Thursday November 15, 2007                                                    

09:00 – 10:00 Invited Talk: Tom Maibaum

         Challenges  in Software Certification

10:30 – 11:00 Break

10:30 – 12:30 Automated Analysis

Model Checking with SAT-Based Characterization of ACTL Formulas.

Wenhui Zhang.

Automating refinement checking in probabilistic system design.

Carlos Gonzalia and Annabelle McIver.

Model Checking in Practice: Analysis of Generic Bootloader Using SPIN.

Kuntal Das Barman and Debapriyay Mukhopadhyay.

Model Checking Propositional Projection Temporal Logic Based on SPIN.  

Cong Tian and Zhenhua Duan.

12:30 – 14:00 Lunch

14:00 – 15:30 Hardware

A denotational semantics for Handel-C hardware compilation.

Juan Perna and Jim Woodcock.

Automatic Generation of Verified Concurrent Hardware.

Marcel Oliveira and Jim Woodcock.

Modeling and Verification of Master/Slave Clock Synchronization using Hybrid Automata and Model-checking.

Guillermo Rodriguez-Navas, Julián Proenza and Hans Hansson.

15:30 – 16:00 Break

16:00 – 17:30 Concurrency

Efficient Symbolic Execution of Large Quantifications in a Process Algebra.

Benoit Fraikin and Marc Frappier.

Formalizing SANE Virtual Processors in thread algebra.

Duong Vu and Chris Jesshope.

Calculating and composing progress properties in terms of the leads-to relation.

Arjan Mooij.