<%@ page language="java" contentType="text/html" %>
<%-- Include common initialisation code --%>
<%@ include file="/arch/common.jsp" %>
<%-- The current tab --%>
<% String currentTab = "Research"; %>
<%-- Content of navigation pane --%>
<%@ include file="nav.jsp" %>
<% showCurrentLink=true; %>
<%-- Current navigation location --%>
<% String currentNav = "Reports and Theses"; %>
<%-- Include the code for the document header --%>
<%@ include file="/arch/header.jsp" %>
Research Report CS-RR-403
<%-- Include the code for the lines and navigation --%>
<%@ include file="/arch/middle.jsp" %>
Aleksandar Dimovski and Ranko Lazic,
Software Model Checking Based on Game Semantics and CSP
(August 11, 2004; revised 2 September 2004).
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. Effectiveness of our approach is evaluated on several examples.
Download
cs-rr-403.ps.gz
<%-- Include the code for the document footer --%>
<%@ include file="/arch/footer.jsp" %>