Scope

The SPIN workshop is a forum for practitioners and researchers interested in state space-based techniques for the validation and analysis of software systems. The focus of the workshop is on theoretical advances and empirical evaluations based on explicit representations of state spaces, as implemented in the SPIN model checker or other tools, or techniques based on combinations of explicit and other symbolic representations. We welcome papers describing the development and application of state-space and path-exploration techniques for the testing and the verification of security-critical software, enterprise and web applications, embedded software, and other interesting software platforms. The workshop aims to encourage interactions and exchanges of ideas with all related areas in software engineering.

Topics of Interest Include (but are not limited to):

  • Algorithms and storage methods for explicit-state model checking
  • Theoretical and algorithmic foundations of model-checking based analysis
  • Directed model checking using heuristics
  • Parallel or distributed model checking
  • Model checking of timed and probabilistic systems
  • Abstraction and symbolic execution techniques in relation to software verification
  • Static analysis for state space reduction
  • Combinations of enumerative and symbolic techniques
  • Analysis for modeling languages, such as UML/state charts
  • Property specification languages, including new forms of temporal logic
  • Model checking for various programming languages and code analysis
  • Automated testing using state space and/or path exploration techniques
  • Derivation of specifications, test cases, or other useful material from state spaces
  • Combination of model-checking techniques with other analysis techniques
  • Modularity and compositionality
  • Comparative studies, including comparisons with other model-checking techniques
  • Case studies of interesting systems or with interesting results
  • Engineering and implementation of model-checking tools and platforms
  • Benchmarks for software verification

Proceedings

As in previous years, the proceedings of SPIN 2010 will appear in the LNCS series published by Springer.