| In this project, we aim at specifying and verifying multithreaded object oriented programs. For this we use the formalism of separation Logic . Initial work towards this direction has been led by Parkinson et al. We adapt Parkinson's work to Java's style of parallelism and Java's style of locking. Furthermore, we propose extensions to existing specifications techniques to allow more expressive properties to be specified and verified. |
