[TYPES/announce] Call for Model-Checking Community Feedback

[Kristin Yvonne Rozier]

*** Apologies for multiple postings

*********************************************************************
        Webinar & Call for Model-Checking Community Feedback

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

https://urldefense.com/v3/__https://modelchecker.temporallogic.org__;!!IBzWLUs!F_lEA0ENqxxd-vkyRmKq_iBKoFjNLx-vT0yDLsGsAk4d6dzw0JxOXoVbe_iRkk1FTI2z_JB_NCckTg$ 
*********************************************************************

Research Goal:
---------------
This is an NSF (U.S. National Science Foundation)-funded effort to 
develop an open-source, state-of-the-art symbolic model-checking 
framework for the international model-checking research community. 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 will create a 
community resource with a well-documented intermediate representation to 
enable extensibility, and a web portal, facilitating new modeling 
languages and back-end algorithmic advances. To add new modeling 
languages or algorithms, researchers need only to develop a translator 
to/from the new intermediate language, and will then be able to 
integrate each advance with the full state-of-the-art in model checking.


Project Status:
----------------
We have developed a candidate intermediate representation for symbolic 
model checking and revised it via feedback from a Technical Advisory 
Board. We are now ready for wider community feedback to fuel our next 
round of revisions and developments.

Visit our project website for more details, presentation slides, and 
more opportunities to interact, including providing comments, joining 
our mailing list, registering for future webinars, and suggesting names 
for the new framework.


Webinar:
--------

Our first workshop will be held online via zoom:
15 February 2022
1:00pm-3:00pm US-CST (GMT-6)
Registration is at: https://urldefense.com/v3/__https://modelchecker.temporallogic.org__;!!IBzWLUs!F_lEA0ENqxxd-vkyRmKq_iBKoFjNLx-vT0yDLsGsAk4d6dzw0JxOXoVbe_iRkk1FTI2z_JB_NCckTg$ 

Agenda:
15 minutes: Project overview and introduction
45 minutes: Candidate intermediate representation details
60 minutes: Moderated community feedback and questions

*** Additional webinars will be held to accommodate other time-zones; 
please register for a future workshop on the website and provide your 
timezone when asked.


Research Leads:
---------------
Kristin Yvonne Rozier, Iowa State University
Natarajan Shankar, SRI
Cesare Tinelli, University of Iowa
Moshe Y. Vardi, Rice University

-- 
  ____________________________________________________________
                                     __
            /\                       \ \_____
           /  \                   ###[==_____>
          /    \                     /_/      __
         /  __  \                             \ \_____
         | (  ) |                          ###[==_____>
        /| /\/\ |\                            /_/
       / | |  | | \
      /  |=|==|=|  \       Kristin Yvonne Rozier, Ph.D.
    /    | |  | |    \   Black&Veatch Associate Prof, Iowa State Univ
   / USA | ~||~ |NASA \    Departments of Aerospace Engineering,
  |______|  ~~  |______|     Computer Science, Mathematics, and
         (__||__)            Electrical and Computer Engineering
         /_\  /_\          Virtual Reality Applications Center
         !!!  !!!https://urldefense.com/v3/__http://temporallogic.org/kyr__;!!IBzWLUs!F_lEA0ENqxxd-vkyRmKq_iBKoFjNLx-vT0yDLsGsAk4d6dzw0JxOXoVbe_iRkk1FTI2z_JC0iO0BSw$