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

Verification of large and complicated concurrent programs is an importantissue in the software world. Stateless model checking is an appropriate methodfor systematically and automatically testing of large programs, which hasproved its power in verifying code of large programs. Another well-known methodin this area is runtime verification. Both stateless model checking and runtimeverification are similar in some ways. One common approach in runtimeverification is to construct runtime monitors for properties expressed inlinear temporal logic. Currently, there are some semantics to check lineartemporal logic formulae on finite paths proposed in the field of runtimeverification, which can also be applied to stateless model checking. However,existing stateless model checkers do not support LTL formulae. In somesettings, it is more advantageous to make use of stateless model checkinginstead of runtime verification. This paper proposes a novel encoding of one ofthe recent LTL semantics on finite paths into an actor-based system. We take atruly parallel approach without saving any program states or traces, which notonly addresses important problems in runtime verification, but can also beapplied to stateless model checking.

A New Approach to Stateless Model Checking of LTL Properties