The 22nd International Symposium on Formal Methods in Oxford, UK, from 15 to 17 July 2018 as part of the FLoC 2018, the Federated Logic Conferences had an associated Doctoral Symposium that took place on 14 July. The aim of the doctoral symposium was to provide a helpful environment in which selected PhD students could present and discuss their ongoing work, meet other students working on similar topics, and receive helpful advice and feedback from a panel of researchers and academics.

The doctoral symposium had five contributed talks from PhD students as well as an invited talk from Sylvain Conchon, Professor of Computer Science at Université Paris-Sud, speaking on "Cubicle : a model checker for parameterized array-based transition systems”.

CV: Sylvain Conchon is a Professor of Computer Science at Université Paris-Sud and a member of LRI, the laboratory for Computer Science joint between Université Paris-Sud and CNRS. His research interests are at the crossroads of Model Checking, SMT solving, functional programming, and compilation techniques. He is also an enthusiastic OCaml programmer. He currently focuses on the design and development of the SMT solver Alt-Ergo and the SMT-based model checker Cubicle.

Abstract: In this talk, I will present Cubicle, a model checker for verifying safety properties of array-based systems, a syntactically restricted class of para­metrized transition systems with states represented as arrays indexed by an arbitrary number of processes. Cache coherence protocols and mutual exclusion algorithms are typical examples of such systems. After a short presentation of the semantics of its input language, I will present some details about its implementation, mainly its symbolic backward reachability analysis which makes use of Satisfiabilty Modulo Theories. I will conclude with a presentation of current and future works.

The contributed papers are included in these proceedings.

They were reviewed by a program committee consisting of:

Bernhard Aichernig, TU Graz, AT 

Nikolaj Bjørner, Microsoft Research, US 

Andrew Butterfield, Trinity College, IE 

Ana Cavalcanti, University of York, GB

Sylvian Conchon, Univ. Paris-Sud, F 

Stefania Gnesi, ISTI-CNR, Pisa, I

Jan Friso Groote, TU Eindhoven, NL

Cliff Jones, Newcastle University, GB 

Peter Gorm Larsen, Aarhus University, DK

Elizabeth Leonard, Naval Research Laboratory, US

Zhiming Liu, Southwest University, CN

Mercedes Merayo, Universidad Complutense Madrid, Spain

Cesar Munoz, NASA, US

Matteo Rossi, Politecnico di Milano, IT 

Martin Steffen, University of Oslo, N

Maurice Ter Beek, ISTI-CNR, IT

Elena Troubitsyna, Aabo Akademi, SF

We would like to thank the PhD students who made submissions, the invited speaker, and the program committee members for constructive reviews and helpful feedback to the PhD students. We would like to thank the organisers of FLOC’18 and FM’18 for their support, in particular Erik de Vink, Dave Parker, Radu Calinescu, Jan Peleska and Gethin Norman.