Third Workshop on
Model Checking and Artificial Intelligence
MoChArt '05

August 27, 2005 - San Francisco, CA, USA
co-located with CONCUR 2005 and SPIN 2005

Register early!  
Before July 20 at the CONCUR '05 website (mirror)

Preliminary Programme

Instructions to Authors

Announcement and Call For Papers

Aim and Scope

Exploration of very large search spaces is at the heart of many disciplines of computer science and engineering, and formal verification and artificial intelligence in particular.  On one hand, model checking (MC) is used to automatically verify logical properties over a model of a system, and MC procedures for many classes of models and logics of interest have been efficiently automated and successfully applied to a broad range of real-size applications in the last decade. These recent advances have lead to a growth of interest in the use of MC principles and tools in Artificial Intelligence (AI).  In the meantime, the AI community has had a long and impressive line of research in developing and improving search algorithms over very large state spaces under a broad range of assumptions. MC researchers are interested in leveraging this vast body of knowledge, as a way to mitigate the state-space explosion problem. Under a slightly different perspective, there is also a demand for innovative verification approaches, such as model checking, for AI applications.  This is becoming a critical need, as AI technologies are increasingly considered for safety-critical applications such as space missions. AI software typically features unconventional architectures and requirements that ask for specific verification solutions. All these trends call for an increased dialogue between the AI and V&V communities.

The purpose of the MoChArt workshop series is therefore to bring together researchers with an interest in both MC and AI. The goals are to tease out common themes and differences, identify common problems and their solutions, share experiences with the applicability of techniques from one field to problems from the other, and to identify the key issues to be addressed in increasing the convergence between MC and AI. The workshop will welcome submissions on all ideas, research, experiments and tools that relate to both MC and AI fields.

MoChArt '05 follows on two very lively and productive editions: MoChArt '02 in Lyon (associated to ECAI) and MoChArt '03 in Acapulco (associated to IJCAI), both coupled to artificial intelligence conferences.  This time, MoChArt '05 will be co-located with two major international events in the field of formal verification: the 16th International Conference on Concurrency Theory (CONCUR 2005) and the 12th International SPIN Workshop on Model Checking of Software (SPIN 2005).  The event will be held at the Stanford Court Hotel in San Francisco, CA.

Registration and Participation

The workshop will take place in the Russian Room of the Stanford Court Hotel.

Participation will be open to all, but limited to available seating (30 seats). Priority will be given to authors of presented papers and participants of past MoChArt events. Registration to CONCUR 2005 and/or SPIN 2005 is not required to attend the workshop (though we strongly recommend not to miss the opportunity). 

Participants should register through the website of the CONCUR '05 conference (mirror). Registration fees for this workshop will be 125 USD (early) / 140 USD (late), including participant's proceedings, lunch and coffee breaks. Early registration ends on July 20th, 2005.

The proceedings of the workshop will be published electronically by Elsevier as a volume of Electronic Notes in Theoretical Computer Science (Editor's site).  The volume should be available before the workshop begins.  A hardcopy will be distributed to workshop participants. 

Please contact Charles Pecheur for any additional information:

Charles Pecheur
UCL, Dept. Computing Science and Engineering
Place Sainte Barbe 2
1348 Louvain La Neuve
Phone: +32-10-47 87 79

Last updated July 8, 2005 – Curator: Charles Pecheur