Lecture Notes in Computer Science, 2007, Volume 4600/2007, 235-258, DOI: 10.1007/978-3-540-73147-4_12

Towards Modular Algebraic Specifications for Pointer Programs: A Case Study

Claude Marché

View Related Documents

Abstract

We present on an example the framework currently under development in the Why/Krakatoa/Caduceus platform for proving that a Java or a C program is a correct implementation of some model defined by algebraic specifications, in a modular setting.

Fulltext Preview

Image of the first page of the fulltext document