Software Model Checking Based on Game Semantics and CSP | Zendy

Aleksandar S. Dimovski | Zendy; Ranko Lazić | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Software Model Checking Based on Game Semantics and CSP

Author(s) -

Aleksandar S. Dimovski,

Ranko Lazić

Publication year - 2005

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2005.04.007

Subject(s) - programming language , computer science , model checking , equivalence (formal languages) , semantics (computer science) , compiler , game semantics , theoretical computer science , operational semantics , software , action semantics , denotational semantics , mathematics , discrete mathematics

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

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research