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 Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Formal verification techniques aim at formally proving the correctness of acomputer program with respect to a formal specification, but the expertise andeffort required for applying formal specification and verification techniquesand scalability issues have limited their practical application. In recentyears, the tremendous progress with SAT and SMT solvers enabled theconstruction of a new generation of tools that promise to make formalverification more accessible for software engineers, by automating most if notall of the verification process. The Dafny system is a prominent example ofthat trend. However, little evidence exists yet about its accessibility. Tohelp fill this gap, we conducted a set of 10 case studies of developingverified implementations in Dafny of some real-world algorithms and datastructures, to determine its accessibility for software engineers. We foundthat, on average, the amount of code written for specification and verificationpurposes is of the same order of magnitude as the traditional code written forimplementation and testing purposes (ratio of 1.14) -- an ``overhead'' thatcertainly pays off for high-integrity software. The performance of the Dafnyverifier was impressive, with 2.4 proof obligations generated per line of codewritten, and 24 ms spent per proof obligation generated and verified, onaverage. However, we also found that the manual work needed in writingauxiliary verification code may be significant and difficult to predict andmaster. Hence, further automation and systematization of verification tasks arepossible directions for future advances in the field.

Case studies of development of verified programs with Dafny for accessibility assessment