27th International SPIN Symposium on Model Checking of SoftwareSPIN 2021
The 27th edition of the SPIN symposium aims at bringing together researchers and practitioners interested in automated tool-based techniques for the analysis of software as well as models of software, for the purpose of verification and validation. The symposium specifically focuses on concurrent software but does not exclude the analysis of sequential software. Submissions are solicited on theoretical results, novel algorithms (classical and quantum), tool development for modern hardware (parallel and distributed), and empirical evaluation.
Invited talks
Vincenzo Ciancia, CNR-ISTI
► Spatial Model Checking and its applications to Medical Image Analysis
Spatial aspects of computation are prominent in Computer Science, especially when dealing with systems distributed in physical space or with image data acquired from various sources. However, formal verification techniques are usually concerned with temporal properties and do not explicitly handle spatial information. Our work stems from the topological interpretation of modal logics, the so-called Spatial Logics. We present a topology-based approach to model checking for spatial and spatio-temporal properties.
Our research was initiated with the definition of a modal logic enhanced with: 1) a reachability operator, in the general setting of Cech closure spaces, encompassing both topological spaces and graphs; 2) a collective extension, permitting global operators akin to region calculi. On top of this, applicability has been demonstrated via free and open source software tools, and case studies in the setting of smart transportation and image analysis.
In recent work, we explored the application domain of automatic contouring in Medical Imaging, introducing the tool VoxLogicA, which merges the state-of-the-art imaging library ITK with the unique combination of declarative specification and optimised execution provided by spatial model checking. The analysis of existing benchmarks of medical images, for segmentation of brain tumors, and for the automated contouring of nevi, shows that simple VoxLogicA specifications can reach state-of-the-art accuracy, competing with best-in-class algorithms based on machine learning, with the advantage of explainability and easy replicability.
More recently, we introduced a geometric interpretation on continuous space exploiting simplicial complexes, with applications to the analysis of 3D meshes, a GPU-based implementation, enabling a consistent efficiency speed-up, and a definition of bisimilarity, aimed at minimization up-to logical equivalence.
Mariëlle Stoelinga, Twente / Radboud University
► Safety versus security: why have they not married yet?
Safety and security are two historically separated fields that have many aspects in common. Safety is the absence of disruptions due to unintended failures; security is the absence of disruptions due to malicious attacks. While both safety and security aim at mitigating system risks with cost-effective counter measures, they take opposing views when in comes to modelling, measuring and mitigating. In this talk, I will present the main differences and similarities between safety and security risk analyses, as well as directions to reconcile these important fields, through mathematical game theory, uncertainty reasoning and stochastic analysis. The research is funded by an ERC consolidator grant CAESAR: integrating safety and cybersecurity through stochastic model checking.Moshe Vardi, Rice University
► The Rise and Fall of Linear Temporal Logic
One of the surprising developments in the area of program verification in the late part of the 20th Century is the emergence of Linear Temporal Logic (LTL), a logic that emerged in philisophical studies of free will, as the cannonical language for describing temporal behavior of computer systems. LTL, however, is not expressive enough for industrial applications. The first decade of the 21 Century saw the emergence of industrial temporal logics such as ForSpec, PSL, and SVA. These logics, however, are not clean enough to serve as objects of theoretical study. This talk will describe the rise and fall of LTL, and will propose a new cannonical temporal logic: Linear Dynamic Logic (LDL).Mon 12 JulDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
09:50 - 10:00 | |||
10:00 - 11:00 | Invited talk 1SPIN at SPIN Chair(s): Dragan Bosnacki Eindhoven University of Technology, The Netherlands | ||
10:00 60mTalk | Safety versus security: why have they not married yet? SPIN Marielle Stoelinga University of Twente and Radboud University, Nijmegen | ||
11:00 - 12:00 | |||
11:00 20mTalk | Verifying Pipeline Implementations in OpenMP SPIN | ||
11:20 20mTalk | A model-checked I2C specification SPIN Lukas Humbel ETH Zurich, Daniel Schwyn ETH Zurich, Nora Hossle ETH Zurich, Roni Häcki ETH Zurich, Melissa Licciardello ETH Zurich, Jan Schär ETH Zurich, David Cock ETH Zurich, Michael Giardino ETH Zurich, Timothy Roscoe ETH Zurich | ||
11:40 20mTalk | PatEC: Pattern-based Equivalence Checking SPIN Marie-Christine Jakobs TU Darmstadt, Germany | ||
13:00 - 14:00 | |||
13:00 60mTalk | Spatial Model Checking and its applications to Medical Image Analysis SPIN Vincenzo Ciancia Istituto di Scienza e Tecnologie dell'Informazione "A. Faedo", Consiglio Nazionale delle Ricerche, Pisa, ITALY | ||
14:00 - 15:00 | |||
14:00 20mTalk | Spotlight Abstraction in Model Checking Real-Time Task Schedulability SPIN Madoda Nxumalo University of Pretoria, Nils Timm University of Pretoria, Stefan Gruner University of Pretoria | ||
14:20 20mTalk | Accelerating the Computation of Dead and Concurrent Places using Reductions SPIN | ||
14:40 20mCoffee break | Coffee break SPIN | ||
15:00 - 16:00 | |||
15:00 60mTalk | The Rise and Fall of Linear Temporal Logic SPIN | ||
16:00 - 17:00 | |||
16:00 20mTalk | Go2Pins: a framework for the LTL verification of Go programs SPIN | ||
16:20 20mTalk | C-SMC: A Hybrid Statistical Model Checking and Concrete Runtime Engine for Analyzing C Programs SPIN Antoine Chenoy Université catholique de Louvain, Fabien Duchene ICTEAM, UCLouvain, Thomas Given-Wilson Université catholique de Louvain, Axel Legay Université Catholique de Louvain, Belgium | ||
16:40 20mTalk | Probabilistic Model Checking of Randomized Java Code SPIN Syyeda Zainab Fatmi York University, Xiang Chen University of Waterloo, Yash Dhamija York University, Maeve Wildes McGill University, Qiyi Tang University of Oxford, Franck van Breugel York University, Canada | ||
17:00 - 17:15 | |||
Accepted Papers
Call for Papers
The 27th edition of the SPIN symposium aims at bringing together researchers and practitioners interested in automated tool-based techniques for the analysis of software as well as models of software, for the purpose of verification and validation. The symposium specifically focuses on concurrent software but does not exclude the analysis of sequential software. Submissions are solicited on theoretical results, novel algorithms (classical and quantum), tool development for modern hardware (parallel and distributed), and empirical evaluation.
Topics
Topics of interest include, but are not limited to:
- Formal verification techniques for automated analysis of software
- Formal analysis for modeling languages, such as UML/state charts
- Formal specification languages, temporal logic, design-by-contract
- Model checking
- Automated theorem proving, including SAT and SMT
- Verifying compilers
- Abstraction and symbolic execution techniques
- Static analysis and abstract interpretation
- Combination of verification techniques
- Modular and compositional verification techniques
- Verification of timed and probabilistic systems
- Automated testing using advanced analysis techniques
- Combination of static and dynamic analyses
- Derivation of specifications, test cases, or other useful material via formal analysis
- Case studies of interesting systems or with interesting results
- Engineering and implementation of software verification and analysis tools
- Benchmark and comparative studies for formal verification and analysis tools
- Formal methods of education and training
- Insightful surveys or historical accounts on topics of relevance to the symposium
- Relevant tools and algorithms for modern hardware, e.g.: parallel, GPU, TPU, cloud, and quantum
Submission Guidelines
The proceedings of SPIN 2021 will be published in Springer’s Lecture Notes in Computer Science series. Submissions should adhere to the LNCS format: LNCS Information for Authors.
With the exception of survey and history papers, the papers should contain original work that has not been submitted or accepted for publication elsewhere. We are soliciting three categories of papers:
- Full Research or Tool Papers describing fully developed work and complete results (16 pages – references are not included in this limit);
- Short Papers presenting tools, technology, experiences with lessons learned, new ideas, work in progress with preliminary results, and novel contributions to formal methods (6 pages – references are not included in this limit).
- Tool Demo Papers presenting the foundations, capabilities, application domains and relevant examples using the tools, with a clear description of what is expected to be shown in a live demonstration (4 pages to describe the tool foundations, features and use examples, plus an appendix explaining the content of the demo).
Papers should be submitted via the EasyChair SPIN 2021 submission website. All papers that conform to submission guidelines will be peer-reviewed by members of the program committee. Submissions will be evaluated on the basis of originality, the importance of contribution, soundness, evaluation, quality of presentation, and appropriate comparison to related work. At least one author of each accepted paper must attend the symposium and present the paper.
STTT
A selection of papers will be invited to a special issue of the International Journal on Software Tools for Technology Transfer (STTT).
| Mon 12 Jul 2021 - Conference |
| Sun 30 May 2021 Camera-ready version |
| Thu 20 May 2021 Author notification |
| Tue 20 Apr 2021 Submission deadline |
Jiri Barnat
Masaryk University
Maurice H. ter Beek
ISTI-CNR
Italy
Tom van Dijk
University of Twente
Netherlands
Vedran Dunjko
Leiden University
Stefan Edelkamp
University of Koblenz
Germany
Grigory Fedyukovich
Florida State University
United States
Patrice Godefroid
Microsoft Research, USA
United States
Henri Hansen
Tampere University
Finland
Arnd Hartmanns
University of Twente
Netherlands
Gerard Holzmann
NASA/Caltech Jet Propulsion Laboratory
United States
Antti Hyvärinen
Università della Svizzera Italiana
Switzerland
Nils Jansen
Radboud University Nijmegen
Netherlands
Peter Gjøl Jensen
Aalborg University, Denmark
Denmark
Sung-Shik Jongmans
Open University of the Netherlands; CWI
Netherlands
Jeroen J.A. Keiren
Eindhoven University of Technology
Igor Konnov
Informal Systems Inc
Austria
Alberto Lluch Lafuente
Technical University of Denmark
Denmark
Kuldeep S. Meel
National University of Singapore
Alice Miller
University of Glasgow
United Kingdom
Sergio Mover
Ecole Polytechnique
Rajagopal Nagarajan
Middlesex University
Doron Peled
Bar Ilan University
Israel
Tatjana Petrov
Universität Konstanz
Germany
Jaco van de Pol
Aarhus University
Denmark
Stephen F. Siegel
University of Delaware
United States
Carsten Sinz
Karlsruhe Institute of Technology
Jiri Srba
Aalborg University
Michael Tautschnig
Amazon Web Services
Yann Thierry-Mieg
Sorbonne Université — LIP6
France
Yakir Vizel
Technion—Israel Institute of Technology
Israel
Georg Weissenbacher
TU Wien
Austria
Anton Wijs
Eindhoven University of Technology
Netherlands