English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Formal verification tools are often developed by experts for experts; as aresult, their usability by programmers with little formal methods experiencemay be severely limited. In this paper, we discuss this general phenomenon withreference to AutoProof: a tool that can verify the full functional correctnessof object-oriented software. In particular, we present our experiences of usingAutoProof in two contrasting contexts representative of non-expert usage.First, we discuss its usability by students in a graduate course on softwareverification, who were tasked with verifying implementations of various sortingalgorithms. Second, we evaluate its usability in verifying code developed forprogramming assignments of an undergraduate course. The first scenariorepresents usability by serious non-experts; the second represents usability on"standard code", developed without full functional verification in mind. Wereport our experiences and lessons learnt, from which we derive some generalsuggestions for furthering the development of verification tools with respectto improving their usability.

The AutoProof Verifier: Usability by Non-Experts and on Standard Code