C.OPEN and ANNOTATOR: Tools for On-the-Fly Model Checking C Programs

This paper describes a set of verification components that open the way to perform on-the-fly software model checking with the Cadp toolbox, originally designed for verifying the functional correctness of Lotos specifications. Two new tools (named C.Open and Annotator) have been added to the toolbox. The approach taken fits well within the existing architecture of Cadp which doesn’t need to be altered to enable C program verification.

• Type: Conference
• Year: 2007
• Where: SPIN
• Authors: María-del-Mar Gallardo, Christophe Joubert, Pedro Merino, David Sanán
• Keywords: Approach Taken fits, Cadp Toolbox, On-the-fly Software Model, SPIN 2007, Theoretical Computer Science