Abstract
We show that the precision of static abstract software checking algorithms can be enhanced by taking explicitly into account the abstractions that are involved in the design of the program model/abstract semantics. This is illustrated on reachability analysis and abstract testing.
This work was supported in part by the RTD project IST-1999-20527 Daedalus of the european IST FP5 programme.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Cousot, P., Cousot, R.: Temporal abstract interpretation. In: 27th POPL, Boston, USA, ACM Press (2000) 12–25
Schmidt, D.: From trace sets to modal-transition systems by stepwise abstract interpretation. Submitted for publication (2001)
Cousot, P.:Méthodes itératives de construction et d’approximation de points fixes d’opérateurs monotones sur un treillis, analyse sémantique de programmes. Thèse d’État ès sciences mathématiques, Université scientifique et médicale de Grenoble, Grenoble, France (1978)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: 6th POPL, San Antonio, USA, ACM Press (1979) 269–282
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4 th POPL, Los Angeles,USA, ACM Press (1977) 238–252
Cousot, P.: Semantic foundations of program analysis. In Muchnick, S., Jones, N., eds.: Program Flow Analysis: Theory and Applications. Prentice-Hall (1981) 303–342
Bourdoncle, F.: Abstract debugging of higher-order imperative languages. In: Proc. ACM SIGPLAN’93 Conf. PLDI. ACM SIGPLAN Not. 28(6), Albuquerque,USA, ACM Press (1993) 46–55
Cousot, P., Cousot, R.: Induction principles for proving invariance properties of programs. In Néel, D., ed.: Tools & Notions for Program Construction. Cambridge U. Press (1982) 43–119
Clarke, E., Emerson, E.: Synthesis of synchronization skeletons for branching time temporal logic. In: IBM Workshop on Logics of Programs. Yorktown Heights, USA, LNCS 131, Springer-Verlag (1981)
Clarke, E., Emerson, E., Sistla, A.: Automatic verification of finite-state concurrent systems using temporal logic specifications. TOPLAS 8 (1986) 244–263
Queille, J.P., Sifakis, J.: Verification of concurrent systems in Cesar. In: Proc. Int. Symp. on Programming. LNCS 137. Springer-Verlag (1982) 337–351
Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.: Symbolic model checking: 1020 states and beyond. Inform. and Comput. 98 (1992) 142–170
Biere, A., Cimatti, A., Clarke, E., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Proc. 36th Conf. DAC’ 99. New Orleans, USA. ACM Press (21–25 June 1999) 317–320
Cousot, P., Cousot, R.: Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, invited paper. In Bruynooghe, M., Wirsing, M., eds.: Proc. 4 th Int. Symp. PLILP’ 92. Leuven, Belgium, 26–28 Aug. 1992, LNCS 631, Springer-Verlag (1992) 269–295
Cousot, P.: Partial completeness of abstract fixpoint checking, invited paper. In Choueiry, B., Walsh, T., eds.: Proc. 4 th Int. Symp. SARA’2000. Horseshoe Bay, USA, LNAI 1864. Springer-Verlag (2000) 1–25
Clarke, E., Grumberg, O., Long, D.: Model checking and abstraction. TOPLAS 16 (1994) 1512–1542
Cleaveland, R., Iyer, P., Yankelevitch, D.: Optimality in abstractions of model checking. In Mycroft, A., ed.: Proc. 2 nd Int. Symp. SAS’95. Glasgow, UK, 25–27 Sep. 1995, LNCS 983. Springer-Verlag (1995) 51–63
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: 5 th POPL, Tucson, USA, ACM Press (1978) 84–97
Halbwachs, N.: About synchronous programming and abstract interpretation. Sci. Comput. Programming 31 (1998) 75–89
Graf, S., Loiseaux, C.: A tool for symbolic program verification and abstraction. In Courcoubetis, C., ed.: Proc. 5 th Int. Conf. CAV’ 93. Elounda, Grece, LNCS 697, Springer-Verlag (1993) 71–84
Katoen, J.P., Stevens, P., eds.: Relative Completeness of Abstraction Refinement for Software Model Checking. In Katoen, J.P., Stevens, P., eds.: Proc. 8 th Int. Conf. TACAS’ 2002. Grenoble, France, LNCS 2280, Springer-Verlag (2002)
Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. ACM 47 (2000) 361–416
Karr, M.: Affine relationships among variables of a program. Acta Informat. 6 (1976) 133–151
Cousot, P., Cousot, R.: Systematic design of program transformation frameworks. In: 29th POPL, Portland, USA, ACM Press (2002) 178–190
Cousot, P.: The Marktoberdorf’98 generic abstract interpreter. http://www.di.ens.fr/~cousot/Marktoberdorf98.shtml (1998)
Cousot, P.: Calculational design of semantics and static analyzers by abstract interpretation. NATO Int. Summer School 1998 on Calculational System Design. Marktoberdorf, DE. Organized by F.L. Bauer, M. Broy, E.W. Dijkstra, D. Gries and C.A.R. Hoare. (1998)
Cousot, P., Cousot, R.: Refining model checking by abstract interpretation. Aut. Soft. Eng. 6 (1999) 69–95
Berezin, S., Clarke, E., Jha, S., Marrero, W.: Model checking algorithms for the μ-calculus. Tech. rep. tr-cmu-cs-96-180, Carnegie Mellon University, USA, (1996)
Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. J. Logic Programming 13 (1992) 103–179 (The editor of J. Logic Programming has mistakenly published the unreadable galley proof. For a correct version of this paper, see http://www.di.ens.fr/~cousot.).
Kaplan, M., Ullman, J.: A general scheme for the automatic inference of variable types. J. ACM 27 (1980) 128–145
Massé, D.: Combining forward and backward analyzes of temporal properties. In Danvy,., Filinski, A., eds.: Proc. 2 nd Symp. PADO’2001. Århus, Danmark, 21–23 May 2001, LNCS 2053, Springer-Verlag (2001) 155–172
Granger, P.: Improving the results of static analyses of programs by local decreasing iterations. In Shyamasundar, R., ed.: Proc. 12th FST & TCS. New Delhi, India, 18–20 Dec. 1992, LNCS 652, Springer-Verlag (1992) 68–79
Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In Emerson, E., Sistla, A., eds.: Proc. 12th Int. Conf. CAV’00. Chicago, USA, LNCS 1855, SPRINGER (2000) 154–169
Giacobazzi, R., Quintarelli, E.: Incompleteness, counterexamples and refinements in abstract model-checking. In Cousot, P., ed.: Proc. 8 th Int. Symp. SAS’ 01. Paris, France, LNCS 2126, Springer-Verlag (2001) 356–373
Ferdinand, C., Heckmann, R., Langenbach, M., Martin, F., Schmidt, M., Theiling, H., Thesing, S., Wilhelm, R.: Reliable and precise WCET determination for a real-life processor. In Henzinger, T., Kirsch, C., eds.: Proc. 1st Int. Workshop ESOP’2001. Volume 2211 of LNCS. Springer-Verlag (2001) 469Ñ-485
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cousot, P., Cousot, R. (2002). On Abstraction in Software Verification. In: Brinksma, E., Larsen, K.G. (eds) Computer Aided Verification. CAV 2002. Lecture Notes in Computer Science, vol 2404. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45657-0_3
Download citation
DOI: https://doi.org/10.1007/3-540-45657-0_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43997-4
Online ISBN: 978-3-540-45657-5
eBook Packages: Springer Book Archive