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 Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

We propose a novel technique (TOUR) to improve both bug detection ability and verification speed of ARMC by detecting a target path quickly. The key idea of TOUR is an <italic>error location directed search</italic> that utilizes <italic>the distance to an error location</italic> and <italic>function call context</italic> at runtime. TOUR applies four different distance metrics and a distance metric selection heuristic using static features of a target program. We have extensively evaluated TOUR on 3,042 real-world C programs in a software verification competition benchmark. The experiment results show that TOUR, due to its error location directed search, finds bugs in 20&#x0025; more programs in 11&#x0025; less model checking time than the state-of-the-art ARMC technique (i.e., block-abstraction memoization) for 354 buggy programs. Also, TOUR verifies 15&#x0025; more programs within 15&#x0025; less model checking time than the block-abstraction memoization for 652 <italic>complex</italic> clean programs.

Directed Model Checking for Fast Abstract Reachability Analysis