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

Software model checking techniques can provide the guaranty a system respects a specification. However, some limitations reduce the expressiveness of the most used specification formalisms (the assertions and LTL) and increase the risk of error, especially for concurrent programs. We design a new specification formalism that extends LTL by allowing local variables and code positions in LTL atomic propositions. We introduce validity areas to extend the definition of atomic propositions using local variables and to handle positions in source code. Then, we introduce a source to source transformation that aims to reduce the LTL verification problem to an assertion verification problem for finite programs by building the product between the program code source and the implementation of Büchi automaton. Eventually, we apply this transformation to verify a small benchmark specified with the specification formalism we proposed.

On Handling Source Code Positions and Local Variables in LTL Software Model Checking