Abstract
Static analyzers like Astrée are incomplete, hence, may produce false alarms. We propose a framework for the investigation of the alarms produced by Astrée , so as to help classifying them as true errors or false alarms that are due to the approximation inherent in the static analysis. Our approach is based on the computation of an approximation of a set of traces specified by an initial and a (set of) final state(s). Moreover, we allow for finer analyses to focus on some execution patterns or on some possible inputs. The underlying algorithms were implemented inside Astrée and used successfully to track alarms in large, critical embedded applications.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Ball, T., Majumdar, R., Millstein, T., Rajamani, S.: Automatic predicate abstraction of C programs. In: PLDI (2001)
Ball, T., Naik, M., Rajamani, S.: From symptom to cause: Localizing errors in counterexample traces. In: POPL (2003)
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A Static Analyzer for Large Safety Critical Software. In: PLDI (2003)
Canfora, G., Cimitille, A., Lucia, A.D.: Condition program slicing. Information and Software Technology; Special issue on Program Slicing (1998)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 752–794. Springer, Heidelberg (2000)
Cousot, P.: Méthodes itératives de construction et d’approximation de points fixes d’opérateurs monotones sur un treillis, analyse sémantique des programmes. PhD thesis (1978)
Cousot, P.: Semantic foundations of program analysis. In: Muchnick, S., Jones, N. (eds.) Program Flow Analysis: Theory and Applications, pp. 303–342. Prentice-Hall, Inc., Englewood Cliffs (1981)
Cousot, P., Cousot, R.: Abstract Interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)
Cousot, P., Cousot, R.: Abstract Interpretation and Application to Logic Programs. Journal of Logic Programming 13(2-3), 103–179 (1992)
Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTRÉE analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21–30. Springer, Heidelberg (2005)
Dor, N., Rodeh, M., Sagiv, M.: CSSV: Towards a realistic tool for statically detecting all buffer overflows in C. In: PLDI (2003)
Erez, G.: Generating counter examples for sound abstract interpretation. Master’s thesis (2004)
Feret, J.: Static analysis of digital filters. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 33–48. Springer, Heidelberg (2004)
Fox, C., Danicic, S., Harman, M., Hierons, R.: ConSIT: A Conditioned Program Slicing System. Software - Practice and Experience (2004)
Gaucher, F., Jahier, E., Jeannet, B., Maraninchi, F.: Automatic state reaching for debugging reactive programs. In: AADEBUG (2003)
Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. Journal of the ACM, 361–416 (2000)
Granger, P.: Improving the results of static analyses programs by local decreasing iteration. In: FSTTCS (1992)
Hierons, R., Harman, M., Fox, C., Ouarbya, L., Daoudi, D.: Conditioned slicing supports partition testing. Journal of Software Testing, Verification and Reliability (2002)
Horwitz, S., Reps, T., Binkley, D.: Interprocedural Slicing using Program Dependence Graphs. In: Programming Languages and Systems (1990)
Jeannet, B.: Dynamic partitioning in linear relation analysis. In: Formal Methods in System Design (2003)
Korel, B., Laski, J.: Dynamic Program Slicing. In: Information Processing Letters (1988)
Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 280–302. Springer, Heidelberg (2000)
Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzers. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 5–20. Springer, Heidelberg (2005)
Miné, A.: Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 3–17. Springer, Heidelberg (2004)
Miné, A.: Weakly relational numerical abstract domains. PhD thesis (2004)
Pace, G., Halbwachs, N., Raymond, P.: Counter-example generation in symbolic abstract model-checking. In: 6th International Workshop on Formal Methods for Industrial Critical Systems, FMICS (2001)
Podelski, A.: Software model checking with abstraction refinement. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 1–3. Springer, Heidelberg (2002)
Venet, A., Brat, G.: Precise and efficient array bound checking for large embedded c programs. In: PLDI (2004)
Weiser, M.: Program slicing. In: Proceeding of the Fifth International Conference on Software Engineering, pp. 439–449 (1981)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rival, X. (2005). Understanding the Origin of Alarms in Astrée . In: Hankin, C., Siveroni, I. (eds) Static Analysis. SAS 2005. Lecture Notes in Computer Science, vol 3672. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11547662_21
Download citation
DOI: https://doi.org/10.1007/11547662_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28584-7
Online ISBN: 978-3-540-31971-9
eBook Packages: Computer ScienceComputer Science (R0)