Klaus Havelund Knihy

The SPIN workshop serves as a platform for researchers focused on automata-based, explicit-state model checking technologies for analyzing and verifying asynchronous concurrent and distributed systems. The SPIN model checker, developed by Gerard Holzmann, is widely recognized and boasts a large user community, largely due to its efficient state exploration algorithms and its modeling language, Promela, which resembles a programming language. Traditionally, the workshop features papers on SPIN extensions and applications. This year, however, the workshop expanded its focus to include software verification, encouraging submissions that analyze and verify programs written in conventional programming languages. This led to a collection of papers discussing methods such as translating source code to Promela and developing model checkers that directly accept source code. This emerging research direction is expected to present new challenges and solutions for the formal methods community. A key strategy for addressing large state spaces is abstraction, and there is potential for integrating model checking with static program analysis and testing techniques. Consequently, papers addressing these topics are included in the proceedings.

This book constitutes the refereed proceedings of the 7th International Symposium on NASA Formal Methods, NFM 2015, held in Pasadena, CA, USA, in April 2015. The 24 revised regular papers presented together with 9 short papers were carefully reviewed and selected from 108 submissions. The topics include model checking, theorem proving; SAT and SMT solving; symbolic execution; static analysis; runtime verification; systematic testing; program refinement; compositional verification; security and intrusion detection; modeling and specification formalisms; model-based development; model-based testing; requirement engineering; formal approaches to fault tolerance; and applications of formal methods.

This book constitutes the refereed proceedings of the 15th International SPIN workshop on Model Checking Software, SPIN 2008, held in Los Angeles, CA, USA, in August 2008. The 17 revised full papers presented together with 1 tool paper and 4 invited talks were carefully reviewed and selected from 41 submissions. The main focus of the workshop series is software systems, including models and programs. The papers cover theoretical and algorithmic foundations as well as tools for software model checking and foster interactions and exchanges of ideas with related areas in software engineering, such as static analysis, dynamic analysis, and testing.

Software validation is a crucial yet costly aspect of modern software production. The FATES/RV 2006 workshop aimed to unite academics and industry professionals to explore formal methods for testing, analyzing programs, and monitoring their execution. These formal approaches encompass various techniques, including theorem proving, model checking, static program analysis, and more, enhancing traditional monitoring methods used in testing and debugging. From 31 submissions, 14 high-quality papers were selected, each undergoing rigorous anonymous reviews. Additionally, the proceedings feature two invited talks from Wolfgang Grieskamp (Microsoft Research) and Oege de Moor (Oxford University). This event marked the first collaboration between the FATES and RV workshops, demonstrating the benefits of integrating these two communities. Previous editions of FATES were held in locations such as Aalborg (2001), Brno (2002), Montreal (2003), and Vienna (2004), often in affiliation with other conferences. Since 2003, the proceedings of FATES have been published by Springer in the LNCS series, reflecting the ongoing commitment to advancing the field through collaborative efforts.