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: