July
23rd
2024

The OSSyM 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.

Open-Source, State-of-the-Art
Symbolic Model-Checking Framework
for the Model-Checking Research Community

Technical Information

     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.

The OSSyM Workshop is part of

CAV 2024

36th International Conference on Computer Aided Verification

from July 22-27, 2024, at Concordia University, Montreal, Canada

Workshop Agenda

Duration
Speaker
Event
1 hr
Kristin Yvonne Rozier
Introduction, Background, Project Overview, Workshop Goals, Agenda
Break
Break
Break
1.5 hr
Cesare Tinelli
Model Checking MoXI Tutorial
30 mins
CCRI Investigators
Language Demo, Audience Interaction, Q&A
Lunch
Lunch
Lunch
2 hr
TAB
10-15 minute talks by advisory board members:
-Aarti Gupta (Princeton University)
-Alberto Griggio (FBK)
-Arie Gurfinkel (University of Waterloo)
Break
Break
Break
45 mins
CCRI Investigators
Panel: PIs and advisory board members conduct moderated discussion and respond to questions/feedback from international research community
1 hr
Natarajan Shankar
Demo from SRI team (Shankar and PhD students) of PVS2C implementation and existing translations to/from model checking intermediate language

Organizational Information

Main Contact for the Workshop

Kristin Yvonne Rozier

Workshop Chair
Iowa State University
kyrozier@iastate.edu

Contact Information of the Workshop Organizers

• Kristin Yvonne Rozier, Iowa State University, kyrozier@iastate.edu

• Natarajan Shankar, SRI International, shankar@csl.sri.com

• Cesare Tinelli, University of Iowa, cesare-tinelli@uiowa.edu

• Moshe Y. Vardi, Rice University, vardi@cs.rice.edu