Scientific publications

@techreport{SenS07TR,

title = {Executable Analysis with Circular Linear Progressions},

author = {R. Sen and Y. N. Srikant},

year  = {2007},

date = {2007-01-01},

number = {IISc-CSA-TR-2007-3},

address = {Bangalore, India},

institution = {Department of Computer Science and Automation, 

 Indian Institute of Science},

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.},

keywords = {},

pubstate = {published},

tppubtype = {techreport}

}

@techreport{BagnaraHZ07TRb,

title = {An Improved Tight Closure Algorithm 

 for Integer Octagonal Constraints},

author = {R. Bagnara and P. M. Hill and E. Zaffanella},

url = {http://bugseng.com/products/ppl/documentation/BagnaraHZ07TRb.pdf},

year  = {2007},

date = {2007-01-01},

number = {467},

institution = {Dipartimento di Matematica, Università di Parma, Italy},

abstract = {Integer octagonal constraints (a.k.a. emphUnit Two 

 Variables Per Inequality or emphUTVPI integer 

 constraints) constitute an interesting class of 

 constraints for the representation and solution of 

 integer problems in the fields of constraint programming 

 and formal analysis and verification of software and 

 hardware systems, since they couple algorithms having 

 polynomial complexity with a relatively good expressive 

 power. The main algorithms required for the 

 manipulation of such constraints are the satisfiability 

 check and the computation of the inferential closure of 

 a set of constraints. The latter is called emphtight 

 closure to mark the difference with the (incomplete) 

 closure algorithm that does not exploit the integrality 

 of the variables. In this paper we present and fully 

 justify an $O(n^3)$ algorithm to compute the tight 

 closure of a set of UTVPI integer constraints.},

note = {Available at urlhttp://www.cs.unipr.it/Publications/. 

 Also published as tt arXiv:0705.4618v2 [cs.DS], available from urlhttp://arxiv.org/.},

keywords = {},

pubstate = {published},

tppubtype = {techreport}

}

@techreport{BagnaraHZ07TRa,

title = {Applications of Polyhedral Computations to the Analysis 

 and Verification of Hardware and Software Systems},

author = {R. Bagnara and P. M. Hill and E. Zaffanella},

url = {http://bugseng.com/products/ppl/documentation/BagnaraHZ07TRa.pdf},

year  = {2007},

date = {2007-01-01},

number = {458},

institution = {Dipartimento di Matematica, Università di Parma, Italy},

abstract = {Convex polyhedra are the basis for several abstractions 

 used in static analysis and computer-aided verification 

 of complex and sometimes mission critical systems. For 

 such applications, the identification of an appropriate 

 complexity-precision trade-off is a particularly acute 

 problem, so that the availability of a wide spectrum of 

 alternative solutions is mandatory. We survey the range 

 of applications of polyhedral computations in this area; 

 give an overview of the different classes of polyhedra 

 that may be adopted; outline the main polyhedral 

 operations required by automatic analyzers and 

 verifiers; and look at some possible combinations of 

 polyhedra with other numerical abstractions that have 

 the potential to improve the precision of the analysis. 

 Areas where further theoretical investigations can 

 result in important contributions are highlighted.},

note = {Available at urlhttp://www.cs.unipr.it/Publications/. 

 Also published as tt arXiv:cs.CG/0701122, available from urlhttp://arxiv.org/.},

keywords = {},

pubstate = {published},

tppubtype = {techreport}

}

@techreport{BagnaraHZ06TR,

title = {The Parma Polyhedra Library: Toward a Complete Set of Numerical 

 Abstractions for the Analysis and Verification 

 of Hardware and Software Systems},

author = {R. Bagnara and P. M. Hill and E. Zaffanella},

url = {http://bugseng.com/products/ppl/documentation/BagnaraHZ06TR.pdf},

year  = {2006},

date = {2006-01-01},

number = {457},

institution = {Dipartimento di Matematica, Università di Parma, Italy},

abstract = {Since its inception as a student project in 2001, 

 initially just for the handling (as the name implies) of 

 convex polyhedra, the emphParma Polyhedra Library has 

 been continuously improved and extended by joining 

 scrupulous research on the theoretical foundations of 

 (possibly non-convex) numerical abstractions to a total 

 adherence to the best available practices in software 

 development. Even though it is still not fully mature 

 and functionally complete, the Parma Polyhedra Library 

 already offers a combination of functionality, 

 reliability, usability and performance that is not 

 matched by similar, freely available libraries. In this 

 paper, we present the main features of the current 

 version of the library, emphasizing those that 

 distinguish it from other similar libraries and those 

 that are important for applications in the field of 

 analysis and verification of hardware and software 

 systems.},

note = {Available at urlhttp://www.cs.unipr.it/Publications/. 

 Also published as tt arXiv:cs.MS/0612085, available from urlhttp://arxiv.org/.},

keywords = {},

pubstate = {published},

tppubtype = {techreport}

}