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