Structural Invariants for Parameterized Architectures
245
20. Clarke, E., Talupur, M., Veith, H.: Environment abstraction for parameterized verification.
In: Emerson, E.A., Namjoshi, K.S. (eds.) Verification, Model Checking, and Abstract Interpretation. pp. 126–141 (2006)
21. Conchon, S., Goel, A., Krsti´ c, S., Mebsout, A., Za¨ ıdi, F.: Cubicle: A parallel SMT-based
model checker for parameterized systems. In: Madhusudan, P., Seshia, S.A. (eds.) Computer
Aided Verification. pp. 718–724 (2012)
22. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Conference
Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 269–282. ACM Press, New York, NY, San Antonio, Texas (1979)
23. Dams, D., Lakhnech, Y., Steffen, M.: Iterating transducers. The Journal of Logic and Algebraic Programming 52-53, 109 – 127 (2002)
24. Delzanno, G.: Automatic verification of parameterized cache coherence protocols. In: Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July
15-19, 2000, Proceedings. pp. 53–68 (2000)
25. Dijkstra, E.W., Scholten, C.S.: Termination detection for diffusing computations. Inf. Process. Lett. 11(1), 1–4 (1980)
26. Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: CADE.
Lecture Notes in Computer Science, vol. 1831, pp. 236–254. Springer (2000)
27. Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: POPL’95 Proceedings. pp. 85–94
(1995)
28. Esparza, J., Ledesma-Garza, R., Majumdar, R., Meyer, P.J., Niksic, F.: An smt-based approach to coverability analysis. In: CAV. Lecture Notes in Computer Science, vol. 8559, pp.
603–619. Springer (2014)
29. Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput.
Sci. 256(1-2), 63–92 (2001)
30. Fribourg, L., Ols´ en, H.: Reachability sets of parameterized rings as regular languages. Electr.
Notes Theor. Comput. Sci. 9, 40 (1997)
31. German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3),
675–735 (1992)
32. Hartmanns, A., Seidl, M.: tacas20ae.ova (10 2019), https://figshare.com/articles/tacas20ae
ova/9699839
33. Henriksen, J., Jensen, J., Jørgensen, M., Klarlund, N., Paige, B., Rauhe, T., Sandholm, A.:
Mona: Monadic second-order logic in practice. In: Tools and Algorithms for the Construction
and Analysis of Systems, First International Workshop, TACAS ’95, LNCS 1019 (1995)
34. Jacobs, S., Sakr, M.: Analyzing guarded protocols: Better cutoffs, more systems, more
expressivity. In: VMCAI. Lecture Notes in Computer Science, vol. 10747, pp. 247–268.
Springer (2018)
35. Jensen, H.E., Lynch, N.A.: A proof of Burns n-process mutual exclusion algorithm using
abstraction. In: TACAS (1998)
36. Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with
rich assertional languages. Theoretical Computer Science 256(1), 93 – 112 (2001)
37. Khoussainov, B., Nerode, A.: Automata Theory and Its Applications. Birkhauser Boston,
Inc. (2001)
38. Pnueli, A., Ruah, S., Zuck, L.: Automatic deductive verification with invisible invariants.
In: Margaria, T., Yi, W. (eds.) Tools and Algorithms for the Construction and Analysis of
Systems. pp. 82–97 (2001)
39. Sifakis, J.: Structural properties of petri nets. In: Winkowski, J. (ed.) Mathematical Foundations of Computer Science 1978. pp. 474–483 (1978)
245
20. Clarke, E., Talupur, M., Veith, H.: Environment abstraction for parameterized verification.
In: Emerson, E.A., Namjoshi, K.S. (eds.) Verification, Model Checking, and Abstract Interpretation. pp. 126–141 (2006)
21. Conchon, S., Goel, A., Krsti´ c, S., Mebsout, A., Za¨ ıdi, F.: Cubicle: A parallel SMT-based
model checker for parameterized systems. In: Madhusudan, P., Seshia, S.A. (eds.) Computer
Aided Verification. pp. 718–724 (2012)
22. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Conference
Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 269–282. ACM Press, New York, NY, San Antonio, Texas (1979)
23. Dams, D., Lakhnech, Y., Steffen, M.: Iterating transducers. The Journal of Logic and Algebraic Programming 52-53, 109 – 127 (2002)
24. Delzanno, G.: Automatic verification of parameterized cache coherence protocols. In: Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July
15-19, 2000, Proceedings. pp. 53–68 (2000)
25. Dijkstra, E.W., Scholten, C.S.: Termination detection for diffusing computations. Inf. Process. Lett. 11(1), 1–4 (1980)
26. Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: CADE.
Lecture Notes in Computer Science, vol. 1831, pp. 236–254. Springer (2000)
27. Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: POPL’95 Proceedings. pp. 85–94
(1995)
28. Esparza, J., Ledesma-Garza, R., Majumdar, R., Meyer, P.J., Niksic, F.: An smt-based approach to coverability analysis. In: CAV. Lecture Notes in Computer Science, vol. 8559, pp.
603–619. Springer (2014)
29. Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput.
Sci. 256(1-2), 63–92 (2001)
30. Fribourg, L., Ols´ en, H.: Reachability sets of parameterized rings as regular languages. Electr.
Notes Theor. Comput. Sci. 9, 40 (1997)
31. German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3),
675–735 (1992)
32. Hartmanns, A., Seidl, M.: tacas20ae.ova (10 2019), https://figshare.com/articles/tacas20ae
ova/9699839
33. Henriksen, J., Jensen, J., Jørgensen, M., Klarlund, N., Paige, B., Rauhe, T., Sandholm, A.:
Mona: Monadic second-order logic in practice. In: Tools and Algorithms for the Construction
and Analysis of Systems, First International Workshop, TACAS ’95, LNCS 1019 (1995)
34. Jacobs, S., Sakr, M.: Analyzing guarded protocols: Better cutoffs, more systems, more
expressivity. In: VMCAI. Lecture Notes in Computer Science, vol. 10747, pp. 247–268.
Springer (2018)
35. Jensen, H.E., Lynch, N.A.: A proof of Burns n-process mutual exclusion algorithm using
abstraction. In: TACAS (1998)
36. Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with
rich assertional languages. Theoretical Computer Science 256(1), 93 – 112 (2001)
37. Khoussainov, B., Nerode, A.: Automata Theory and Its Applications. Birkhauser Boston,
Inc. (2001)
38. Pnueli, A., Ruah, S., Zuck, L.: Automatic deductive verification with invisible invariants.
In: Margaria, T., Yi, W. (eds.) Tools and Algorithms for the Construction and Analysis of
Systems. pp. 82–97 (2001)
39. Sifakis, J.: Structural properties of petri nets. In: Winkowski, J. (ed.) Mathematical Foundations of Computer Science 1978. pp. 474–483 (1978)