Module: ppl/ppl Branch: master Commit: 2f1203b99f97684a6c7b52747fe785595b421940 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2f1203b99f976...
Author: Patricia Hill patricia.hill@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, }
+@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." }
+@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." }
+@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",