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

The automatic verification of programs that maintain unbounded low-level datastructures is a critical and open problem. Analyzers and verifiers developed inprevious work can synthesize invariants that only describe data structures ofheavily restricted forms, or require an analyst to provide predicates overprogram data and structure that are used in a synthesized proof of correctness.  In this work, we introduce a novel automatic safety verifier of programs thatmaintain low-level data structures, named LTTP. LTTP synthesizes proofs ofprogram safety represented as a grammar of a given program's control paths,annotated with invariants that relate program state at distinct points withinits path of execution. LTTP synthesizes such proofs completely automatically,using a novel inductive-synthesis algorithm.  We have implemented LTTP as a verifier for JVM bytecode and applied it toverify the safety of a collection of verification benchmarks. Our resultsdemonstrate that LTTP can be applied to automatically verify the safety ofprograms that are beyond the scope of previously-developed verifiers.

Proofs as Relational Invariants of Synthesized Execution Grammars