9^th International Symposium on Formal Aspects of Component Software

Program

Wednesday, September 12

9:15 - 9:30 Opening

9:30 - 10:45 Invited Talk 1
Session chair: Gwen Salaun

• Tevfik Bultan. Analyzing Interactions of Asynchronously Communicating Software Components

10:45 - 11:15 Coffee Break

11:15 - 12:15 Session 1 (2 papers) - Message Passing and Composition
Session chair: Mario Bravetti

• Harsh Beohar and Pieter Cuijpers. Desynchronisation of Concrete Synchronous Systems.
• Domenico Bianculli, Carlo Ghezzi and Pierluigi San Pietro. The Tale of SOLOIST: a Specification Language for Service Compositions Interactions.

12:15 - 14:00 Lunch

14:00 - 16:00 Session 2 (4 papers) - Interface Theory and Connectors
Session chair: Marjan Sirjani

• Sebastian Bauer, Rolf Hennicker and Axel Legay. Component Interfaces with Contracts on Ports.
• Qiusong Yang, Edmund M. Clarke, Anvesh Komuravelli, Mingshu Li. Assumption Generation for Asynchronous Systems by Abstraction Refinement.
• Chris Chilton, Bengt Jonsson and Marta Kwiatkowska. Assume-Guarantee Reasoning for Safe Component Behaviours.
• Christos Kloukinas and Mert Ozkaya. XcD - Modular, Realizable Software Architectures.

18:00 - 19:00 Steering Committee Meeting.

Thursday, September 13

9:30 - 10:45 Invited Talk 2
Session chair: Corina Pasareanu

• Shaz Qadeer. Safe Programming of Asynchronous Interaction: Can We Do It for Real?

10:45 - 11:15 Coffee Break

11:15 - 12:15 Session 3 (2 papers) - Rewriting Logic
Session chair: Farhad Arbab

• Kyungmin Bae, Jose Meseguer and Peter Olveczky. Formal Patterns for Multirate Distributed Real-Time Systems.
• Ralf Sasse, Samuel King, Jose Meseguer and Shuo Tang. IBOS: A Correct-By-Construction Modular Browser.

12:15 - 13:30 Lunch

13:30 Visit to the Ames Exploration Center

14:30 - 16:30 Session 4 (4 papers) - Model Checking, SAT Solving, and Z Specification
Session chair: Peter Olveczky

• Hanne Riis Nielson, Flemming Nielson and Roberto Vigo. A Calculus for Quality.
• Nils Jansen, Erika Abraham, Barna Zajzon, Ralf Wimmer, Johann Schuster, Joost-Pieter Katoen and Bernd Becker. Symbolic Counterexample Generation for Discrete-time Markov Chains.
• Zachary J. Oster, Ganesh Ram Santhanam, Samik Basu and Vasant Honavar. Model Checking of Qualitative Sensitivity Preferences to Minimize Credential Disclosure.
• Pablo Castro, Nazareno Aguirre, Carlos Gustavo Lopez Pombo and Tom Maibaum. A Categorical Approach to Structuring and Promoting Z Specifications.

20:00 Banquet at Xanh restaurant

Friday, September 14

9:30 - 10:30 Panel "Component Software: Challenges for the Future"
Participants: Tevfik Bultan, Dimitra Giannakopoulou, Shankar Natarajan (moderator), Corina Pasareanu, Shaz Qadeer, Gwen Salaun.

10:30 - 11:00 Coffee Break

11:00 - 12:45 Session 5 (3 papers + 1 tool paper) - Deadlock Analysis and Run-time Verification
Session chair: Rolf Hennicker

• Frank de Boer, Mario Bravetti, Immo Grabe, Matias Lee, Martin Steffen and Gianluigi Zavattaro. Proving Deadlock Freedom for Active Objects and Futures.
• Steinar Hugi Sigurdarson, Marjan Sirjani, Yngvi Bjornsson and Arni Herman Reynisson. Guided Search for Deadlocks in Actor-Based Models.
• Amir Molzam Sharifloo and Paola Spoletini. LOVER: Light-weight Formal Verification of adaptivE systems at Run time.
• Stijn De Gouw and Frank S. De Boer. Run-Time Verification of Black-Box Components using Behavioral Specifications: An Experience Report on Tool Development.

12:45 - 14:30 Lunch