| Abstract |
|
The verification methodology studied in this paper stems
from investigations on respectively deduction-based model
checking and semantics of concurrency. Specifically, we
consider imperative programs with CSP-like communication
and use a categorical semantics as foundation to extract
from a program a control graph labelled by transition predicates.
This logical content acts as system description for
a deduction-based model checker of LTL properties. We illustrate
the methodology with a concrete realisation in form
of the Mc5 verification tool written in Ocaml and using the
theorem prover PVS as back-end.
|
 Additional Information
|
Citation:
Christoph Sprenger, Krzysztof Worytkiewicz,
"A Verification Methodology for Infinite-State Message Passing Systems,"
memocode,
p. 255,
First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE’03),
2003
|
