Entry Reps:2010:FDL from toplas.bib

Last update: Tue May 1 02:05:46 MDT 2012                Valid HTML 3.2!

Index sections

Top | Symbols | 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{Reps:2010:FDL,
  author =       "Thomas Reps and Mooly Sagiv and Alexey Loginov",
  title =        "Finite differencing of logical formulas for static
                 analysis",
  journal =      j-TOPLAS,
  volume =       "32",
  number =       "6",
  pages =        "24:1--24:55",
  month =        aug,
  year =         "2010",
  CODEN =        "ATPSDT",
  DOI =          "http://doi.acm.org/10.1145/1749608.1749613",
  ISSN =         "0164-0925 (print), 1558-4593 (electronic)",
  ISSN-L =       "0164-0925",
  bibdate =      "Wed Sep 8 18:52:47 MDT 2010",
  bibsource =    "http://www.acm.org/pubs/contents/journals/toplas/;
                 http://www.math.utah.edu/pub/tex/bib/toplas.bib",
  abstract =     "This article concerns mechanisms for maintaining the
                 value of an instrumentation relation (also known as a
                 {\em derived relation\/} or {\em view\/}), defined via
                 a logical formula over core relations, in response to
                 changes in the values of the core relations. It
                 presents an algorithm for transforming the
                 instrumentation relation's defining formula into a {\em
                 relation-maintenance formula\/} that captures what the
                 instrumentation relation's new value should be. The
                 algorithm runs in time linear in the size of the
                 defining formula.\par

                 The technique applies to program analysis problems in
                 which the semantics of statements is expressed using
                 logical formulas that describe changes to core relation
                 values. It provides a way to obtain values of the
                 instrumentation relations that reflect the changes in
                 core relation values produced by executing a given
                 statement.\par

                 We present experimental evidence that our technique is
                 an effective one: for a variety of benchmarks, the
                 relation-maintenance formulas produced automatically
                 using our approach yield the same precision as the best
                 available hand-crafted ones.",
  acknowledgement = ack-nhfb,
  articleno =    "24",
  fjournal =     "ACM Transactions on Programming Languages and
                 Systems",
  keywords =     "3 - valued logic; Abstract interpretation; finite
                 differencing; materialized view; shape analysis; static
                 analysis",
}

Related entries