Entry Pugh:1994:CSP from sigplan1990.bib

Last update: Thu Apr 12 03:37:15 MDT 2012                Valid HTML 3.2!

Index sections

Top | Symbols | Numbers | Math | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z

BibTeX entry

@Article{Pugh:1994:CSP,
  author =       "William Pugh",
  title =        "Counting Solutions to {Presburger} Formulas: How and
                 Why",
  journal =      j-SIGPLAN,
  volume =       "29",
  number =       "6",
  pages =        "121--134",
  month =        jun,
  year =         "1994",
  CODEN =        "SINODQ",
  DOI =          "http://doi.acm.org/10.1145/178243.178254",
  ISBN =         "0-89791-598-4",
  ISBN-13 =      "978-0-89791-598-4",
  ISSN =         "0362-1340 (print), 1523-2867 (print), 1558-1160 (electronic)",
  ISSN-L =       "0362-1340",
  bibdate =      "Wed Jun 18 16:26:55 MDT 2008",
  bibsource =    "http://portal.acm.org/;
                 http://www.acm.org/pubs/contents/proceedings/pldi/178243/index.html",
  URL =          "http://www.acm.org:80/pubs/citations/proceedings/pldi/178243/p121-pugh/",
  abstract =     "We describe methods that are able to count the number
                 of integer solutions to selected free variables of a
                 Presburger formula, or sum a polynomial over all
                 integer solutions of selected free variables of a
                 Presburger formula. This answer is given symbolically,
                 in terms of symbolic constants (the remaining free
                 variables in the Presburger formula). For example, we
                 can create a Presburger formula who's solutions
                 correspond to the iterations of a loop. By counting
                 these, we obtain an estimate of the execution time of
                 the loop. In more complicated applications, we can
                 create Presburger formulas who's solutions correspond
                 to the distinct memory locations or cache lines touched
                 by a loop, the flops executed by a loop, or the array
                 elements that need to be communicated at a particular
                 point in a distributed computation. By counting the
                 number of solutions, we can evaluate the
                 computation/memory balance of a computation, determine
                 if a loop is load balanced and evaluate message traffic
                 and allocate message buffers.",
  acknowledgement = ack-nhfb,
  annote =       "Published as part of the Proceedings of PLDI'94.",
  classification = "C4240P (Parallel programming and algorithm theory);
                 C6120 (File organisation)",
  conflocation = "Orlando, FL, USA; 20-24 June 1994",
  conftitle =    "ACM SIGPLAN '94 Conference on Programming Language
                 Design and Implementation (PLDI)",
  corpsource =   "Dept. of Comput. Sci., Maryland Univ., College Park,
                 MD, USA",
  keywords =     "algorithms; buffer storage; cache lines; computational
                 complexity; counting solutions; distinct memory
                 locations; distributed algorithms; distributed
                 computation; distributed distinct memory locations;
                 integer solutions; message buffers; message traffic;
                 Presburger formulas; storage allocation; theory;
                 verification",
  sponsororg =   "ACM",
  subject =      "{\bf F.4.1} Theory of Computation, MATHEMATICAL LOGIC
                 AND FORMAL LANGUAGES, Mathematical Logic. {\bf I.1.0}
                 Computing Methodologies, SYMBOLIC AND ALGEBRAIC
                 MANIPULATION, General. {\bf F.2.1} Theory of
                 Computation, ANALYSIS OF ALGORITHMS AND PROBLEM
                 COMPLEXITY, Numerical Algorithms and Problems,
                 Computations on polynomials. {\bf F.2.1} Theory of
                 Computation, ANALYSIS OF ALGORITHMS AND PROBLEM
                 COMPLEXITY, Numerical Algorithms and Problems,
                 Computations on matrices.",
  treatment =    "T Theoretical or Mathematical",
}

Related entries