SEQ.OPEN: A Tool for Efficient Trace-Based Verification
Hubert Garavel and Radu Mateescu
Proceedings of the 11th International SPIN Workshop on Model Checking of Software SPIN'2004 (Barcelona, Spain), April 2004
We report about recent enhancements of the CADP verification tool set that allow to check the correctness of event traces obtained by simulating or executing complex, industrial-size systems. Correctness properties are expressed using either regular expressions or modal mu-calculus formulas, and verified efficiently on very large traces.
|Slides of H. Garavel's lecture at SPIN'04||(a mistake in slide 3 was corrected in January 2014)|