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.

6 pages


Slides of H. Garavel's lecture at SPIN'04
(a mistake in slide 3 was corrected in January 2014)