(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 [slides]

 11:00 - 12:30 Session 1: Verification

  • Jonatan Wiik and Pontus Boström
Specification and Automated Verification of Dynamic Dataflow Networks [slides]

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

  • Giordano Pola, Elena De Santis and Maria Domenica Di Benedetto
On Approximate Diagnosability of Metric Systems [slides]

 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 [slides]

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

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

  • 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 [slides]

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

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

Thursday, September 7

 9:00 - 10:20 Invited Talk

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

 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 [slides]

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

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

 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 [slides]

 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) [slides]

  • 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) [slides]

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 [slides]

 11:00 - 12:30 Session 7: Concurrency

  • Marie-Christine Jakobs
PART_PW: From Partial Analysis Results To a Proof Witness [slides]

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

  • 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 [slides]
 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 [slides]

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

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

  • 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 [slides]

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

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

Proceedings - Online version

Online version of the proceedings of SEFM 2017 is available for registered participants at this link.

Best Paper Award

The Program Committee of the 15th International Conference on Software Engineering and Formal Methods has granted the SEFM 2017 Best Paper Award to:

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

Gianni Zampedri,
Sep 18, 2017, 1:53 AM