| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 10329451 | Electronic Notes in Theoretical Computer Science | 2005 | 21 Pages |
Abstract
We present an approach for software model checking based on game semantics and CSP. Open program fragments are compositionally modelled as CSP processes which represent their game semantics. This translation is performed by a prototype compiler. Observational equivalence and verification of properties are checked by traces refinement using the FDR tool. The effectiveness of our approach is evaluated on several examples.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Aleksandar Dimovski, Ranko LaziÄ,