Abstract is missing.
- Processing Text for Privacy: An Information Flow PerspectiveNatasha Fernandes, Mark Dras, Annabelle McIver. 3-21 [doi]
- 20 Years of Real Real Time Model ValidationKim Guldstrand Larsen, Florian Lorber, Brian Nielsen. 22-36 [doi]
- Deadlock Detection for Actor-Based CoroutinesKeyvan Azadbakht, Frank S. de Boer, Erik P. de Vink. 39-54 [doi]
- An Algebraic Approach for Reasoning About Information FlowArthur Américo, Mário S. Alvim, Annabelle McIver. 55-72 [doi]
- Towards 'Verifying' a Water Treatment SystemJingyi Wang, Jun Sun 0001, Yifan Jia, Shengchao Qin, Zhiwu Xu. 73-92 [doi]
- FSM Inference from Long TracesFlorent Avellaneda, Alexandre Petrenko. 93-109 [doi]
- A Weakness Measure for GR(1) FormulaeDavide Giacomo Cavezza, Dalal Alrajeh, András György. 110-128 [doi]
- Producing Explanations for Rich LogicsSimon Busard, Charles Pecheur. 129-146 [doi]
- The Compound Interest in Relaxing PunctualityThomas Ferrère. 147-164 [doi]
- IPL: An Integration Property Language for Multi-model Cyber-physical SystemsIvan Ruchkin, Joshua Sunshine, Grant Iraci, Bradley R. Schmerl, David Garlan. 165-184 [doi]
- Timed Epistemic Knowledge Bases for Social NetworksRaúl Pardo, César Sánchez, Gerardo Schneider. 185-202 [doi]
- Optimal and Robust Controller Synthesis - Using Energy Timed Automata with UncertaintyGiovanni Bacci 0001, Patricia Bouyer, Uli Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, Pierre-Alain Reynier. 203-221 [doi]
- Encoding Fairness in a Synchronous Concurrent Program AlgebraIan J. Hayes, Larissa A. Meinicke. 222-239 [doi]
- A Wide-Spectrum Language for Verification of Programs on Weak Memory ModelsRobert J. Colvin, Graeme Smith. 240-257 [doi]
- Operational Semantics of a Weak Memory Model with Channel SynchronizationDaniel Schnetzer Fava, Martin Steffen, Volker Stolz. 258-276 [doi]
- Stepwise Development and Model Checking of a Distributed Interlocking System - Using RAISESigne Geisler, Anne Elisabeth Haxthausen. 277-293 [doi]
- Resource-Aware Design for Reliable Autonomous Applications with Multiple PeriodsRongjie Yan, Di Zhu, Fan Zhang, Yiqi Lv, Junjie Yang, Kai Huang. 294-311 [doi]
- Verifying Auto-generated C Code from Simulink - An Experience Report in the Automotive DomainPhilipp Berger, Joost-Pieter Katoen, Erika Ábrahám, Md Tawhid Bin Waez, Thomas Rambow. 312-328 [doi]
- QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable SystemsAndrea Vandin, Maurice H. ter Beek, Axel Legay, Alberto Lluch-Lafuente. 329-337 [doi]
- Modular Verification of Programs with Effects and Effect Handlers in CoqThomas Letan, Yann Régis-Gianas, Pierre Chifflier, Guillaume Hiet. 338-354 [doi]
- Combining Tools for Optimization and Analysis of Floating-Point ComputationsHeiko Becker, Pavel Panchekha, Eva Darulova, Zachary Tatlock. 355-363 [doi]
- A Formally Verified Floating-Point Implementation of the Compact Position Reporting AlgorithmLaura Titolo, Mariano M. Moscato, César A. Muñoz, Aaron Dutle, François Bobot. 364-381 [doi]
- Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and RecommendationsJohanna Nellen, Thomas Rambow, Md Tawhid Bin Waez, Erika Ábrahám, Joost-Pieter Katoen. 382-398 [doi]
- Multi-robot LTL Planning Under UncertaintyClaudio Menghi, Sergio García, Patrizio Pelliccione, Jana Tumova. 399-417 [doi]
- Vector Barrier Certificates and Comparison SystemsAndrew Sogokon, Khalil Ghorbal, Yong Kiam Tan, André Platzer. 418-437 [doi]
- Timed VacuityHana Chockler, Shibashis Guha, Orna Kupferman. 438-455 [doi]
- Falsification of Cyber-Physical Systems Using Deep Reinforcement LearningTakumi Akazaki, Shuang Liu, Yoriyuki Yamagata, Yihai Duan, Jianye Hao. 456-465 [doi]
- Dynamic Symbolic Verification of MPI ProgramsDhriti Khanna, Subodh Sharma, César Rodríguez, Rahul Purandare. 466-484 [doi]
- To Compose, or Not to Compose, That Is the Question: An Analysis of Compositional State Space GenerationSander de Putter, Anton Wijs. 485-504 [doi]
- View Abstraction for Systems with Component IdentitiesGavin Lowe. 505-522 [doi]
- Compositional Reasoning for Shared-Variable Concurrent ProgramsFuyuan Zhang, Yongwang Zhao, David Sanán, Yang Liu, Alwen Tiu, Shang-Wei Lin, Jun Sun 0001. 523-541 [doi]
- Statistical Model Checking of LLVM CodeAxel Legay, Dirk Nowotka, Danny Bøgsted Poulsen, Louis-Marie Traonouez. 542-549 [doi]
- SDN-Actors: Modeling and Verification of SDN ProgramsElvira Albert, Miguel Gómez-Zamalloa, Albert Rubio, Matteo Sammartino, Alexandra Silva 0001. 550-567 [doi]
- CompoSAT: Specification-Guided Coverage for Model FindingSorawee Porncharoenwase, Tim Nelson, Shriram Krishnamurthi. 568-587 [doi]
- Approximate Partial Order ReductionChuchu Fan, Zhenqi Huang, Sayan Mitra. 588-607 [doi]
- A Lightweight Deadlock Analysis for Programs with Threads and Reentrant LocksCosimo Laneve. 608-624 [doi]
- Formal Specification and Verification of Dynamic Parametrized ArchitecturesAlessandro Cimatti, Ivan Stojic, Stefano Tonetta. 625-644 [doi]
- From Formal Requirements to Highly Assured Software for Unmanned Aircraft SystemsCésar A. Muñoz, Anthony Narkawicz, Aaron Dutle. 647-652 [doi]
- Interlocking Design Automation Using Prover TridentArne Borälv. 653-656 [doi]
- Model-Based Testing for Avionics SystemsJörg Brauer, Uwe Schulze. 657-661 [doi]
- On Software Safety, Security, and Abstract InterpretationDaniel Kästner, Laurent Mauborgne, Christian Ferdinand. 662-665 [doi]
- Variant Analysis with QLPavel Avgustinov, Kevin Backhouse, Man Yue Mo. 666-670 [doi]
- Object-Oriented Security ProofsErnie Cohen. 671-674 [doi]
- Z3 and SMT in Industrial R&DNikolaj Bjørner. 675-678 [doi]
- Evidential and Continuous Integration of Software Verification ToolsTewodros A. Beyene, Harald Ruess. 679-685 [doi]
- Disruptive Innovations for the Development and the Deployment of Fault-Free SoftwareThierry Lecomte. 686-689 [doi]