ARCH17: Editor's Preface

This volume of proceedings contains the papers presented at the fourth International Workshop on Applied veRification for Continuous and Hybrid systems (ARCH). The workshop was collocated with Cyber-Physical Systems Week (CPSWeek) on April 17, 2017 in Pittsburgh, PA, USA. It continues the series of ARCH workshops that were held 2014 in Berlin, 2015 in Seattle, and 2016 in Vienna. The goal of the ARCH workshops is to bring people from industry together with researchers and tool developers interested in applying verification techniques to continuous and hybrid systems. The workshops are accompanied by a collaborative website (cps-vo.org/group/ARCH), which features a curated collection of benchmarks, disseminates results submitted by researchers and tool developers, and provides feedback from practitioners in the form of experience reports. The benchmark repository is intended to serve as a lasting and evolving resource to the research community.

The workshop received 12 submissions. Each submission was reviewed by 3-4 program committee members, including at least one member from academia and one from industry. The committee accepted 10 papers. The program included the invited talk

• Sebastian Scherer: Challenges for Safe Autonomous Flight.

As in previous years, the ARCH workshop awarded a prize to an outstanding submission. The program committee proposed four candidates and the workshop attendees selected the final winner. The 2017 prize for the best paper was sponsored by Bosch and went to 

• Stanley Bak and Parasara Sridhar Duggirala: Direct Verification of Linear Systems with over 10000 Dimensions.

In additon to the workshop papers, these proceedings present the results of the first edition of ARCH-COMP, a competition for the formal verification of continuous and hybrid systems. ARCH-COMP is a friendly competition that was carried out online from February to April, 2017. Its results were presented at the ARCH workshop. ARCH-COMP showcases which methods are particularly suitable to which types of problems. As a side effect, it aims at establishing a consensus for comparing different software implementations in the context of verification, as such comparisons are routinely demanded by reviewers of scientific publications. 

All participating tools were represented in the competition jury, headed by the organizers. In the problem phase of the competition, participants submitted problem instances, which were then approved by the jury by consensus. In the evaluation phase, experiments were carried out by the tool authors themselves, who then submit the performance measurements and a repeatability package to the evaluation chair. The submitted results were approved by the jury and verified by an independent repeatability evaluation lead by Taylor T. Johnson. To establish further trustworthiness of the results, the code with which the results have been obtained is publicly available. 

In this first edition of ARCH-COMP, 13 tools have participated: Axelerator, BACH, CORA, Flow*, HyDRA, Hylaa, Isabelle/HOL, Lyse, PHAVer, SpaceEx, S-TaLiRo, VeriSiMPL, and XSpeed. The competition was divided into the following categories:

• Hybrid Systems with Piecewise Constant Dynamics (lead: Goran Frehse)
• Continuous and Hybrid Systems with Linear Continuous Dynamics (lead: Matthias Althoff)
• Continuous Systems with Nonlinear Dynamics (lead: Xin Chen)
• Bounded Model Checking of Hybrid Systems with Piecewise Constant Dynamics (lead: Lei Bu)
• Falsification (lead: Georgios Fainekos)

The problem descriptions and the results are provided in a report for each category, drafted by the category lead together with representatives of the participating tools. Due to the diversity of problems, ARCH-COMP does not provide any ranking of tools. Nonetheless, the presented results probably provide the most complete assessment of tools for the safety verification of continuous and hybrid systems up to this date.