Computer Science – Programming Languages
Scientific paper
2007-03-15
Verification, Abstract Interpretation and Model Checking (VMCAI) (01/2006) 348-363
Computer Science
Programming Languages
(update: reversed author first and last names)
Scientific paper
We present lightweight and generic symbolic methods to improve the precison of numerical static analyses based on Abstract Interpretation. The main idea is to simplify numerical expressions before they are fed to abstract transfer functions. An important novelty is that these simplifications are performed on-the-fly, using information gathered dynamically by the analyzer. A first method, called "linearization," allows abstracting arbitrary expressions into affine forms with interval coefficients while simplifying them. A second method, called "symbolic constant propagation," enhances the simplification feature of the linearization by propagating assigned expressions in a symbolic way. Combined together, these methods increase the relationality level of numerical abstract domains and make them more robust against program transformations. We show how they can be integrated within the classical interval, octagon and polyhedron domains. These methods have been incorporated within the Astr\'{e}e static analyzer that checks for the absence of run-time errors in embedded critical avionics software. We present an experimental proof of their usefulness.
No associations
LandOfFree
Symbolic Methods to Enhance the Precision of Numerical Abstract Domains does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Symbolic Methods to Enhance the Precision of Numerical Abstract Domains, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Symbolic Methods to Enhance the Precision of Numerical Abstract Domains will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-363599