Software engineering and formal methods : 15th International Conference, SEFM 2017, Trento, Italy, September 4?8, 2017, Proceedings

Front Matter ....Pages I-XIX
 Information Flow Tracking for Linux Handling Concurrent System Calls and Shared Memory  (Laurent Georget, Mathieu Jaume, Guillaume Piolle, Frédéric Tronel, Valérie Viet Triem Tong)....Pages 1-16
 Focused Certification of an Industrial Compilation and Static Verification Toolchain  (Zhi Zhang, Robby, John Hatcliff, Yannick Moy, Pierre Courtieu)....Pages 17-34
 A Complete Generative Label Model for Lattice-Based Access Control Models  (N. V. Narendra Kumar, R. K. Shyamasundar)....Pages 35-53
 From Model Checking to a Temporal Proof for Partial Models  (Anna Bernasconi, Claudio Menghi, Paola Spoletini, Lenore D. Zuck, Carlo Ghezzi)....Pages 54-69
 Modeling and Reasoning on Requirements Evolution with Constrained Goal Models  (Chi Mai Nguyen, Roberto Sebastiani, Paolo Giorgini, John Mylopoulos)....Pages 70-86
 Participatory Verification of Railway Infrastructure by Representing Regulations in RailCNL  (Bjørnar Luteberget, John J. Camilleri, Christian Johansen, Gerardo Schneider)....Pages 87-103
 An In-Depth Investigation of Interval Temporal Logic Model Checking with Regular Expressions  (Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron)....Pages 104-119
 PART\\(_\\mathrm {PW}\\): From Partial Analysis Results to a Proof Witness  (Marie-Christine Jakobs)....Pages 120-135
 Specification and Automated Verification of Dynamic Dataflow Networks  (Jonatan Wiik, Pontus Boström)....Pages 136-151
 Specification Clones: An Empirical Study of the Structure of Event-B Specifications  (Marie Farrell, Rosemary Monahan, James F. Power)....Pages 152-167
 User Studies of Principled Model Finder Output  (Natasha Danas, Tim Nelson, Lane Harrison, Shriram Krishnamurthi, Daniel J. Dougherty)....Pages 168-184
 Using Shared Memory Abstractions to Design Eager Sequentializations for Weak Memory Models  (Ermenegildo Tomasco, Truc Lam Nguyen, Bernd Fischer, Salvatore La Torre, Gennaro Parlato)....Pages 185-202
 On Run-Time Enforcement of Authorization Constraints in Security-Sensitive Workflows  (Daniel Ricardo dos Santos, Silvio Ranise)....Pages 203-218
 Trace Partitioning and Local Monitoring for Asynchronous Components  (Duncan Paul Attard, Adrian Francalanza)....Pages 219-235
 Compositional Verification of Interlocking Systems for Large Stations  (Alessandro Fantechi, Anne E. Haxthausen, Hugo D. Macedo)....Pages 236-252
 Formalizing Timing Diagram Requirements in Discrete Duration Calculus  (Raj Mohan Matteplackel, Paritosh K. Pandya, Amol Wakankar)....Pages 253-268
 On Approximate Diagnosability of Metric Systems  (Giordano Pola, Elena De Santis, Maria Domenica Di Benedetto)....Pages 269-283
 A Hazard Analysis Method for Systematic Identification of Safety Requirements for User Interface Software in Medical Devices  (Paolo Masci, Yi Zhang, Paul Jones, José C. Campos)....Pages 284-299
 Modular Verification of Information Flow Security in Component-Based Systems  (Simon Greiner, Martin Mohr, Bernhard Beckert)....Pages 300-315
 IJIT: An API for Boolean Program Analysis with Just-in-Time Translation  (Peizun Liu, Thomas Wahl)....Pages 316-331
 Specification and Semantic Analysis of Embedded Systems Requirements: From Description Logic to Temporal Logic  (Nesredin Mahmud, Cristina Seceleanu, Oscar Ljungkrantz)....Pages 332-348
 Computing Conditional Probabilities: Implementation and Evaluation  (Steffen Märcker, Christel Baier, Joachim Klein, Sascha Klüppelholz)....Pages 349-366
 Validating the Meta-Theory of Programming Languages (Short Paper)  (Guglielmo Fachini, Alberto Momigliano)....Pages 367-374
 Towards Inverse Uncertainty Quantification in Software Development (Short Paper)  (Matteo Camilli, Angelo Gargantini, Patrizia Scandurra, Carlo Bellettini)....Pages 375-381
 Interpolation-Based Learning as a Mean to Speed-Up Bounded Model Checking (Short Paper)  (Gianpiero Cabodi, Paolo Camurati, Marco Palena, Paolo Pasini, Danilo Vendraminetto)....Pages 382-387
 Towards Automated Deployment of Self-adaptive Applications on Hybrid Clouds (Short Paper)  (Lom Messan Hillah, Rodrigo Assad, Antonia Bertolino, Marcio Delamaro, Fabio De Rosa, Vinicius Garcia et al.)....Pages 388-393
 A Diagnosis Framework for Critical Systems Verification (Short Paper)  (Vincent Leildé, Vincent Ribaud, Ciprian Teodorov, Philippe Dhaussy)....Pages 394-400
 Design of Embedded Systems with Complex Task Dependencies and Shared Resource Interference (Short Paper)  (Fotios Gioulekas, Peter Poplavko, Rany Kahil, Panagiotis Katsaros, Marius Bozga, Saddek Bensalem et al.)....Pages 401-407
Back Matter ....Pages 409-410