• Vellvm

  • Referenced in 6 articles [sw13286]
  • Formalizing the LLVM intermediate representation for verified program transformations. This paper presents Vellvm (verified LLVM ... about programs expressed in LLVM’s intermediate representation and transformations that operate on it. Vellvm ... test suite and thus be compared against LLVM reference implementations. To demonstrate Vellvm’s practicality ... implementation of the transformation pass that plugs into the real LLVM infrastructure; its performance...
  • CANAL

  • Referenced in 1 article [sw28166]
  • Cache Timing Analysis Framework via LLVM Transformation. A unified modeling framework for non-functional properties ... program by transforming its intermediate representation in the LLVM compiler. CANAL inserts auxiliary variables...
  • Loopy

  • Referenced in 1 article [sw40305]
  • assembling transformations, while automation and checking prevent errors. Loopy is implemented for the LLVM framework ... show substantial improvements over fully automated loop transformations, using simple and direct specifications...
  • Polly

  • Referenced in 2 articles [sw41994]
  • data-locality optimizer and optimization infrastructure for LLVM. It uses an abstract mathematical representation based ... program. We currently perform classical loop transformations, especially tiling and loop fusion to improve data...
  • Ocelot

  • Referenced in 3 articles [sw09713]
  • that leverages the Low Level Virtual Machine (LLVM) code generator to target x86 and other ... effect on application performance. Several novel code transformations are explored that are applicable only when...
  • Coq

  • Referenced in 1898 articles [sw00161]
  • Coq is a formal proof management system. It...
  • Yices

  • Referenced in 156 articles [sw04436]
  • Yices is an efficient SMT solver that decides...
  • z3

  • Referenced in 603 articles [sw04887]
  • Z3 is a high-performance theorem prover being...
  • LLVM

  • Referenced in 88 articles [sw04892]
  • The LLVM Project is a collection of modular...
  • KLEE

  • Referenced in 45 articles [sw04894]
  • KLEE: Unassisted and Automatic Generation of High-Coverage...
  • ARMC

  • Referenced in 28 articles [sw04949]
  • ARMC: The Logical Choice for Software Model Checking...
  • CeTA

  • Referenced in 47 articles [sw06584]
  • Certification of termination proofs using CeTA. There are...
  • AProVE

  • Referenced in 161 articles [sw07831]
  • AProVE 1.2: Automatic Termination Proofs in the Dependency...
  • UFO

  • Referenced in 23 articles [sw09570]
  • Ufo: A Framework for Abstraction- and Interpolation-Based...
  • SLAyer

  • Referenced in 21 articles [sw09712]
  • SLAyer: Memory Safety for Systems-Level Code. SLAyer...
  • CoLoR

  • Referenced in 38 articles [sw09806]
  • CoLoR: a Coq library on well-founded rewrite...
  • CiME

  • Referenced in 38 articles [sw09970]
  • CiME is a rewriting toolbox. Distributed since 1996...
  • gem5

  • Referenced in 10 articles [sw10707]
  • The gem5 Simulator System. A modular platform for...
  • PAGAI

  • Referenced in 8 articles [sw13095]
  • PAGAI: A Path Sensitive Static Analyser. We describe...