Software Engineering and Formal Methods

Tutorials

Tutorial 1: John Rushby, A Tutorial Introduction to Modern Formal Methods

1. 09:00 - 10:30: Lecture
2. 10:30 - 11:00: Coffee Break
3. 11:00 - 12:30: Lecture
4. 12:30 - 14:00: Lunch
5. 14:00 - 16:00: Lecture

Tutorial 2: Joseph Sifakis, Component-based Construction of Heterogeneous Real-time Systems in BIP

1. 09:00 - 10:30: Lecture
2. 10:30 - 11:00: Coffee Break
3. 11:00 - 12:30: Lecture
4. 12:30 - 14:00: Lunch
5. 14:00 - 18:00: Social Event (visit Temple of Literature and Fine-Art Museum)(Free)

Conference

8:00 - 8:45: Registration

8:45 - 9:00: Opening

9:00 - 10:00: Keynote 1:

Chair: Antonio Cerone

Joseph Sifakis, Embedded Systems Design - Scientific Challenges and Work Directions

10:00 - 10:30: Coffee Break

10:30 - 12:00:  Session 1: Real-Time Systems,

Chair: Manuel Nunez

1. Marcello Bersani, Carlo Alberto Furia, Matteo Pradella and Matteo Rossi. Integrated Modeling and Verification of Real-Time Systems through Multiple Paradigms
2. Matthias Daum, Norbert Schirmer and Mareike Schmidt. Implementation Correctness of a Real-Time Operating System
3. Christian Colombo, Gordon Pace and Gerardo Schneider. LARVA -- Safer Monitoring of Real-Time Java Programs

12:00 - 13:30: Lunch Break

13:30 - 15:00: Session 2: Distributed Systems,

Chair: Gerardo Schneider

1. Rob Hierons and Manuel Nunez. Simulation relations for systems with distributed interfaces
2. Jonathan Ezekiel and Alessio Lomuscio. An automated approach to verifying diagnosability in multi-agent systems
3. Prakash Chandrasekaran and Madhavan Mukund. Specifying Interacting Components with Coordinated Concurrent Scenarios

15:00 - 15:30: Coffee Break

15:30 - 17:00: Session 3: Testing/Valdiation,

Chair: Madhavan Mukund

1. Cesar Andres, Mercedes Merayo and Manuel Nunez. Formal passive testing of timed systems: A case study with the Stream Control Transmission Protocol
2. Bertrand Jeannet. Relational interprocedural verification of concurrent programs
3. Mahadevan Subramaniam, Bo Guo and Zoltan Pap. Using Change Impact Analysis to Select Tests for Extended Finite State Machines

17:00 - 17:10: Presentation of SEFM 2010

19:00 - 20:30: Reception at Press Club, 59A Ly Thai To Str., Hoang Kiem Dist.

9:00 - 10:00 Keynote 2:

Chair: Paddy Krishnan

Bernd-Holger Schlingloff, Advances in Model-Based Testing

10:00 - 10:30: Coffee Break

10:30 - 12:00: Session 4: Model Checking,

Chair: Jean-Yves Marion

1. Do Thi Bich Ngoc and Ogawa Mizuhito. Roundoff and Overflow Error Analysis via Model Checking
2. Cristiano Bertolini and Alexandre Mota. Using Probabilistic Model Checking to Evaluate GUI Testing Techniques
3. Thang Bui and Albert Nymeyer. Heuristic Sensitivity in Guided Random-Walk Based Model Checking

12:00 - 13:30: Lunch Break

13:30 - 15:00: Session 5: Behaviours and Scenario Specification,

Chair: Anh-Hoang Truong

1. Judith Thyssen and Benjamin Hummel. Behavioral Specification of Reactive Systems Using Stream-Based I/O Tables
2. Jewgenij Botaschanjan and Alexander Harhurin. Property Driven Scenario Integration
3. Rob Hierons, Guy-Vincent Jourdan, Hasan Ural and Husnu Yenigun. Checking Sequence Construction Using Adaptive and Preset Distinguishing Sequences

15:00 - 15:30: Coffee Break

15:30 - 17:00: Session 6: Program Analysis,

Chair: Guy-Vincent Jourdan

1. Pietro Ferrara. Checkmate: a Generic Static Analyzer of Java Multithreaded Programs
2. Makoto Tatsuta, Wei-Ngan Chin and Mahmudul Faisal Al Ameen. Completeness of Pointer Program Verification by Separation Logic
3. Ivan Lanese and Gianluigi Zavattaro. Programming Sagas in SOCK

19:00 - 21:30: Conference Banquet at Sen restaurant, No. 614 Lac Long Quan Road, Tay Ho Dist., Hanoi

9:00 - 10:00: Keynote 3:

Chair: Dang Van Hung

John Rushby, Software Verification and System Assurance

10:00 - 10:30: Coffee Break

10:30 - 12:00: Session 7: B/VDM,

Chair: Guillaume Bonfante

1. Ninh Thuan Truong, Viet Ha Nguyen and Thanh Binh Trinh. Coordinated consensus analysis of multi-agent systems using Event-B
2. Thai Son Hoang, Jean-Raymond Abrial and Andreas Fuerst. Event-B Patterns and Their Tool Support
3. Yojiro Kawamata, Christian Sommer, Fuyuki Ishikawa and Shinichi Honiden. Inter-specification consistency verification for VDM++

12:00 - 13:30: Lunch Break

13:30 - 15:00: Session 8: Program Analysis,

Chair: Mahadevan Subramaniam

1. Guillaume Bonfante, Jean-Yves Marion and Daniel Reynaud. A computability perspective on self-modifying programs
2. Davide Bresolin, Valentin Goranko, Angelo Montanari and Guido Sciavicco. Right Propositional Neighborhood Logic over Natural Numbers with Integer Constraints for Interval Lengths
3. Manuel Martins, Alexandre Madeira and L. S. Barbosa. Refinement via interpretation

15:00 - 15:30: Lunch Break

15:30 - 16:30: Session 9: Modelling/Analysis,

Chair: Ivan Lanese

1. Dzung Dang and Ohnishi Atsushi. Ontology-based Reasoning in Requirements Elicitation
2. Elisabeth Lien and Peter Olveczky. Formal Modeling and Analysis of an IETF Multicast Protocol

16:30 - 17:30: Session 10: Components/Database,

Chair: Dang Van Hung

1. Hugo Pacheco and Alcino Cunha. Mapping between Alloy specifications and database implementations
2. Gregor Goessler and Jean-Baptiste Raclet. Modal Contracts for Component-based Design

17:30 - 18:00: Session 11: Short/Tool Papers,

Chair: Ha Nguyen Viet

1. Duc-Hanh Dang and Martin Gogolla. Precise Model-Driven Transformations Based on Graphs and Metamodels [Tool Paper]
2. Patrice Chalin. Adjusted Verification Rules for Loops Are More Complete and Give Better Diagnostics for Less (short paper)