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

Stateless Model Checking (SMC) is a verification technique for concurrentprograms that checks for safety violations by exploring all possible threadschedulings. It is highly effective when coupled with Dynamic Partial OrderReduction (DPOR), which introduces an equivalence on schedulings and needexplore only one in each equivalence class. Even with DPOR, SMC often spendsunnecessary effort in exploring loop iterations that are pure, i.e., have noeffect on the program state. We present techniques for making SMC with DPORmore effective on programs with pure loop iterations. The first is a staticprogram analysis to detect loop purity and an associated programtransformation, called Partial Loop Purity Elimination, that inserts assumestatements to block pure loop iterations. Subsequently, some of these assumesare turned into await statements that completely remove many assume-blockedexecutions. Finally, we present an extension of the standard DPOR equivalence,obtained by weakening the conflict relation between events. All thesetechniques are incorporated into a new DPOR algorithm, Optimal-DPOR-Await,which can handle both awaits and the weaker conflict relation, is optimal inthe sense that it explores exactly one execution in each equivalence class, andcan also diagnose livelocks. Our implementation in Nidhugg shows that thesetechniques can significantly speed up the analysis of concurrent programs thatare currently challenging for SMC tools, both for exploring their complete setof interleavings, but even for detecting concurrency errors in them.

Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing Happens