Paul C. Bell (editor) - Reachability Problems: 15th International Conference, RP 2021, Liverpool, UK, October 25–27, 2021, Proceedings

More information about this subseries at http://www.springer.com/series/7407

Chapter Recent Advances on Reachability Problems for Valence Systems (Invited Talk) is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/). For further details see license information in the chapter.

This Springer imprint is published by the registered company Springer Nature Switzerland AG

The registered company address is: Gewerbestrasse 11, 6330 Cham, Switzerland

This volume contains the papers presented at the 15th International Conference on Reachability Problems (RP 2021), organized by the University of Liverpool and Liverpool John Moores University, UK. Previous events in the series were located at the University of Paris, France (2020), Universit Libre de Bruxelles, Belgium (2019), Aix-Marseille University, France (2018), Royal Holloway, University of London, UK (2017), Aalborg University, Denmark (2016), the University of Warsaw, Poland (2015), the University of Oxford, UK (2014), Uppsala University, Sweden (2013), the University of Bordeaux, France (2012), the University of Genoa, Italy (2011), Masaryk University Brno, Czech Republic (2010), cole Polytechnique, France (2009), the University of Liverpool, UK (2008), and Turku University, Finland (2007).

The aim of the conference is to bring together scholars from diverse fields with a shared interest in reachability problems, and to promote the exploration of new approaches for the modeling and analysis of computational processes by combining mathematical, algorithmic, and computational techniques. Topics of interest include (but are not limited to) reachability for infinite state systems; rewriting systems; reachability analysis in counter/timed/cellular/communicating automata; Petri nets; computational game theory; computational aspects of semigroups, groups, and rings; reachability in dynamical and hybrid systems; frontiers between decidable and undecidable reachability problems; complexity and decidability aspects; predictability in iterative maps, and new computational paradigms.

Recent Advances on Reachability Problems for Valence Systems (Invited Talk)

The conference received 27 submissions (17 regular and 10 presentation only submissions) from which four regular papers were withdrawn. Each submission was carefully reviewed by three Program Committee (PC) members. Based on these reviews, the PC decided to accept six regular papers in addition to four invited speakers contributions. The members of the PC and the list of external reviewers can be found at the end of this preface. We are grateful for the high-quality work produced by the PC and the external reviewers. Overall this volume contains six contributed papers and four papers from invited speakers which cover their talks.

The conference also provided the opportunity to other young and established researchers to present work in progress or work already published elsewhere. This year in addition to six regular submissions, the PC accepted 10 high-quality informal presentations on various reachability aspects in theoretical computer science. A list of accepted presentation-only submissions is given below:

Guillaume Girol, Benjamin Farinier, and Sebastien Bardin

Abstract. This paper introduces a new property called robust reachability which refines the standard notion of reachability in order to take replicability into account. A bug is robustly reachable if a controlled input can make it so the bug is reached whatever the value of uncontrolled input. Robust reachability is better suited than standard reachability in many realistic situations related to security (e.g., criticality assessment or bug prioritization) or software engineering (e.g., replicable test suites and flakiness). We propose a formal treatment of the concept, and we revisit existing symbolic bug finding methods through this new lens. Remarkably, robust reachability allows differentiating bounded model checking from symbolic execution while they have the same deductive power in the standard case. Finally, we propose the first symbolic verifier dedicated to robust reachability: we use it for criticality assessment of four existing vulnerabilities and compare it with standard symbolic execution. Note: this paper has been published in the proceedings of CAV 2021.