CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Interactive Verification of JCSP Programs

Philipp Rümmer (Institutionen för data- och informationsteknik, Datavetenskap (Chalmers))
Göteborg : Chalmers University of Technology, 2005. - 232 pages s.
[Rapport]

The foundations of a verification system for concurrent Java programs written using the JCSP library are defined and investigated. To this end, the semantics of JCSP is modelled using the CSP process algebra (this step is only sketched here), and concurrent programs are composed from sequential ones. In order to obtain a deduction system, a calculus based on a structural operational semantics of sequential Java---originally used for JavaCard Dynamic Logic---is combined with a rewriting system for CSP. The present document concentrates on the latter rewriting system and introduces an extension of CSP that enables efficient symbolic execution.



Denna post skapades 2006-08-25. Senast ändrad 2013-08-12.
CPL Pubid: 3263