Abstract
We study the underapproximation of the predicate transformers used to give semantics to the modalities in dynamic and temporal logic. Because predicate transformers operate on state sets, we define appropriate powerdomains for sound approximation. We study four such domains — two are based on “set inclusion” approximation, and two are based on “quantification” approximation — and we apply the domains to synthesize the most precise, underapproximating \(\widetilde{pre}\) and pre transformers, in the latter case, introducing a focus operation. We also show why the expected abstractions of post and \(\widetilde{post}\) are unsound, and we use the powerdomains to guide us to correct, sound underapproximations.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
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
Bourdoncle, F.: Abstract debugging of higher-order imperative languages. In: Proc. ACM Conf. PLDI, pp. 46–55 (2003)
Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems 16(5), 1512–1542 (1994)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)
Cleaveland, R., Iyer, P., Yankelevich, D.: Optimality in abstractions of model checking. In: Mycroft, A. (ed.) SAS 1995. LNCS, vol. 983. Springer, Heidelberg (1995)
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. PhD thesis, University of Grenoble (1978)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs. In: Proc. 4th ACM Symp. POPL, pp. 238–252 (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proc. 6th ACM Symp. POPL, pp. 269–282 (1979)
Cousot, P., Cousot, R.: Temporal abstract interpretation. In: Proc. 27th ACM Symp. on Principles of Programming Languages, pp. 12–25. ACM Press, New York (2000)
Dams, D.: Abstract interpretation and partition refinement for model checking. PhD thesis, Technische Universiteit Eindhoven, The Netherlands (1996)
Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. ACM Trans. Prog. Lang. Systems 19, 253–291 (1997)
Dams, D., Namjoshi, K.: The existence of finite abstractions for branching time model checking. In: Proc. IEEE Symp. LICS 2004, pp. 335–344 (2004)
Dams, D.R., Namjoshi, K.S.: Automata as abstractions. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 216–232. Springer, Heidelberg (2005)
Davey, B.A., Priestly, H.A.: Introduction to Lattices and Order, 2nd edn. Cambridge University Press, Cambridge (2002)
Fecher, H., Huth, M.: Complete abstractions through extensions of disjunctive modal transition systems. Technical Report 0604, Institut für Informatik und Praktische Mathematik der Christian-Albrechts-Universitaet zu Kiel (2005)
Giacobazzi, R., Quintarelli, E.: Incompleteness, counterexamples, and refinements in abstract model-checking. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 356–373. Springer, Heidelberg (2001)
Giacobazzi, R., Ranzato, F.: The reduced relative power operation on abstract domains. Theoretical Comp. Sci. 216, 159–211 (1999)
Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. ACM 47, 361–416 (2000)
Heckmann, R.: Power domain constructions. PhD thesis, Univ. Saarbrücken (1990)
Larsen, K.: Proof systems for Hennessy-Milner logic with recursion. In: Dauchet, M., Nivat, M. (eds.) CAAP 1988. LNCS, vol. 299. Springer, Heidelberg (1988)
Larsen, K.G., Xinxin, L.: Equation solving using modal transition systems. In: LICS 1990 (1990)
Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for verification of concurrent systems. Formal Methods in System Design 6, 1–36 (1995)
Massé, D.: Combining forward and backward analyses of temporal properties. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol. 2053, pp. 103–172. Springer, Heidelberg (2001)
Massé, D.: Property checking driven abstract interpretation-based static analysis. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 56–69. Springer, Heidelberg (2002)
Plotkin, G.: Domains. Lecture notes, Univ. Pisa/Edinburgh (1983)
Ranzato, F., Tapparo, F.: Strong preservation as completeness in abstract interpretation. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 18–32. Springer, Heidelberg (2004)
Ranzato, F., Tapparo, F.: An abstract interpretation-based refinement algorithm for strong preservation. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 140–156. Springer, Heidelberg (2005)
Ranzato, F., Tapparo, F.: Strong preservation of temporal fixpoint-based operators by abstract interpretation. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 332–347. Springer, Heidelberg (2005)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM TOPLAS 24, 217–298 (2002)
Schmidt, D.A.: Data-flow analysis is model checking of abstract interpretations. In: Proc. 25th ACM Symp. on Principles of Prog. Languages. ACM Press, New York (1998)
Schmidt, D.A.: Closed and logical relations for over- and under-approximation of powersets. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 22–37. Springer, Heidelberg (2004)
Schmidt, D.A.: A calculus of logical relations for over- and underapproximating static analyses. Science of Computer Programming (in press)
Shoham, S., Grumberg, O.: Monotonic abstraction-refinement for CTL. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 546–560. Springer, Heidelberg (2004)
Shoham, S., Grumberg, O.: 3-valued abstraction: More precision at less cost. In: LICS 2006 (2006)
Steffen, B.: Generating data-flow analysis algorithms for modal specifications. Science of Computer Programming 21, 115–139 (1993)
Steffen, B., Classen, A., Klein, M., Knoop, J., Margaria, T.: The fixpoint analysis machine. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 72–87. Springer, Heidelberg (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schmidt, D.A. (2006). Underapproximating Predicate Transformers. In: Yi, K. (eds) Static Analysis. SAS 2006. Lecture Notes in Computer Science, vol 4134. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11823230_9
Download citation
DOI: https://doi.org/10.1007/11823230_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37756-6
Online ISBN: 978-3-540-37758-0
eBook Packages: Computer ScienceComputer Science (R0)