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

For all the successes in verifying low-level, efficient, security-criticalcode, little has been said or studied about the structure, architecture andengineering of such large-scale proof developments.  We present the design, implementation and evaluation of a set oflanguage-based techniques that allow the programmer to modularly write andverify code at a high level of abstraction, while retaining control over thecompilation process and producing high-quality, zero-overhead, low-level codesuitable for integration into mainstream software.  We implement our techniques within the F* proof assistant, and specificallyits shallowly-embedded Low* toolchain that compiles to C. Through ourevaluation, we establish that our techniques were critical in scaling thepopular HACL* library past 100,000 lines of verified source code, and broughtabout significant gains in proof engineer productivity.  The exposition of our methodology converges on one final, novel case study:the streaming API, a finicky API that has historically caused many bugs inhigh-profile software. Using our approach, we manage to capture the streamingsemantics in a generic way, and apply it ``for free'' to over a dozenuse-cases. Six of those have made it into the reference implementation of thePython programming language, replacing the previous CVE-ridden code.

Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification