Software

APEX: A verification tool for probabilistic programs.
See also this paper, this paper, and this paper.
SLAP: A static livelock analyser for CSP processes (now bundled within FDR).
See also this paper, this paper, and this paper.
MAGIC: A model checker for sequential and concurrent C programs.
See also this paper, this paper, this paper, this paper, this paper, this paper, and this paper.

I have also contributed to:

UCLID: A verification tool for infinite-state systems.
(Implemented by S. K. Lahiri and S. A. Seshia.)
See also this paper, this paper, and this paper.

Back to Joel Ouaknine's home page
Last updated in April 2011