Li Li, Jun Sun and Jin Song Dong.

Automated Verification of Timed Security Protocols with Clock Drift

Victor B. F. Gomes and Georg Struth

Modal Kleene Algebra Applied to Program Correctness

Artem Khyzha, Alexey Gotsman and Matthew Parkinson

A Generic Logic for Proving Linearizability

Antonio E. Flores Montoya.

Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost Relations

Ian J. Hayes, Robert Colvin, Larissa Meinicke, Kirsten Winter and Andrius Velykis

An algebra of synchronous atomic steps

Zhe Hou, David Sanan, Alwen Tiu, Yang Liu and Koh Chuen Hoa.

An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for The LEON3 Processor

Nikola Benes, Lubos Brim, Martin Demko, Samuel Pastva and David Šafránek.

A Model Checking Approach to Discrete Bifurcation Analysis

Mahieddine Dellabani, Saddek Bensalem, Jacques Combaz and Marius Bozga.

Local Planning of Multiparty Interactions with a Bounded Horizon

Adel Djoudi, Sébastien Bardin and Éric Goubault.

Recovering high-level conditions from binary programs

Thomas Letan, Pierre Chifflier, Guillaume Hiet, Pierre Néron and Benjamin Morin.

SpecCert: Specifying and Verifying Hardware-based Security Enforcement

Hanno Becker, Juan Manuel Crespo, Jacek Galowicz, Ulrich Hensel, Yoichi Hirai, César Kunz, Keiko Nakata, Jorge Luis Sacchini, Hendrik Tews and Thomas Tuerk. Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor

Dimitra Giannakopoulou, Dennis Guck and Johann Schumann.

Exploring Model Quality for ACAS X

Rajdeep Mukherjee, Saurabh Joshi, Andreas Griesmayer, Daniel Kroening and Tom Melham.

Equivalence Checking of a Floating-point Unit Against a High-level C Model

Yusuke Kawamoto, Fabrizio Biondi and Axel Legay.

Hybrid Statistical Estimation of Mutual Information for Quantifying Information Flow

Bat-Chen Rothenberg and Orna Grumberg.

Sound and Complete Mutation-Based Program Repair

Miran Hasanagic, Peter Gorm Larsen, Peter W. V. Tran-Jørgensen and Kenneth Lausdahl.

Formalising and Validating the Interface Description in the FMI standard

Zhengfeng Yang, Chao Huang, Xin Chen, Wang Lin and Zhiming Liu.

A Linear Programming Relaxation Based Approach for Generating Barrier Certificates of Hybrid Systems

Ofer Strichman and Maor Veitsman.

Regression Verification for unbalanced recursive functions

Cristina David, Pascal Kesseli, Daniel Kroening and Matt Lewis.

Danger Invariants

Gaogao Yan, Li Jiao, Yangjia Li, Shuling Wang and Naijun Zhan.

Approximate Bisimulation and Discretization of Hybrid CSP

Tsutomu Kobayashi, Fuyuki Ishikawa and Shinichi Honiden.

Refactoring Refinement Structures of Event-B Machines

Pingfan Kong, Yi Li, Xiaohong Chen, Jun Sun, Meng Sun and Jingyi Wang.

Towards Concolic Testing for Hybrid Systems

Mingshuai Chen, Martin Fränzle, Yangjia Li, Peter N. Mosaad and Naijun Zhan.

Validated Simulation-Based Verification of Delayed Differential Dynamics

Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo and Wei-Ngan Chin.

Automated Mutual Explicit Induction Proof in Separation Logic

Stanislav Böhm, Ondřej Meca and Petr Jancar.

State-Space Reduction of Non-deterministically Synchronizing Systems Applicable to Deadlock Detection in MPI

Christoph-Simon Senjak and Martin Hofmann.

An Implementation of Deflate in Coq

Gudmund Grov, Yuhui Lin and Vytautas Tumas.

Mechanised Verification Patterns for Dafny

Heinrich Ody, Martin Fränzle and Michael R. Hansen.

Discounted Duration Calculus

Lacramioara Astefanoaei, Saddek Bensalem, Marius Bozga, Chih-Hong Cheng and Harald Ruess.

Compositional Parameter Synthesis

Ori Lahav and Viktor Vafeiadis.

Explaining Relaxed Memory Models with Program Transformations

Amirhossein Vakili and Nancy Day.

Finite Model Finding Using the Logic of Equality with Uninterpreted Functions

Saksham Chand, Annie Liu and Scott Stoller.

Formal Verification of Multi-Paxos for Distributed Consensus

Aleksandar S. Dimovski, Claus Brabrand and Andrzej Wasowski.

Finding Suitable Variability Abstractions for Family-Based Analysis

Anton Wijs, Thomas Neele and Dragan Bosnacki.

GPUexplore 2.0: Unleashing GPU Explicit-State Model Checking

Pedro Antonino, Thomas Gibson-Robinson and Bill Roscoe.

Tighter Reachability Criteria for Deadlock-Freedom Analysis

Yuqi Chen, Christopher M. Poskitt and Jun Sun.

Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation

Gilles Nies, Holger Hermanns, Marvin Stenger, Morten Bisgaard, David Gerhardt and Jan Krčál.

Battery-Aware Scheduling in Low Orbit: The GomX-3 Case

Alessandro Cimatti, Sergio Mover and Mirko Sessa.

From Electrical Switched Networks to Hybrid Automata

Claudio Menghi, Paola Spoletini and Carlo Ghezzi.

Dealing with Incompleteness in Automata-based Model Checking

Parosh Aziz Abdulla, Mohamed Faouzi Atig and Bui Phi Diep.

Counter-Example Guided Program Verification

Andrew Sogokon, Khalil Ghorbal and Taylor T Johnson.

Decoupled simulating abstractions of non-linear ordinary differential equations

Georgios Giantamidis and Stavros Tripakis.

Learning Moore Machines from Input-Output Traces

Teodor Stoenescu, Alin Stefanescu, Sorina Predut and Florentin Ipate.

RIVER: A Binary Analysis Framework using Symbolic Execution and Reversible x86 Instructions

Roberto Cavada, Alessandro Cimatti, Luigi Crema, Mattia Roccabruna and Stefano Tonetta.

Model-Based Design of an Energy-System Embedded Controller using Taste

Bjørnar Luteberget, Christian Johansen, Claus Feyling and Martin Steffen.

Rule-based Incremental Verification Tools Applied to Railway Designs and Regulations

Han Liu, Yu Jiang, Huafeng Zhang, Ming Gu and Jiaguang Sun.

Taming Interrupts For Verifying Industrial Multifunction Vehicle Bus Controllers

Predrag Filipovikj, Nesredin Mahmud, Raluca Marinescu, Cristina Seceleanu, Oscar Ljungkrantz and Henrik Lönn.

Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems

Ahmed Al-Brashdi.

Model-Based Database Design

Artur Gomes.

Mechanising the Translation from Circus to CSPm or Model-Checking Circus

Casper Thule.

Verifying the Co-Simulation Orchestration Engine for INTO-CPS

Rajdeep Mukherjee.

Hardware Verification Using Software Analyzers

Saulo Rodrigues E Silva.

Efficient development of models for user interfaces in high assurance systems

Vincent Bloemen.

Parallel Model Checking of ω-Automata

Mehrnoosh Askarpour.

Risk Assessment in Collaborative Robotic

Francesco Marconi.

Quality analysis and verification of data-intensive applications