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 Tools annual

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 monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

A rigorous formalization of desired system requirements is indispensable whenperforming any verification task. This often limits the application ofverification techniques, as writing formal specifications is an error-prone andtime-consuming manual task. To facilitate this, we present nl2spec, a frameworkfor applying Large Language Models (LLMs) to derive formal specifications (intemporal logics) from unstructured natural language. In particular, weintroduce a new methodology to detect and resolve the inherent ambiguity ofsystem requirements in natural language: we utilize LLMs to map subformulas ofthe formalization back to the corresponding natural language fragments of theinput. Users iteratively add, delete, and edit these sub-translations to amenderroneous formalizations, which is easier than manually redrafting the entireformalization. The framework is agnostic to specific application domains andcan be extended to similar specification languages and new neural models. Weperform a user study to obtain a challenging dataset, which we use to runexperiments on the quality of translations. We provide an open-sourceimplementation, including a web-based frontend.

nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models