Conventional e assessment systems often are not suited for examining analytic, creative and constructive skills, and the few existing ones have very limited functionality. On this account the e assessment system EASy, which focuses on the examination of formative assessments, has been developed. Besides exercise modules for multiple-choice questions, programming exercises and mathematical proofs the system recently offers a module for the computer-supported examination of software verification proofs based on the Hoare Logic. In this work we discuss the module for automated assessment of these proofs. To demonstrate the feasibility of our approach, the applicability, usability and acceptance of the Hoare-Logic module have been evaluated in a lecture on formal specification.

Usener, C. A., Gruttmann, S., Majchrzak, T. A. and Kuchen, H.: Formative E-Assessment of Software Verification Skills in Higher Education. In: Proc. of the IADIS Int. Conf. e-Learning 2010 (eL2010), IADIS Press (2010)