Computer Science – Software Engineering
Scientific paper
2011-06-23
Computer Science
Software Engineering
Accepted at BOOGIE 2011
Scientific paper
Static program verifiers such as Spec#, Dafny, jStar, and VeriFast define the state of the art in automated functional verification techniques. The next open challenges are to make verification tools usable even by programmers not fluent in formal techniques. This paper presents AutoProof, a verification tool that translates Eiffel programs to Boogie and uses the Boogie verifier to prove them. In an effort to be usable with real programs, AutoProof fully supports several advanced object-oriented features including polymorphism, inheritance, and function objects. AutoProof also adopts simple strategies to reduce the amount of annotations needed when verifying programs (e.g., frame conditions). The paper illustrates the main features of AutoProof's translation, including some whose implementation is underway, and demonstrates them with examples and a case study.
Furia Carlo A.
Meyer Bertrand
Nordio Martin
Tschannen Julian
No associations
LandOfFree
Verifying Eiffel Programs with Boogie 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 Verifying Eiffel Programs with Boogie, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Verifying Eiffel Programs with Boogie will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-469861