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