Programme

(Please notice that the program may be subject to changes)

Wednesday, September 6

 9:00 - 10:20 Invited Talk
  • Marsha Chechik (University of Toronto, Canada)
Software Safety and Security, Assurance Cases and Model Management

 11:00 - 12:30 Session 1: Verification
  • Marie-Christine Jakobs
PART_PW: From Partial Analysis Results To a Proof Witness
  • Jonatan Wiik and Pontus Boström
Specification and Automated Verification of Dynamic Dataflow Networks
  • Giordano Pola, Elena De Santis and Maria Domenica Di Benedetto
On Approximate Diagnosability of Metric Systems

 14:00 - 15:50 Session 2: Model Checking

  • Anna Bernasconi, Claudio Menghi, Paola Spoletini, Lenore Zuck and Carlo Ghezzi
From model checking to a temporal proof for partial models

  • Alessandro Fantechi, Anne E. Haxthausen and Hugo Daniel Macedo
Compositional Verification of Interlocking Systems for Large Stations

  • Steffen Märcker, Christel Baier, Joachim Klein and Sascha Klüppelholz
Computing Conditional Probabilities: Implementation and Evaluation

  • Gianpiero Cabodi, Paolo Camurati, Marco Palena, Paolo Pasini and Danilo Vendraminetto
Interpolation-based learning as a means to speed-up Bounded Model Checking (Short paper)

 16:20 - 17:40 Session 3: Verification and Tools

  • Zhi Zhang, Na Robby, John Hatcliff, Yannick Moy and Pierre Courtieu
Focused Certification of an Industrial Compilation and Static Verification Toolchain

  • Peizun Liu and Thomas Wahl
IJIT: An API for Boolean Program Analysis with Just-in-Time Translation

  • Leilde Vincent, Vincent Ribaud, Ciprian Teodorov and Philippe Dhaussy
A diagnosis framework for critical systems verification (Short paper)


Thursday, September 7

 9:00 - 10:20 Invited Talk

  • Jeff Kramer (Imperial College London, United Kingdom)
The Challenge of Change

 11:00 - 12:30 Session 4: Requirement and Specification 1

  • Chi Mai Nguyen, Roberto Sebastiani, Paolo Giorgini and John Mylopoulos
Modeling and Reasoning on Requirements Evolution with Constrained Goal Models

  • Bjørnar Luteberget, John J. Camilleri, Christian Johansen and Gerardo Schneider
Participatory Verification of Railway Infrastructure by Representing Regulations in RailCNL

  • Marie Farrell, Rosemary Monahan and James Power
Specification Clones: An empirical study of the structure of Event-B specifications

 14:00 - 15:30 Session 5: Requirement and Specification 2

  • Nesredin Mahmud, Cristina Seceleanu and Oscar Ljungkrantz
Specification and Semantic Analysis of Embedded Systems Requirements: From Description Logic to Temporal Logic

  • Raj Mohan Matteplackel, Paritosh K Pandya and Amol Wakankar
Formalizing Timing Diagram Requirements in Discrete Duration Calculus

  • Paolo Masci, Yi Zhang, Paul Jones and Jose C. Campos
A Hazard Analysis Method for Systematic Identification of Safety Requirements for User Interface Software in Medical Devices

 16:00 - 16:40 Session 6: Design and Deployment

  • Fotios Gioulekas, Peter Poplavko, Rany Kahil, Panagiotis Katsaros, Marius Bozga, Saddek Bensalem and Pedro Palomo
Design of embedded systems with complex task dependencies and shared resource interference (Short paper)

  • Lom Messan Hillah, Rodrigo Assad, Antonia Bertolino, Marcio Delamaro, Fabio De Rosa, Vinicius Garcia, Francesca Lonetti, Ariele-Paolo Maesano, Libero Maesano, Eda Marchetti, Breno Miranda, Auri Vincenzi and Juliano Iyoda
Towards automated deployment of self-adaptive applications on hybrid clouds (Short paper)


Friday, September 8

 9:00 - 10:20    Invited Talk

  • Alberto Sangiovanni-Vincentelli (Berkeley University, United States)
A Formal Contract-Based Design Methodology for CyberPhysical Systems 

 11:00 - 12:30 Session 7: Concurrency

  • Laura Bozzelli, Alberto Molinari, Angelo Montanari and Adriano Peron
An in-Depth Investigation of Interval Temporal Logic Model Checking with Regular Expressions

  • Duncan Attard and Adrian Francalanza
Trace Partitioning and Local Monitoring for Asynchronous Components

  • Ermenegildo Tomasco, Truc Nguyen Lam, Bernd Fischer, Salvatore La Torre and Gennaro Parlato
Using Shared Memory Abstractions to Design Eager Sequentializations for Weak Memory Models
 
 14:00 - 16:00 Session 8: Security

  • Laurent Georget, Mathieu Jaume, Guillaume Piolle, Frédéric Tronel and Valérie Viet Triem Tong
Information Flow Tracking for Linux Handling Concurrent System Calls and Shared Memory

  • Rudrapatna Shyamasundar and Narendra Kumar Nelabhotla
A Complete Generative Label Model for Lattice-based Access Control Models

  • Daniel Ricardo Dos Santos and Silvio Ranise
On Run-time Enforcement of Authorization Constraints in Security-Sensitive Business Processes

  • Simon Greiner, Martin Mohr and Bernhard Beckert
Modular Verification of Information-Flow Security in Component-Based Systems
 
 16:30 - 17:40    Session 9

  • Natasha Danas, Tim Nelson, Lane Harrison, Shriram Krishnamurthi and Daniel J. Dougherty
User Studies of Principled Model Finder Output

  • Matteo Camilli, Angelo Gargantini, Patrizia Scandurra and Carlo Bellettini.
Towards Inverse Uncertainty Quantification in Software Development (Short paper)

  • Guglielmo Fachini and Alberto Momigliano.
Validating the Meta-Theory of Programming Languages (Short paper)