[PPL-devel] [GIT] ppl/ppl(master): More references added.
Patricia Hill
patricia.hill at bugseng.com
Sat Dec 28 14:01:24 CET 2013
Module: ppl/ppl
Branch: master
Commit: 2f1203b99f97684a6c7b52747fe785595b421940
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2f1203b99f97684a6c7b52747fe785595b421940
Author: Patricia Hill <patricia.hill at bugseng.com>
Date: Sat Dec 28 13:00:59 2013 +0000
More references added.
---
doc/ppl.bib | 34 +++++++++++++++++++++++++++++
doc/ppl_citations.bib | 57 +++++++++++++++++++++++++++++++++++++++++++++++++
2 files changed, 91 insertions(+), 0 deletions(-)
diff --git a/doc/ppl.bib b/doc/ppl.bib
index cbb16bb..bc5a897 100644
--- a/doc/ppl.bib
+++ b/doc/ppl.bib
@@ -1967,6 +1967,40 @@ Summarizing:
Year = 1994,
}
+ at InCollection{KapurZHZLN13,
+ Author = "D. Kapur and Z. Zhang and M. Horbach and H. Zhao and Q. Lu and T. Nguyen",
+ Title = "Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants",
+ Booktitle = "Automated Reasoning and Mathematics:
+ Essays in Memory of William W. McCune",
+ Editor = "M. P. Bonacina and M. E. Stickel",
+ Publisher = "Springer-Verlag, Berlin",
+ Series = "Lecture Notes in Computer Science",
+ Volume = 7788,
+ Pages = "189--228",
+ Year = 2013,
+ ISBN = "978-3-642-36674-1 (Print) 978-3-642-36675-8 (Online)"
+ Abstract = "Geometric heuristics for the quantifier elimination
+ approach presented by Kapur (2004) are investigated to
+ automatically derive loop invariants expressing weakly
+ relational numerical properties (such as l =< x =< h or
+ l =< +/- x +/- y =< h) for imperative programs. Such properties
+ have been successfully used to analyze commercial
+ software consisting of hundreds of thousands of lines of
+ code (using for example, the Astr\'ee tool based on
+ abstract interpretation framework proposed by Cousot and
+ his group). The main attraction of the proposed approach
+ is its much lower complexity in contrast to the abstract
+ interpretation approach (O(n^2) in contrast to O(n^4),
+ where n is the number of variables) with the ability to
+ still generate invariants of comparable strength. This
+ approach has been generalized to consider disjunctive
+ invariants of the similar form, expressed using maximum
+ function (such as max (x + a,y + b,z + c,d) ≤ max
+ (x + e,y + f,z + g,h)), thus enabling automatic
+ generation of a subclass of disjunctive invariants for
+ imperative programs as well."
+}
+
@Article{KhachiyanBBEG06,
Author = "L. Khachiyan and E. Boros and K. Borys
and K. Elbassioni and V. Gurvich",
diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib
index cdbf314..e6e4f6f 100644
--- a/doc/ppl_citations.bib
+++ b/doc/ppl_citations.bib
@@ -1087,6 +1087,33 @@ Summarizing:
hypersurfaces) are computed."
}
+ at Article{BrauerKK13,
+ Author = "J. Brauer and A King. and S. Kowalewski",
+ Title = "Abstract interpretation of microcontroller code: Intervals meet congruences",
+ Journal = "Science of Computer Programming",
+ Volume = 78,
+ Number = "7",
+ Pages = "862--883",
+ Year = 2006,
+ Publisher = "Elsevier North-Holland, Inc.",
+ Address = "Amsterdam, The Netherlands",
+ ISSN = "0167-6423",
+ Abstract = "Bitwise instructions, loops and indirect data access
+ present challenges to the verification of
+ microcontroller programs. In particular, since registers
+ are often memory mapped, it is necessary to show that an
+ indirect store operation does not accidentally mutate a
+ register. To prove this and related properties, this
+ article advocates using the domain of bitwise linear
+ congruences in conjunction with intervals to derive
+ accurate range information. The paper argues that these
+ two domains complement one another when reasoning about
+ microcontroller code. The paper also explains how SAT
+ solving, which applied with dichotomic search, can be
+ used to recover branching conditions from binary code
+ which, in turn, further improves interval analysis."
+}
+
@Inproceedings{BrihayeDGQRW13,
Author = "T. Brihaye and L. Doyen and G. Geeraerts and J. Ouaknine and J.-F. Raskin and J. Worrell",
Title = "Time-Bounded Reachability for Monotonic Hybrid Automata: Complexity and Fixed Points",
@@ -2954,6 +2981,36 @@ Summarizing:
techniques."
}
+ at Article{Jakubczy12k,
+ Author = "K. Jakubczyk",
+ Title = "Sweeping in Abstract Interpretation",
+ Journal = "Electronic Notes in Theoretical Computer Science ({ENTCS})",
+ Publisher = "Elsevier Science Publishers B. V.",
+ Address = "Amsterdam, The Netherlands",
+ Volume = 288,
+ Pages = "25--36",
+ Year = 2012,
+ ISSN = "1571-0661",
+ Abstract = "In this paper we present how sweeping line techniques,
+ which are very popular in computational geometry, can be
+ adapted for static analysis of computer software by
+ abstract interpretation. We expose how concept of the
+ sweeping line can be used to represent elements of a
+ numerical abstract domain of boxes, which is a
+ disjunctive refinement of a well known domain of
+ intervals that allows finite number of disjunctions. We
+ provide a detailed description of the representation
+ along with standard domain operations
+ algorithms. Furthermore we introduce very precise
+ widening operator for the domain. Additionally we show
+ that the presented idea of the representation based on
+ sweeping line technique is a generalisation of the
+ representation that uses Linear Decision Diagrams (LDD),
+ which is one of possible optimisations of our idea. We
+ also show that the presented widening operator is often
+ more precise than the previous one."
+}
+
@Article{JhalaM09,
Author = "R. Jhala and R. Majumdar",
Title = "Software Model Checking",
More information about the PPL-devel
mailing list