Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson & Yih-Kuen Tsay (1996):
General Decidability Theorems for Infinite-State Systems.
In: LICS.
IEEE Computer Society,
pp. 313–321,
doi:10.1109/LICS.1996.561359.
Krzysztof R. Apt & Dexter Kozen (1986):
Limits for Automatic Verification of Finite-State Concurrent Systems..
Inf. Process. Lett. 22(6),
pp. 307–309,
doi:10.1016/0020-0190(86)90071-2.
E. M. Clarke, T. Filkorn & S. Jha (1993):
Exploiting Symmetry in Temporal Logic Model Checking.
In: CAV,
LNCS 697,
pp. 450–462,
doi:10.1007/3-540-56922-7_37.
Edmund M. Clarke, Muralidhar Talupur & Helmut Veith (2006):
Environment Abstraction for Parameterized Verification..
In: VMCAI,
LNCS 3855,
pp. 126–141,
doi:10.1007/11609773_9.
Jamieson M. Cobleigh, Dimitra Giannakopoulou & Corina S. Pasareanu (2003):
Learning Assumptions for Compositional Verification.
In: TACAS,
LNCS 2619.
Springer,
pp. 331–346,
doi:10.1007/3-540-36577-X_24.
A. Cohen & K. S. Namjoshi (2007):
Local Proofs for Global Safety Properties.
In: CAV,
LNCS 4590.
Springer,
pp. 55–67,
doi:10.1007/978-3-540-73368-3_9.
A. Cohen & K. S. Namjoshi (2008):
Local Proofs for Linear-Time Properties of Concurrent Programs.
In: CAV,
LNCS 5123.
Springer,
pp. 149–161,
doi:10.1007/978-3-540-70545-1_15.
A. Cohen, K. S. Namjoshi & Y. Sa'ar (2010):
A Dash of Fairness for Compositional Reasoning.
In: CAV,
pp. 543–557,
doi:10.1007/978-3-642-14295-6_46.
A. Cohen, K. S. Namjoshi & Y. Sa'ar (2010):
SPLIT: A Compositional LTL Verifier.
In: CAV,
pp. 558–561,
doi:10.1007/978-3-642-14295-6_47.
Ariel Cohen, Kedar S. Namjoshi, Yaniv Sa'ar, Lenore D. Zuck & Katya I. Kisyova (2010):
Parallelizing A Symbolic Compositional Model-Checking Algorithm.
In: HVC,
LNCS 6504,
pp. 46–59,
doi:10.1007/978-3-642-19583-9_9.
E.W. Dijkstra & C.S. Scholten (1990):
Predicate Calculus and Program Semantics.
Springer Verlag,
doi:10.1007/978-1-4612-3228-5.
E. Allen Emerson & Vineet Kahlon (2000):
Reducing Model Checking of the Many to the Few..
In: CADE,
LNCS 1831,
pp. 236–254,
doi:10.1007/10721959_19.
E.A. Emerson & K.S. Namjoshi (1995):
Reasoning about Rings.
In: ACM Symposium on Principles of Programming Languages,
doi:10.1145/199448.199468.
E.A. Emerson & A.P. Sistla (1993):
Symmetry and Model Checking.
In: CAV,
LNCS 697,
pp. 463–478,
doi:10.1007/3-540-56922-7_38.
C. Flanagan & S. Qadeer (2003):
Thread-Modular Model Checking..
In: SPIN,
LNCS 2648,
pp. 213–224,
doi:10.1007/3-540-44829-2_14.
S. German & A.P. Sistla (1992):
Reasoning about Systems with Many Processes.
Journal of the ACM,
doi:10.1145/146637.146681.
Martin Golubitsky & Ian Stewart (2006):
Nonlinear dynamics of networks: the groupoid formalism.
Bull. Amer. Math. Soc. 43,
pp. 305–364,
doi:10.1090/S0273-0979-06-01108-6.
Ashutosh Gupta, Corneliu Popeea & Andrey Rybalchenko (2011):
Predicate abstraction and refinement for verifying multi-threaded programs.
In: POPL.
ACM,
pp. 331–344,
doi:10.1145/1926385.1926424.
Gerard J. Holzmann (2004):
The SPIN Model Checker - primer and reference manual.
Addison-Wesley.
C.N. Ip & D. Dill (1996):
Better Verification Through Symmetry.
Formal Methods in System Design 9(1/2),
pp. 41–75,
doi:10.1007/BF00625968.
L. Lamport (1977):
Proving the Correctness of Multiprocess Programs..
IEEE Trans. Software Eng. 3(2),
doi:10.1109/TSE.1977.229904.
Leslie Lamport (1997):
Composition: A Way to Make Proofs Harder.
In: COMPOS,
pp. 402–423,
doi:10.1007/3-540-49213-5_15.
Kenneth L. McMillan & Lenore D. Zuck (2011):
Invisible Invariants and Abstract Interpretation.
In: Eran Yahav: SAS,
Lecture Notes in Computer Science 6887.
Springer,
pp. 249–262,
doi:10.1007/978-3-642-23702-7_20.
K. S. Namjoshi (2007):
Symmetry and Completeness in the Analysis of Parameterized Systems.
In: VMCAI,
LNCS 4349,
pp. 299–313,
doi:10.1007/978-3-540-69738-1_22.
Kedar S. Namjoshi & Richard J. Trefler (2012):
Local Symmetry and Compositional Verification.
In: VMCAI,
LNCS 7148,
pp. 348–362,
doi:10.1007/978-3-642-27940-9_23.
Kedar S. Namjoshi & Richard J. Trefler (2013):
Uncovering Symmetries in Irregular Process Networks.
In: VMCAI,
LNCS 7737,
pp. 496–514,
doi:10.1007/978-3-642-35873-9_29.
S. S. Owicki & D. Gries (1976):
Verifying Properties of Parallel Programs: An Axiomatic Approach..
Commun. ACM 19(5),
pp. 279–285,
doi:10.1145/360051.360224.
A. Pnueli, S. Ruah & L. D. Zuck (2001):
Automatic Deductive Verification with Invisible Invariants..
In: TACAS,
LNCS 2031,
pp. 82–97,
doi:10.1007/3-540-45319-9_7.
W-P. de Roever, F. de Boer, U. Hannemann, J. Hooman, Y. Lakhnech, M. Poel & J. Zwiers (2001):
Concurrency Verification: Introduction to Compositional and Noncompositional Proof Methods.
Cambridge University Press.
Alejandro Sánchez, Sriram Sankaranarayanan, César Sánchez & Bor-Yuh Evan Chang (2012):
Invariant Generation for Parametrized Systems Using Self-reflection - (Extended Version).
In: Antoine Miné & David Schmidt: SAS,
Lecture Notes in Computer Science 7460.
Springer,
pp. 146–163,
doi:10.1007/978-3-642-33125-1_12.
Alan Weinstein (1996):
Groupoids: Unifying Internal and External Symmetry-A Tour through Some Examples.
Notices of the AMS.
eptcs@eptcs.org