Parametrized invariance for infinite state processes

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)

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)

Abdulla, P.A., Delzanno, G., Rezine, A.: Approximated parameterized verification of infinite-state processes with global conditions. FMSD 34(2), 126–156 (2009)

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)

Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307–309 (1986)

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)

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)

Bradley, A.R.: SAT-based model checking without unrolling. In: Proceedings of VMCAI’11. LNCS, vol. 6538, pp. 70–87. Springer, Berlin (2011)

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)

Browne, A., Manna, Z., Sipma, H.B.: Generalized verification diagrams. In: Proceedings of FSTTCS’95. LNCS, vol. 1206, pp. 484–498. Springer, Berlin (1995)

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)

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)

Clarke, E.M., Jha, S., Enders, R., Filkorn, T.: Exploiting symmetry in temporal logic model checking. FMSD 9(1/2), 77–104 (1996)

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)

Dutertre, B.: Yices 2.2. In: Proceedings of CAV’14, LNCS, vol. 8559, pp. 737–744. Springer, Berlin (2014)

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)

Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: Proceedings of POPL’95, pp. 85–94. ACM, New York (1995)

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)

Emerson, E.A., Sistla, A.P.: Symmetry and model checking. FMSD 9(1/2), 105–131 (1996)

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)

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)

German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675–735 (1992)

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)

Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgran-Kaufmann, Burlington (2008)

Hoder, K., Bjørner, N.: Generalized property directed reachability. In: Proceedings of SAT’12, LNCS, vol. 7317, pp. 157–171. Springer, Berlin (2012)

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)

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)

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)

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)

Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Berlin (1995)

Marco Bozzano, G.D.: Beyond parameterized verification. In: TACAS’02. LNCS, vol. 2280, pp. 221–235. Springer, Berlin (2002)

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)

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)

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)

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)

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)

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)

Sánchez, A., Sánchez, C.: Parametrized verification diagrams. In: Proceedings of TIME’14, pp. 132–141. IEEE Computer Society Press, Los Alamitos (2014)

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)

Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Proceedings of CADE’05, LNCS, vol. 3632, pp. 219–234. Springer, Berlin (2005)

Suzuki, I.: Proving properties of a ring of finite-state machines. Inf. Process. Lett. 28, 213–214 (1988)

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)

Tinelli, C., Zarba, C.G.: Combining nonstably infinite theories. J. Autom. Reas. 34, 209–238 (2005)

Totla, N., Wies, T.: Complete instantiation-based interpolation. In: Proceedings of POPL’13, pp. 537–548. ACM, New York (2013)

Vafeiadis, V.: Shape-value abstraction for verifying linearizability. In: VMCAI. Lecture Notes in Computer Science, vol. 5403, pp. 335–348. Springer, Berlin (2009)

Vafeiadis, V.: Automatically proving linearizability. In: Proceedings of CAV’10, LNCS, vol. 6174, pp. 450–464. Springer, Berlin (2010)

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)