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 recent extensive availability of "big data" platforms calls for a widespread adoption by the formal verification community. Cloud computing platforms represent a great opportunity to run massively parallel jobs, yet classical formal verification tools/techniques must undergo a deep technological transformation in order to exploit the new available architectures. This has raised an increasing interest in deploying verification techniques on parallel/distributed frameworks. In this paper we introduce a framework to ease the adoption of a distributed approach to verification of Computation Tree Logic (CTL) formulas on very large state spaces. The approach exploits/integrates a recently developed, parametric state-space builder. The whole framework adopts M AP R EDUCE as core computational model, and can be tailored to different modelling formalisms. The outcomes of several tests performed on (Petri-nets based) benchmark specifications are presented, thus showing the convenience of the proposed approach.

CTL Model Checking in the Cloud Using MapReduce