AutoProof Meets Some Verification Challenges

AutoProof is a verifier for Eiffel programs. Even though we did not participate in the FM 2012 verification challenge on site, we did solve the challenges with AutoProof later on. The results have been published in a special section on Program Verification in the International Journal on Software Tools for Technology Transfer (STTT).

The publication is available as a PDF file.

Verification Challenges

The verification challenge consisted of three problems:

• Longest Common Prefix: given an integer array and two indices into the array, return the length of the longest prefix starting at those two indeces.
  AutoProof solution of LCP.
• Prefix Sum: given an integer array a, calculate the prefix sum for each array position using a specific in-place algorithm.
  AutoProof solution of Prefix Sum.
• Tree Deletion: given a binary tree, use a specific algorithm to delete the minimum value.
  AutoProof solution of Tree Deletion.