Computer-Supported Assessment of Software Verification Proofs

Most conventional e-assessment systems are not suited for examining analytic, creative and constructive skills and the few existing ones have too limited functionality to appropriately support Computer Science assessments. On this account the e-assessment system EASy has been developed which e.g. provides relevant exercise modules for Computer Science tasks. Recently the system has been extended by a module for the computer-supported examination of software verification proofs based on the Hoare Logic. In this work we discuss this module and evaluate its applicability, usability and acceptance in terms of a lecture on Formal Specification.