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