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

One of the main challenges when verifying multi-threaded Java applications isthe state space explosion problem. Due to thread interleavings, the number ofstates that the model checker has to verify can grow rapidly and impede thefeasibility of verification. In the Java language, the source of threadinterleavings can be the system under test as well as the Java Development Kit(JDK) itself. In our paper, we propose a method to minimize the state spaceexplosion problem for applications verified under the Java PathFinder (JPF)model checker. Our method is based on abstracting the state of the applicationto a smaller domain and implementing application behavior using the Model JavaInterface (MJI) of JPF. To show the capabilities of our approach, we havecreated a JPF extension called jpf-concurrent which abstracts classes from theJava Concurrency Utilities. Several benchmarks proved the usefulness of ourapproach. In all cases, our implementation was faster than the JDKimplementation when running under the JPF model checker. Moreover, ourimplementation led to significantly smaller state spaces.

jpf-concurrent: An extension of Java PathFinder for java.util.concurrent