University of Ulm, Faculty of Computer Science, Dept. of Artificial Intelligence up: Publications

Representing, Verifying and Applying Software Development Steps using the PVS System

Axel Dold

Appeared in: Proceedings of the Conference on
Algebraic Methodology and Software Technology (AMAST'95)


 Abstract

In this paper generic software development steps of different complexity are represented and verified using the (higher-order, strongly typed) specification and verification system PVS. The transformations considered in this paper include large powerful steps encoding general algorithmic paradigms as well as smaller transformations for the operationalization of a descriptive specification. The application of these transformation patterns is exemplified by means of simple examples. Furthermore, we show how to guide proofs of correctness assertions about development steps. Finally, this work serves as a case-study and test for the usefulness of the PVS system.

 Online Copy

Available as Postscript (128 KB) or compressed Postscript (48 KB)

 BibTeX Entry

@InProceedings{Dold95,

  author = "Axel Dold",
  title = "Representing, Verifying and Applying Software Development Steps
using the PVS System",
  volume = "936",
  series = "Lecture Notes in Computer Science",
  pages = "431--435",
  booktitle = "Proceedings of the Fourth International Conference on
Algebraic Methodology and Software Technology, AMAST'95, Montreal",
  year = "1995",
  publisher = "Springer-Verlag",
  editor = "V.S. Alagar and Maurice Nivat" }


Dept. of AI Homepage Research Help Mail to Webmaster Axel Dold, Mar 18, 1998