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

A unified modeling framework for non-functional properties of a program isessential for research in software analysis and verification, since it reducesburdens on individual researchers to implement new approaches and compareexisting approaches. We present CANAL, a framework that models the cachebehaviors of a program by transforming its intermediate representation in theLLVM compiler. CANAL inserts auxiliary variables and instructions over thesevariables, to allow standard verification tools to handle a new class of cacherelated properties, e.g., for computing the worst-case execution time anddetecting side-channel leaks. We demonstrate the effectiveness of CANAL usingthree verification tools: KLEE, SMACK and Crab-llvm. We confirm the accuracy ofour cache model by comparing with CPU cycle-accurate simulation results ofGEM5. CANAL is available on GitHub and YouTube.

CANAL: A Cache Timing Analysis Framework via LLVM Transformation