Write a Blog >>
SPIN 2021
Mon 12 Jul 2021 Online
co-located with ECOOP and ISSTA 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).
You're viewing the program in a time zone which is different from your device's time zone change time zone

Mon 12 Jul

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

09:50 - 10:00
OpeningSPIN at SPIN
Chair(s): Alfons Laarman Leiden University
10:00 - 11:00
Invited talk 1SPIN at SPIN
Chair(s): Dragan Bosnacki Eindhoven University of Technology, The Netherlands
10:00
60m
Talk
Safety versus security: why have they not married yet?
SPIN
Marielle Stoelinga University of Twente and Radboud University, Nijmegen
11:00 - 12:00
Session 1SPIN at SPIN
Chair(s): Anton Wijs Eindhoven University of Technology
11:00
20m
Talk
Verifying Pipeline Implementations in OpenMP
SPIN
Maik Wiesner TU Darmstadt, Marie-Christine Jakobs TU Darmstadt, Germany
11:20
20m
Talk
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
20m
Talk
PatEC: Pattern-based Equivalence Checking
SPIN
Marie-Christine Jakobs TU Darmstadt, Germany
12:00 - 13:00
Lunch breakSPIN at SPIN
13:00 - 14:00
Invited talk 2SPIN at SPIN
Chair(s): Ana Sokolova University of Salzburg
13:00
60m
Talk
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
Session 2SPIN at SPIN
Chair(s): Sergio Mover Ecole Polytechnique
14:00
20m
Talk
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
20m
Talk
Accelerating the Computation of Dead and Concurrent Places using Reductions
SPIN
Nicolas Amat LAAS-CNRS, Silvano DAL ZILIO LAAS-CNRS, Didier Le Botlan LAAS-CNRS
14:40
20m
Coffee break
Coffee break
SPIN

15:00 - 16:00
Invited talk 3SPIN at SPIN
Chair(s): Stefan Leue
15:00
60m
Talk
The Rise and Fall of Linear Temporal Logic
SPIN
16:00 - 17:00
Session 3SPIN at SPIN
Chair(s): Tatjana Petrov Universität Konstanz
16:00
20m
Talk
Go2Pins: a framework for the LTL verification of Go programs
SPIN
16:20
20m
Talk
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
20m
Talk
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
Closing statementSPIN at SPIN
Chair(s): Alfons Laarman Leiden University

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).

Questions? Use the SPIN contact form.