Accepted Papers

Full papers

  • Sean Sedwards, Axel Legay and Louis-Marie Traonouez. Estimating Rewards & Rare Events in Nondeterminstic Systems

  • Irene Lobo Valbuena and Moa Johansson. Conditional Lemma Discovery and Recursion Induction in Hipster

  • Maximilien Colange, Dimitri Racordon and Didier Buchs. Computing Bounds for Counter Automata

  • Mohammadsadegh Dalvandi, Michael Butler and Abdolbaghi Rezazadeh. Transforming Event-B Models to Dafny Contracts

  • Thomas Pani, Helmut Veith and Florian Zuleger. Loop Patterns in C Programs

  • Cláudio Belo Lourenço, Si-Mohamed Lamraoui, Shin Nakajima and Jorge Sousa Pinto. Studying Verification Conditions for Imperative Programs

  • Florent Chevrou, Aurélie Hurault and Philippe Quéinnec. Automated Verification of Asynchronous Communicating Systems with TLA+

  • Khaoula Es-Salhi, Siham Rim Boudaoud, Ciprian Teodorov, Vincent Ribaud and Zoé Drey. KriQL : A Language for Query-based Diagnosis of Transition Systems

  • Michele Volpato and Jan Tretmans. Approximate Active Learning of Nondeterministic Input Output Transition Systems

  • Vincent Rahli, David Guaspari, Mark Bickford and Robert Constable. Formal Specification, Verification, and Implementation of Fault-Tolerant Systems

  • Alexei Lisitsa. First-order logic for safety verification of hedge rewriting systems

  • Sean Sedwards, Axel Legay, Louis-Marie Traonouez and Cyrille Jegourel. Distributed Verification of Rare Properties using Importance Splitting Observers

  • Bojan Nokovic and Emil Sekerinski. Model-based WCET Analysis with Invariants

  • Ehsan Khamespanah, Marjan Sirjani, Mohammadreza Mousavi, Zeynab Sabahi Kaviani and Mohammadreza Razzazi. State Distribution Policy for Distributed Model Checking of Actor Models

  • Patricia Bouyer, Erwin Fang and Nicolas Markey. Permissive strategies in timed automata and games

Research idea papers

  • Shogo Hattori, Shoji Yuen, Hiroyuki Seki and Shuichi Sato. Automated Hazard Analysis with pMAX-SMT for Automobile Systems

  • Suraj Ajit, Oyindamola Olajubu, Scott Thomson and Mark Edwards. Model Transformation of high-level requirements in a Domain Specific Language into a Formal Specification Language

  • James Baxter and Ana Cavalcanti. A Verified Virtual Machine for Safety-Critical Java

  • Ekaterina Komendantskaya, Peng Fu and Patricia Johann. Structural Resolution for Automated Verification

  • Mohammed Alzahrani. Model Checking Web Applications using SPIN and UPPAAL

  • Mike Smith, Hoang Nga Nguyen and Markus Roggenbach. Revisiting modelling and analysing railway control systems in CSP