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/

Zendy Plus

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

Zendy Tools

Zendy Open

We present a new approach to automated reasoning about higher-order programsby endowing symbolic execution with a notion of higher-order, symbolic values.Our approach is sound and relatively complete with respect to a first-ordersolver for base type values. Therefore, it can form the basis of automatedverification and bug-finding tools for higher-order programs.  To validate our approach, we use it to develop and evaluate a system forverifying and refuting behavioral software contracts of components in afunctional language, which we call soft contract verification. In doing so, wediscover a mutually beneficial relation between behavioral contracts andhigher-order symbolic execution.  Our system uses higher-order symbolic execution, leveraging contracts as asource of symbolic values including unknown behavioral values, and employs anupdatable heap of contract invariants to reason about flow-sensitive facts.Whenever a contract is refuted, it reports a concrete counterexamplereproducing the error, which may involve solving for an unknown function. Theapproach is able to analyze first-class contracts, recursive data structures,unknown functions, and control-flow-sensitive refinements of values, which areall idiomatic in dynamic languages. It makes effective use of an off-the-shelfsolver to decide problems without heavy encodings. The approach is competitivewith a wide range of existing tools---including type systems, flow analyzers,and model checkers---on their own benchmarks. We have built a tool whichanalyzes programs written in Racket, and report on its effectiveness inverifying and refuting contracts.

Higher-order symbolic execution for contract verification and refutation