Cornell University
Library
Cornell UniversityLibrary

eCommons

Help
Log In(current)
  1. Home
  2. Cornell Computing and Information Science
  3. Computer Science
  4. Computer Science Technical Reports
  5. Equational Verification of Cache Blocking in LU Decomposition using Kleene Algebra with Tests

Equational Verification of Cache Blocking in LU Decomposition using Kleene Algebra with Tests

File(s)
2002-1865.ps (156.73 KB)
Permanent Link(s)
https://hdl.handle.net/1813/5848
Collections
Computer Science Technical Reports
Author
Barth, Adam
Kozen, Dexter
Abstract

In a recent paper of Mateev et al. (2001), a new technique for program analysis called fractal symbolic analysis was introduced and applied to verify the correctness of a series of source-level transformations for cache blocking in LU decomposition with partial pivoting. It was argued in that paper that traditional techniques are inadequate because the transformations break definition-use dependencies. We show how the task can be accomplished purely equationally using Kleene algebra with tests.

Date Issued
2002-10-24
Publisher
Cornell University
Keywords
computer science
•
technical report
Previously Published as
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR2002-1865
Type
technical report

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

copyright © 2002-2026 Cornell University Library | Privacy | Web Accessibility Assistance