SPIN model checking and software verification ; proceedings

Más información sobre el libro

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.