As model checking becomes more integrated into the standard design and verification process for safety-critical systems, the platforms for model checking research have become more limited. Previous options have become closed-source or industry tools; current research platforms don’t have support for expressive specification languages needed for verifying real systems. Our goal is to fill the current gap in model checking research platforms: building a freely available, open-source, scalable model checking infrastructure that accepts expressive models and efficiently interfaces with the currently-maintained state-of-the art back-end algorithms to provide an extensible research and verification tool. We are creating an open, community resource with a well-documented intermediate representation to enable extensibility, and a web portal, facilitating new modeling languages and back-end algorithmic advances.

     This workshop aims to introduce the progress-to-date on this collaborative effort and involve the full international research community to reduce barriers to developing new model-checking algorithms and research platforms. The workshop will include tutorials and feedback from the international Model Checking Technical Advisory Board on a design for an extensible framework centering on an intermediate language that will unify popular front-end modeling languages with state-of the-art back-end model-checking tools. This framework will accept expressive models in higher-level languages, such as SMV, and efficiently interface with back-end model-checking tools to provide an extensible research and verification tool. Adding a new high-level modeling language, e.g., to enable new types of models or re-use of existing benchmarks, will simply require a translation into the intermediate language. Similarly, it will be much easier to compare new back-end model checking algorithms against the full current state-of the-art solutions, and analyze models in a variety of modeling languages, simply by creating a translation between the intermediate language and the new back end.

     As a community, we will discuss performance and efficiency concerns for the proposed new, extensible framework, including avenues for contributing optimizations to the translation algorithms, and adding the ability to utilize safety-specific search algorithms, analyze parametric models, and return finite counterexamples. The workshop will also host discussions and facilitate collaborations on related topics including avenues to increase the utility of SMV as a modeling language, and developing novel extensions of the SMV language that better enable analysis of modern complex systems. We aim to provide a platform for catapulting formal verification efforts in many cutting-edge application areas, including security, networking, operating system, and embedded system verification, as the new framework will make hardware verification problems more accessible.