Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Acta Informatica
Published in: Acta Informatica 6/2015

01-09-2015 | Original Article

Parametrized invariance for infinite state processes

Authors: Alejandro Sánchez, César Sánchez

Published in: Acta Informatica | Issue 6/2015

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

We study the uniform verification problem for infinite state processes. This problem consists of proving that the parallel composition of an arbitrary number of processes running the same program (or a finite collection of programs) satisfies a temporal property. Our practical motivation is to build a general framework for the temporal verification of concurrent datatypes. In this paper we propose a general method for the verification of safety properties of parametrized programs that manipulate complex local and global data, including mutable state in the heap. Our method is based on a clear division between the following two dimensions of the problem: the interaction between executing threads—handled by novel parametrized invariance proof rules, and the data being manipulated—handled by specialized decision procedures. Our proof rules discharge automatically a finite collection of verification conditions. The size of this collection depends only on the size of the program and the specification, but not on the number of processes in any given instance or on the kind of data manipulated. Moreover, all verification conditions are quantifier free, which eases the development of decision procedures for complex data-types on top of off-the-shelf SMT solvers. We prove soundness of our proof rules and illustrate their application in the formal verification of (1) two infinite-state mutual exclusion protocols; (2) shape and functional correctness properties of several concurrent data-types, including fine-grained and non-blocking concurrent lists and queues. We report empirical results using a prototype implementation of the proof rules and decision procedures.
previous article Contextual hyperedge replacement

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now
Footnotes
Literature
1.
Abdulla, P.A., Bouajjani, A., Jonsson, B., Nilsson, M.: Handling global conditions in parametrized system verification. In: Proceedings of CAV’99. pp. 134–145 (1999)
2.
Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.K.: General decidability theorems for infinite-state systems. In: Proceedings of LICS’96. pp. 313–321. IEEE Computer Society (1996)
3.
Abdulla, P.A., Delzanno, G., Rezine, A.: Approximated parameterized verification of infinite-state processes with global conditions. FMSD 34(2), 126–156 (2009)MATH
4.
Amit, D., Rinetzky, N., Reps, T.W., Sagiv, M., Yahav, E.: Comparison under abstraction for verifying linearizability. In: Proceedings of CAV’07. LNCS, vol. 4590, pp. 477–490. Springer, Berlin (2007)
5.
Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307–309 (1986)MathSciNetCrossRef
6.
Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.D.: Parameterized verification with automatically computed inductive assertions. In: Proceedings of CAV’01. LNCS, vol. 2102, pp. 221–234. Springer, Berlin (2001)
7.
Berdine, J., Lev-Ami, T., Manevich, R., Ramalingam, G., Sagiv, S.: Thread quantification for concurrent shape analysis. In: Proceedings of CAV’08. LNCS, vol. 5123, pp. 399–413. Springer, Berlin (2008)
8.
Bradley, A.R.: SAT-based model checking without unrolling. In: Proceedings of VMCAI’11. LNCS, vol. 6538, pp. 70–87. Springer, Berlin (2011)
9.
Bradley, A.R., Manna, Z., Sipma., H.B.: What’s decidable about arrays? In: Proceedings of VMCAI’06. LNCS, vol. 3855, pp. 427–442. Springer, Berlin (2006)
10.
Browne, A., Manna, Z., Sipma, H.B.: Generalized verification diagrams. In: Proceedings of FSTTCS’95. LNCS, vol. 1206, pp. 484–498. Springer, Berlin (1995)
11.
Clarke, E.M., Grumberg, O.: Avoiding the state explosion problem in temporal logic model checking. In: Proceedings of PODC’87. pp. 294–303. ACM, New York (1987)
12.
Clarke, E.M., Grumberg, O., Browne, M.C.: Reasoning about networks with many identical finite-state processes. In: PODC’86, pp. 240–248. ACM, New York (1986)
13.
Clarke, E.M., Jha, S., Enders, R., Filkorn, T.: Exploiting symmetry in temporal logic model checking. FMSD 9(1/2), 77–104 (1996)
14.
Clarke, E.M., Talupur, M., Veith, H.: Proving ptolemy right: the environment abstraction framework for model checking concurrent systems. In: Proceedings of TACAS’08. LNCS, vol. 4963, pp. 33–47. Springer, Berlin (2008)
15.
Dutertre, B.: Yices 2.2. In: Proceedings of CAV’14, LNCS, vol. 8559, pp. 737–744. Springer, Berlin (2014)
16.
Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: Proceedings of CADE’00, LNAI, vol. 1831, pp. 236–254. Springer, Berlin (2000)
17.
Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: Proceedings of POPL’95, pp. 85–94. ACM, New York (1995)
18.
Emerson, E.A., Namjoshi, K.S.: Automatic verification of parameterized synchronous systems. In: Proceedings of CAV’96, LNCS, vol. 1102, pp. 87–98. Springer, Berlin (1996)
19.
Emerson, E.A., Sistla, A.P.: Symmetry and model checking. FMSD 9(1/2), 105–131 (1996)
20.
Fontaine, P., Ranise, S., Zarba, C.G.: Combining lists with non-stably infinite theories. In: Proceedings of LPAR’04, pp. 51–66. Springer, Berlin (2004)
21.
Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Proceedings of CAV’04, LNCS, vol. 3114, pp. 175–188. Springer, Berlin (2004)
22.
23.
Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: Proceedings of PLDI’12, pp. 415–416. ACM, New York (2012)
24.
Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgran-Kaufmann, Burlington (2008)
25.
Hoder, K., Bjørner, N.: Generalized property directed reachability. In: Proceedings of SAT’12, LNCS, vol. 7317, pp. 157–171. Springer, Berlin (2012)
26.
Kesten, Y., Pnueli, A., on Raviv, L.: Algorithmic verification of linear temporal logic specifications. In: Proceedings of ICALP’98, LNCS, vol. 1443, pp. 1–16. Springer, Berlin (1998)
27.
Lahiri, S.K., Qadeer, S.: Back to the future: revisiting precise program verification using SMT solvers. In: Proceedings of POPL’08. pp. 171–182. ACM, New York (2008)
28.
Lesens, D., Halbwachs, N., Raymond, P.: Automatic verification of parameterized linear networks of processes. In: Proceedings of POPL’97. pp. 346–357. ACM, New York (1997)
29.
Madhusudan, P., Parlato, G., Qiu, X.: Decidable logics combining heap structures and data. In: Proceedings of POPL’11, pp. 611–622. ACM, New York (2011)
30.
Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Berlin (1995)
31.
Marco Bozzano, G.D.: Beyond parameterized verification. In: TACAS’02. LNCS, vol. 2280, pp. 221–235. Springer, Berlin (2002)
32.
Michael, M.M., Scott, M.L.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: Proceedings of PODC’96, pp. 267–275 (1996)
33.
de Moura, L.M., Bjørner, N.: Z3: An efficient SMT solver. In: Proceedings of TACAS’08, LNCS, vol. 4963, pp. 337–340. Springer, Berlin (2008)
34.
Nelson, C.G., Oppen, D.C.: A simplifier based on efficient decision algorithms. In: Proceedings of POPL’78, pp. 141–150. ACM, New York (1978)
35.
Pnueli, A., Ruah, S., Zuck, L.D.: Automatic deductive verification with invisible invariants. In: Proceedings of TACAS’01, LNCS, vol. 2031, pp. 82–97. Springer, Berlin (2001)
36.
Qiu, X., Garg, P., Stefanescu, A., Madhusudan, P.: Natural proofs for structure, data, and separation. In: Proceedings of PLDI’13, pp. 231–242. ACM, New York (2013)
37.
Sánchez, A., Sánchez, C.: Decision procedures for the temporal verification of concurrent lists. In: Proceedings of ICFEM’10, LNCS, vol. 6447, pp. 74–89. Springer, Berlin (2010)
38.
Sánchez, A., Sánchez, C.: Parametrized verification diagrams. In: Proceedings of TIME’14, pp. 132–141. IEEE Computer Society Press, Los Alamitos (2014)
39.
Sánchez, A., Sankaranarayanan, S., Sánchez, C., Chang, B.Y.E.: Invariant generation for parametrized systems using self-reflection. In: Proceedings of SAS’12, LNCS, vol. 7460, pp. 146–163. Springer, Berlin (2012)
40.
Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Proceedings of CADE’05, LNCS, vol. 3632, pp. 219–234. Springer, Berlin (2005)
41.
Suzuki, I.: Proving properties of a ring of finite-state machines. Inf. Process. Lett. 28, 213–214 (1988)MATHCrossRef
42.
Tinelli, C., Zarba, C.G.: Combining decision procedures for sorted theories. In: Proceedings Logic in Artificial Intelligence (JELIA’04), LNCS, vol. 3229, pp. 641–653. Springer, Berlin (2004)
43.
44.
Totla, N., Wies, T.: Complete instantiation-based interpolation. In: Proceedings of POPL’13, pp. 537–548. ACM, New York (2013)
45.
Vafeiadis, V.: Shape-value abstraction for verifying linearizability. In: VMCAI. Lecture Notes in Computer Science, vol. 5403, pp. 335–348. Springer, Berlin (2009)
46.
Vafeiadis, V.: Automatically proving linearizability. In: Proceedings of CAV’10, LNCS, vol. 6174, pp. 450–464. Springer, Berlin (2010)
47.
Zuck, L.D., Pnueli, A.: Model checking and abstraction to the aid of parameterized systems (a survey). Comput. Lang. Syst. Struct. 30, 139–169 (2004)MATH
Metadata
Title
Parametrized invariance for infinite state processes
Authors
Alejandro Sánchez
César Sánchez
Publication date
01-09-2015
Publisher
Springer Berlin Heidelberg
Published in
Acta Informatica / Issue 6/2015
Print ISSN: 0001-5903
Electronic ISSN: 1432-0525
DOI
https://doi.org/10.1007/s00236-015-0222-5

Premium Partner

    Image Credits