Introduction to the special issue for SPIN 2019

  • PDF / 159,780 Bytes
  • 2 Pages / 595.276 x 790.866 pts Page_size
  • 17 Downloads / 193 Views

DOWNLOAD

REPORT


STTT Special Issue: SPIN 2019

Introduction to the special issue for SPIN 2019 Fabrizio Biondi1 · Thomas Given-Wilson2 · Axel Legay2,3

© Springer-Verlag GmbH Germany, part of Springer Nature 2020

Abstract This short introduction presents the selected papers from SPIN 2019. Keywords Statistical model checking · Applications · Security · Safety

1 Introduction This special issue contains the extended and improved versions of the best papers presented at the 26th International Symposium on Model Checking Software, SPIN 2019, held in Beijing, China, July 15–16, 2019. The original submissions to the conference were addressing topics like: 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 education and training; and insightful surveys or historical accounts on topics of relevance to the symposium.

B

Axel Legay [email protected]

1

Avast Software, Prague, Czech Republic

2

Université Catholique de Louvain, Louvain-La-Neuve, Belgium

3

Aalborg University, Aalborg, Denmark

The symposium attracted 29 submissions that were carefully reviewed by three Program Committee (PC) members. The selection process included further online discussion open to all PC members. As a result, 13 papers were selected for presentation at the symposium and publication in Springer’s proceedings. The program also includes one invited talk by Kim G. Larsen (Aalborg University), and one invited talk by Kuldeep S. Meel (National University of Singapore) From the 13 regular papers, we invited the best ones based on the reviews and the presentations in the event. The authors of four papers accepted to improve and to extend their works. The extended submissions went through a new review process with at least two phases for each paper. The four accepted papers included in this issue addressed all the concerns by the reviewers and by the guest editors. – In the first paper, “Extracting Safe Thread Schedules from Incomplete Model Checking Results” [3], the authors present a technique that uses the results of incomplete concurrent verification attempts to construct a (fair) scheduler that allows the safe execution of the partially verified concurrent program. This schedule