The Spotlight Principle

On Combining Process-Summarizing State Abstractions
  • Björn Wachter
  • Bernd Westphal
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4349)


Formal verification of safety and liveness properties of systems with a dynamically changing, unbounded number of interlinked processes and infinite-domain local data is challenging due to the two sources of infiniteness. The existing state abstraction-based approaches Data Type Reduction and Environment Abstraction each address one aspect, but the former doesn’t support infinite-domain local data and the latter doesn’t support links and is restricted to particular properties.

The contribution of this paper is a combination of both which is obtained by first stating them in the framework of Canonical Abstraction. This new use of Canonical Abstraction, originally designed and used for the analysis of programs with heap-allocated data structures, furthermore unveils a formal connection between the two rather ad-hoc techniques.


Predicate Symbol Concrete State Liveness Property Abstract Domain Reference Process 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Hsu, A., Eskafi, F., Sachs, S., Varaiya, P.: The Design of Platoon Maneuver Protocols for IVHS. PATH Research Report UCB-ITS-PRR-91-6, Institute of Transportation Studies, University of California at Berkeley (1991)Google Scholar
  2. 2.
    Pnueli, A., Xu, J., Zuck, L.: Liveness with (0,1,infty)-counter abstraction. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 107–133. Springer, Heidelberg (2003)Google Scholar
  3. 3.
    Lubachevsky, B.D.: An Approach to Automating the Verification of Compact Parallel Coordination Programs. Acta Informatica 21, 125–169 (1984)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Pong, F., Dubois, M.: Formal verification of complex coherence protocols using symbolic state models. J. ACM 45, 557–587 (1998)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39, 675–735 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Clarke, E.M., Talupur, M., Veith, H.: Environment abstraction for parameterized verification. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 126–141. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  7. 7.
    McMillan, K.L.: Verification of infinite state systems by compositional model checking (charme). In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 219–234. Springer, Heidelberg (1999)Google Scholar
  8. 8.
    Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems 22 (2001)Google Scholar
  9. 9.
    Yahav, E.: Verifying safety properties of concurrent Java programs using 3-valued logic. ACM SIGPLAN Notices 36, 27–40 (2001)CrossRefGoogle Scholar
  10. 10.
    Yahav, E., Ramalingam, G.: Verifying safety properties using separation and heterogeneous abstractions. In: Proceedings of the ACM SIGPLAN conference on Programming language design and implementation, pp. 25–34. ACM Press, New York (2004)Google Scholar
  11. 11.
    Yahav, E., et al.: Verifying Temporal Heap Properties Specified via Evolution Logic. In: Degano, P. (ed.) ESOP 2003 and ETAPS 2003. LNCS, vol. 2618, pp. 204–222. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  12. 12.
    Distefano, D., Katoen, J.P., Rensink, A.: Who is Pointing When to Whom? In: Proceedings of the 24th International Conference On Foundations of Software Technology and Theoretical Computer Science, pp. 250–262 (2004)Google Scholar
  13. 13.
    McMillan, K.L., Qadeer, S., Saxe, J.B.: Induction in Compositional Model Checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 15–19. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  14. 14.
    Manevich, R., et al.: Predicate abstraction and canonical abstraction for singly-linked lists. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 181–198. Springer, Heidelberg (2005)Google Scholar
  15. 15.
    Damm, W., Westphal, B.: Live and Let Die: LSC-based Verification of UML-Models. In: de Boer, F.S., et al. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 99–135. Springer, Heidelberg (2003)Google Scholar
  16. 16.
    Dams, D., Namjoshi, K.S.: Shape Analysis through Predicate Abstraction and Model Checking. In: Zuck, L.D., et al. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 310–324. Springer, Heidelberg (2002)Google Scholar
  17. 17.
    Kesten, Y., Pnueli, A.: Control and Data Abstraction: The Cornerstones of Practical Formal Verification. International Journal on Software Tools for Technology Transfer 2, 328–342 (2000)zbMATHCrossRefGoogle Scholar
  18. 18.
    Lamport, L.: A New Solution of Dijkstra’s Concurrent Programming Problem. Communications of the ACM 17, 453–455 (1974)zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    Lev-Ami, T., Sagiv, M.: TVLA: A System for Implementing Static Analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 280–301. Springer, Heidelberg (2000)Google Scholar
  20. 20.
    Podelski, A., Wies, T.: Boolean Heaps. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 268–283. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  21. 21.
    Wachter, B.: Checking universally quantified temporal properties with three- valued analysis. Master’s thesis, Universität des Saarlandes (2005)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Björn Wachter
    • 1
  • Bernd Westphal
    • 2
  1. 1.Universität des Saarlandes, Im Stadtwald, 66041 SaarbrückenGermany
  2. 2.Carl von Ossietzky Universität Oldenburg, 26111 OldenburgGermany

Personalised recommendations