Module: ppl/w3ppl Branch: master Commit: d6ac343c8a01664da0a95ed69d262bf81f80d13c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=d6ac343c8a0...

Author: Roberto Bagnara bagnara@cs.unipr.it Date: Thu May 7 08:04:15 2009 +0200

Added SenS07TR.

---

htdocs/Documentation/ppl.bib | 27 +++++++++++++++++++++++++++ 1 files changed, 27 insertions(+), 0 deletions(-)

diff --git a/htdocs/Documentation/ppl.bib b/htdocs/Documentation/ppl.bib index 3d81fc5..5a52eec 100644 --- a/htdocs/Documentation/ppl.bib +++ b/htdocs/Documentation/ppl.bib @@ -2322,6 +2322,33 @@ number of static objects being tracked." }

+@Techreport{SenS07TR, + Author = "R. Sen and Y. N. Srikant", + Title = "Executable Analysis with Circular Linear Progressions", + Number = "IISc-CSA-TR-2007-3", + Institution = "Department of Computer Science and Automation, + Indian Institute of Science", + Address = "Bangalore, India", + Year = 2007, + Abstract = "We propose a new abstract domain for static analysis of + executable code. Concrete state is abstracted using + Circular Linear Progressions (CLPs). CLPs model + computations using a finite word length as is seen in + any real life processor. The finite abstraction allows + handling overflow scenarios in a natural and + straight-forward manner. Abstract transfer functions + have been defined for a wide range of operations which + makes this domain easily applicable for analysing code + for a wide range of ISAs. CLPs combine the scalability + of interval domains with the discreteness of linear + congruence domains. We also present a novel, lightweight + method to track linear equality relations between static + objects that is used by the analysis to improve + precision. The analysis is efficient, the total space + and time overhead being quadratic in the number of + static objects being tracked." +} + @Article{Shostak81, Author = "R. E. Shostak", Title = "Deciding Linear Inequalities by Computing Loop Residues",