skip to main content
Explore Scholarly Publications and Datasets in the NSF-PAR

  • Home
  • Search Results
  • Page 1 of 1

Search for: All records

Creators/Authors contains: "Paulsen, Brandon"

Note: When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external site maintained by the publisher. Some full text articles may not yet be available without a charge during the embargo (administrative interval).
What is a DOI Number?

Some links on this page may take you to non-federal websites. Their policies may differ from this site.

  1. ; ( , International Conference on Computer Aided Verification)
    Accepted Manuscript Full Text Available
  2. ; ( , International Conference on Tools and Algorithms for the Construction and Analysis of Systems)
    Full Text Available 
  3. ; ; ; ( , Formal Modeling and Analysis of Timed Systems)
    Full Text Available 
  4. ; ; ( , ACM/IEEE International Conference on Automated Software Engineering)
    A unified modeling framework for non-functional properties of a program is essential for research in software analysis and verification, since it reduces burdens on individual researchers to implement new approaches and compare existing approaches. We present CANAL, a framework that models the cache behaviors of a program by transforming its intermediate representation in the LLVM compiler. CANAL inserts auxiliary variables and instructions over these variables, to allow standard verification tools to handle a new class of cache related properties, e.g., for computing the worst-case execution time and detecting side-channel leaks. We demonstrate the effectiveness of using three verification tools: KLEE, SMACK and Crab-llvm. We confirm the accuracy of our cache model by comparing with CPU cycle-accurate simulation results of GEM5. CANAL is available on GitHub(https://github.com/canalcache/canal) and YouTube(https://youtu.be/JDou3F1j2nY).
    Full Text Available