Front Matter ....Pages I-XIV
Front Matter ....Pages 1-1
Processing Text for Privacy: An Information Flow Perspective (Natasha Fernandes, Mark Dras, Annabelle McIver)....Pages 3-21
20 Years of Real Real Time Model Validation (Kim Guldstrand Larsen, Florian Lorber, Brian Nielsen)....Pages 22-36
Front Matter ....Pages 37-37
Deadlock Detection for Actor-Based Coroutines (Keyvan Azadbakht, Frank S. de Boer, Erik de Vink)....Pages 39-54
An Algebraic Approach for Reasoning About Information Flow (Arthur Américo, Mário S. Alvim, Annabelle McIver)....Pages 55-72
Towards ‘Verifying’ a Water Treatment System (Jingyi Wang, Jun Sun, Yifan Jia, Shengchao Qin, Zhiwu Xu)....Pages 73-92
FSM Inference from Long Traces (Florent Avellaneda, Alexandre Petrenko)....Pages 93-109
A Weakness Measure for GR(1) Formulae (Davide Giacomo Cavezza, Dalal Alrajeh, András György)....Pages 110-128
Producing Explanations for Rich Logics (Simon Busard, Charles Pecheur)....Pages 129-146
The Compound Interest in Relaxing Punctuality (Thomas Ferrère)....Pages 147-164
IPL: An Integration Property Language for Multi-model Cyber-physical Systems (Ivan Ruchkin, Joshua Sunshine, Grant Iraci, Bradley Schmerl, David Garlan)....Pages 165-184
Timed Epistemic Knowledge Bases for Social Networks (Raúl Pardo, César Sánchez, Gerardo Schneider)....Pages 185-202
Optimal and Robust Controller Synthesis (Giovanni Bacci, Patricia Bouyer, Uli Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, Pierre-Alain Reynier)....Pages 203-221
Encoding Fairness in a Synchronous Concurrent Program Algebra (Ian J. Hayes, Larissa A. Meinicke)....Pages 222-239
A Wide-Spectrum Language for Verification of Programs on Weak Memory Models (Robert J. Colvin, Graeme Smith)....Pages 240-257
Operational Semantics of a Weak Memory Model with Channel Synchronization (Daniel Schnetzer Fava, Martin Steffen, Volker Stolz)....Pages 258-276
Stepwise Development and Model Checking of a Distributed Interlocking System - Using RAISE (Signe Geisler, Anne E. Haxthausen)....Pages 277-293
Resource-Aware Design for Reliable Autonomous Applications with Multiple Periods (Rongjie Yan, Di Zhu, Fan Zhang, Yiqi Lv, Junjie Yang, Kai Huang)....Pages 294-311
Verifying Auto-generated C Code from Simulink (Philipp Berger, Joost-Pieter Katoen, Erika Ábrahám, Md Tawhid Bin Waez, Thomas Rambow)....Pages 312-328
QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems (Andrea Vandin, Maurice H. ter Beek, Axel Legay, Alberto Lluch Lafuente)....Pages 329-337
Modular Verification of Programs with Effects and Effect Handlers in Coq (Thomas Letan, Yann Régis-Gianas, Pierre Chifflier, Guillaume Hiet)....Pages 338-354
Combining Tools for Optimization and Analysis of Floating-Point Computations (Heiko Becker, Pavel Panchekha, Eva Darulova, Zachary Tatlock)....Pages 355-363
A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm (Laura Titolo, Mariano M. Moscato, César A. Muñoz, Aaron Dutle, François Bobot)....Pages 364-381
Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations (Johanna Nellen, Thomas Rambow, Md Tawhid Bin Waez, Erika Ábrahám, Joost-Pieter Katoen)....Pages 382-398
Multi-robot LTL Planning Under Uncertainty (Claudio Menghi, Sergio Garcia, Patrizio Pelliccione, Jana Tumova)....Pages 399-417
Vector Barrier Certificates and Comparison Systems (Andrew Sogokon, Khalil Ghorbal, Yong Kiam Tan, André Platzer)....Pages 418-437
Timed Vacuity (Hana Chockler, Shibashis Guha, Orna Kupferman)....Pages 438-455
Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning (Takumi Akazaki, Shuang Liu, Yoriyuki Yamagata, Yihai Duan, Jianye Hao)....Pages 456-465
Dynamic Symbolic Verification of MPI Programs (Dhriti Khanna, Subodh Sharma, César Rodríguez, Rahul Purandare)....Pages 466-484
To Compose, or Not to Compose, That Is the Question: An Analysis of Compositional State Space Generation (Sander de Putter, Anton Wijs)....Pages 485-504
View Abstraction for Systems with Component Identities (Gavin Lowe)....Pages 505-522
Compositional Reasoning for Shared-Variable Concurrent Programs (Fuyuan Zhang, Yongwang Zhao, David Sanán, Yang Liu, Alwen Tiu, Shang-Wei Lin et al.)....Pages 523-541
Statistical Model Checking of LLVM Code (Axel Legay, Dirk Nowotka, Danny Bøgsted Poulsen, Louis-Marie Tranouez)....Pages 542-549
SDN-Actors: Modeling and Verification of SDN Programs (Elvira Albert, Miguel Gómez-Zamalloa, Albert Rubio, Matteo Sammartino, Alexandra Silva)....Pages 550-567
CompoSAT: Specification-Guided Coverage for Model Finding (Sorawee Porncharoenwase, Tim Nelson, Shriram Krishnamurthi)....Pages 568-587
Approximate Partial Order Reduction (Chuchu Fan, Zhenqi Huang, Sayan Mitra)....Pages 588-607
A Lightweight Deadlock Analysis for Programs with Threads and Reentrant Locks (Cosimo Laneve)....Pages 608-624
Formal Specification and Verification of Dynamic Parametrized Architectures (Alessandro Cimatti, Ivan Stojic, Stefano Tonetta)....Pages 625-644
Front Matter ....Pages 645-645
From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems (César Muñoz, Anthony Narkawicz, Aaron Dutle)....Pages 647-652
Interlocking Design Automation Using Prover Trident (Arne Borälv)....Pages 653-656
Model-Based Testing for Avionics Systems (Jörg Brauer, Uwe Schulze)....Pages 657-661
On Software Safety, Security, and Abstract Interpretation (Daniel Kästner, Laurent Mauborgne, Christian Ferdinand)....Pages 662-665
Variant Analysis with QL (Pavel Avgustinov, Kevin Backhouse, Man Yue Mo)....Pages 666-670
Object-Oriented Security Proofs (Ernie Cohen)....Pages 671-674
Z3 and SMT in Industrial R&D (Nikolaj Bjørner)....Pages 675-678
Evidential and Continuous Integration of Software Verification Tools (Tewodros A. Beyene, Harald Ruess)....Pages 679-685
Disruptive Innovations for the Development and the Deployment of Fault-Free Software (Thierry Lecomte)....Pages 686-689
Back Matter ....Pages 691-692