Computer Science – Programming Languages
Scientific paper
2010-11-15
Symposium on Automatic Program Verification 2009, informal proceedings (http://se.ethz.ch/apv/program.html)
Computer Science
Programming Languages
15 pages, 8 figures
Scientific paper
Automated software verification is a very active field of research which has made enormous progress both in theoretical and practical aspects. Recently, an important amount of research effort has been put into applying these techniques on top of mainstream programming languages. These languages typically provide powerful features such as reflection, aliasing and polymorphism which are handy for practitioners but, in contrast, make verification a real challenge. In this work we present Pest, a simple experimental, while-style, multiprocedural, imperative programming language which was conceived with verifiability as one of its main goals. This language forces developers to concurrently think about both the statements needed to implement an algorithm and the assertions required to prove its correctness. In order to aid programmers, we propose several techniques to reduce the number and complexity of annotations required to successfully verify their programs. In particular, we show that high-level iteration constructs may alleviate the need for providing complex loop annotations.
Caso Guido de
Garbervetsky Diego
Gorín Daniel
No associations
LandOfFree
Reducing the Number of Annotations in a Verification-oriented Imperative Language does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Reducing the Number of Annotations in a Verification-oriented Imperative Language, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Reducing the Number of Annotations in a Verification-oriented Imperative Language will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-299120