@inproceedings(sofsem,
 author       = "P. A. Abdulla",
 year         = "2010",
 title        = "Forcing Monotonicity in Parameterized Verification: From Multisets to Words",
 booktitle    = "Proceedings of SOFSEM '10",
 publisher    = "Springer-Verlag",
 pages        = "1--15",
 doi          = "10.1007/978-3-642-11266-9\_1",
)
@inproceedings(lics,
 author       = "P. A. Abdulla and K. Cerans and B. Jonsson and Y.-K. Tsay",
 year         = "1996",
 title        = "General Decidability Theorems for Infinite-State Systems",
 booktitle    = "Proc. of LICS",
 pages        = "313--321",
 doi          = "10.1109/LICS.1996.561359",
)
@inproceedings(vmcai08,
 author       = "P. A. Abdulla and N. B. Henda and G. Delzanno and A. Rezine",
 year         = "2008",
 title        = "Handling Parameterized Systems with Non-atomic Global Conditions",
 booktitle    = "Proc. of VMCAI",
 series       = "LNCS",
 volume       = "4905",
 pages        = "22--36",
 doi          = "10.1007/978-3-540-78163-9\_7",
)
@inproceedings(lossy-lics,
 author       = "P. A. Abdulla and B. Jonsson",
 year         = "1993",
 title        = "Verifying Programs with Unreliable Channels",
 booktitle    = "LICS",
 pages        = "160--170",
 doi          = "10.1109/LICS.1993.287591",
)
@inproceedings(icatpn,
 author       = "P. A. Abdulla and A. Nyl{\'e}n",
 year         = "2001",
 title        = "Timed Petri nets and BQOs",
 booktitle    = "ICATPN",
 pages        = "53--70",
 doi          = "10.1007/3-540-45740-2\_5",
)
@inproceedings(atva09,
 author       = "P.A. Abdulla and M. Atto and J. Cederberg and R. Ji",
 year         = "2009",
 title        = "Automatic Verification of Dynamic Data-Dependent Programs",
 booktitle    = "ATVA",
 series       = "LNCS",
 doi          = "10.1007/978-3-642-04761-9\_16",
)
@inproceedings(AbdullaBCHR08,
 author       = "P.A. Abdulla and A. Bouajjani and J. Cederberg and F. Haziza and A. Rezine",
 year         = "2008",
 title        = "Monotonic Abstraction for Programs with Dynamic Memory Heaps",
 booktitle    = "CAV",
 pages        = "341--354",
 doi          = "10.1007/978-3-540-70545-1\_33",
)
@inproceedings(tacas06,
 author       = "P.A. Abdulla and G. Delzanno and N.B. Henda and A. Rezine",
 year         = "2007",
 title        = "Regular Model Checking Without Transducers",
 booktitle    = "TACAS",
 series       = "LNCS",
 volume       = "4424",
 pages        = "721--736",
 doi          = "10.1007/978-3-540-71209-1\_56",
)
@inproceedings(cav06,
 author       = "P.A. Abdulla and G. Delzanno and A. Rezine",
 year         = "2007",
 title        = "Parameterized Verification of Infinite-State Processes with Global Conditions",
 booktitle    = "CAV",
 series       = "LNCS",
 pages        = "145--157",
 doi          = "10.1007/978-3-540-73368-3\_17",
)
@inproceedings(rp08,
 author       = "P.A. Abdulla and G. Delzanno and A. Rezine",
 year         = "2008",
 title        = "Monotonic Abstraction in Parameterized Verification",
 booktitle    = "RP",
 series       = "ENTCS",
)
@inproceedings(AlbertiAR11a,
 author       = "F. Alberti and A. Armando and S. Ranise",
 year         = "2011",
 title        = "ASASP: Automated Symbolic Analysis of Security Policies",
 booktitle    = "CADE",
 pages        = "26--33",
 doi          = "10.1007/978-3-642-22438-6\_4",
)
@inproceedings(AlbertiAR11b,
 author       = "F. Alberti and A. Armando and S. Ranise",
 year         = "2011",
 title        = "Efficient symbolic automated analysis of administrative attribute-based RBAC-policies",
 booktitle    = "ASIACCS",
 pages        = "165--175",
 doi          = "10.1145/1966913.1966935",
)
@inproceedings(AlbertiBGRS12a,
 author       = "F. Alberti and R. Bruttomesso and S. Ghilardi and S. Ranise and N. Sharygina",
 year         = "2012",
 title        = "Lazy Abstraction with Interpolants for Arrays",
 booktitle    = "LPAR",
 pages        = "46--61",
 doi          = "10.1007/978-3-642-28717-6\_7",
)
@inproceedings(ABGRS12b,
 author       = "F. Alberti and R. Bruttomesso and S. Ghilardi and S. Ranise and N. Sharygina",
 year         = "2012",
 title        = "{SAFARI: SMT-Based Abstraction for Arrays with Interpolants}",
 booktitle    = "CAV",
 doi          = "10.1007/978-3-642-31424-7\_49",
)
@article(fmsd,
 author       = "F. Alberti and R. Bruttomesso and S. Ghilardi and S. Ranise and N. Sharygina",
 year         = "2014",
 title        = "An extension of Lazy Abstraction with Interpolation for programs with arrays",
 journal      = "Formal Methods in System Design",
 volume       = "45",
 number       = "1",
 pages        = "63--109",
 doi          = "10.1007/s10703-014-0209-9",
)
@inproceedings(AlbertiGPRR10a,
 author       = "F. Alberti and S. Ghilardi and E. Pagani and S. Ranise and G. P. Rossi",
 year         = "2010",
 title        = "Brief Announcement: Automated Support for the Design and Validation of Fault Tolerant Parameterized Systems - A Case Study",
 booktitle    = "DISC",
 pages        = "392--394",
 doi          = "10.1007/978-3-642-15763-9\_36",
)
@article(AlbertiGPRR12,
 author       = "F. Alberti and S. Ghilardi and E. Pagani and S. Ranise and G.P. Rossi",
 year         = "2012",
 title        = "Universal Guards, Relativization of Quantifiers, and Failure Models in {Model Checking Modulo Theories}",
 journal      = "JSAT",
 volume       = "8",
 number       = "1/2",
 pages        = "29--61",
)
@inproceedings(AlbertiGS13,
 author       = "F. Alberti and S. Ghilardi and N. Sharygina",
 year         = "2013",
 title        = "Definability of Accelerated Relations in a Theory of Arrays and Its Applications",
 booktitle    = "FroCoS",
 pages        = "23--39",
 doi          = "10.1007/978-3-642-40885-4\_3",
)
@inproceedings(AlbertiGS14,
 author       = "F. Alberti and S. Ghilardi and N. Sharygina",
 year         = "2014",
 title        = "Decision Procedures for Flat Array Properties",
 booktitle    = "TACAS",
 pages        = "15--30",
 doi          = "10.1007/978-3-642-54862-8\_2",
)
@inproceedings(cilc14,
 author       = "F. Alberti and S. Ghilardi and N. Sharygina",
 year         = "2014",
 title        = "A framework for the verification of parameterized infinite-state systems",
 booktitle    = "CILC",
 publisher    = "CEUR",
)
@inproceedings(octagons,
 author       = "M. Bozga and C. Girlea and R. Iosif",
 year         = "2009",
 title        = "Iterating octagons",
 booktitle    = "TACAS",
 series       = "LNCS",
 pages        = "337--351",
 doi          = "10.1007/978-3-642-00768-2\_29",
)
@inproceedings(acceleration_CAV,
 author       = "M. Bozga and R. Iosif and F. Konecny",
 year         = "2010",
 title        = "Fast Acceleration of Ultimately Periodic Relations",
 booktitle    = "CAV",
 series       = "LNCS",
 doi          = "10.1007/978-3-642-14295-6\_23",
)
@article(db2,
 author       = "M. Bozga and R. Iosif and Y. Lakhnech",
 year         = "2009",
 title        = "Flat parametric counter automata",
 journal      = "Fundamenta Informaticae",
 number       = "91",
 pages        = "275--303",
 doi          = "10.3233/FI-2009-0044",
)
@book(BradleyM07,
 author       = "A.R. Bradley and Z. Manna",
 year         = "2007",
 title        = "Calculus of computation: decision procedures with applications to verification",
 publisher    = "Springer",
 doi          = "10.1007/978-3-540-74113-8",
)
@inproceedings(BradleyMS06,
 author       = "A.R. Bradley and Z. Manna and H.B. Sipma",
 year         = "2006",
 title        = "What's Decidable About Arrays?",
 booktitle    = "VMCAI",
 pages        = "427--442",
 doi          = "10.1007/11609773\_28",
)
@inproceedings(BruttomessoCGR12,
 author       = "R. Bruttomesso and A. Carioni and S. Ghilardi and S. Ranise",
 year         = "2012",
 title        = "Automated Analysis of Parametric Timing-Based Mutual Exclusion Algorithms",
 booktitle    = "NASA Formal Methods",
 pages        = "279--294",
 doi          = "10.1007/978-3-642-28891-3\_28",
)
@inproceedings(db1,
 author       = "H. Comon and Y. Jurski",
 year         = "1998",
 title        = "Multiple Counters Automata, Safety Analysis and Presburger Arithmetic",
 booktitle    = "CAV",
 series       = "LNCS",
 volume       = "1427",
 publisher    = "Springer",
 pages        = "268--279",
 doi          = "10.1007/BFb0028751",
)
@inproceedings(cubicle1,
 author       = "S. Conchon and A. Goel and S. Krstić and A. Mebsout and F. Zaïdi",
 year         = "2012",
 title        = "{Cubicle: a Parallel SMT-based Model-Checker fro Parameterized Systems}",
 booktitle    = "Proc. of CAV",
 series       = "LNCS",
 doi          = "10.1007/978-3-642-31424-7\_55",
)
@inproceedings(cubicle2,
 author       = "S. Conchon and A. Goel and S. Krstić and A. Mebsout and F. Zaïdi",
 year         = "2013",
 title        = "{Invariants for Finite Instances and Beyond}",
 booktitle    = "Proc. of FMCAD",
)
@inproceedings(cav-delzanno,
 author       = "G. Delzanno",
 year         = "2000",
 title        = "{Automatic verification of parameterized cache coherence protocols}",
 booktitle    = "Proc. of CAV",
 series       = "LNCS",
 volume       = "1855",
 doi          = "10.1007/10722167\_8",
)
@inproceedings(en-lics,
 author       = "E.A. Emerson and K.S. Namjoshi",
 year         = "1998",
 title        = "On model checking for non-deterministic infinite-state systems",
 booktitle    = "LICS",
 pages        = "70–80",
 doi          = "10.1109/LICS.1998.705644",
)
@inproceedings(bro1,
 author       = "J. Esparza and A. Finkel and R. Mayr",
 year         = "1999",
 title        = "On the Verification of Broadcast Protocols",
 booktitle    = "Proc. of LICS",
 publisher    = "IEEE Computer Society",
 pages        = "352--359",
 doi          = "10.1109/LICS.1999.782630",
)
@inproceedings(presburger,
 author       = "A. Finkel and J. Leroux",
 year         = "2002",
 title        = "How to compose {Presburger}-accelerations: Applications to broadcast protocols",
 booktitle    = "FST TCS ’02",
 publisher    = "Springer",
 pages        = "145--156",
 doi          = "10.1007/3-540-36206-1\_14",
)
@inproceedings(GhilardiNRZ08,
 author       = "S. Ghilardi and E. Nicolini and S. Ranise and D. Zucchelli",
 year         = "2008",
 title        = "{Towards {SMT} Model Checking of Array-Based Systems}",
 booktitle    = "IJCAR",
 pages        = "67--82",
 doi          = "10.1007/978-3-540-71070-7\_6",
)
@article(GhilardiR10a,
 author       = "S. Ghilardi and S. Ranise",
 year         = "2010",
 title        = "{Backward Reachability of Array-based Systems by {SMT} solving: Termination and Invariant Synthesis}",
 journal      = "LMCS",
 volume       = "6",
 number       = "4",
 doi          = "10.2168/LMCS-6(4:10)2010",
)
@inproceedings(JhalaM07,
 author       = "R. Jhala and K.L. McMillan",
 year         = "2007",
 title        = "{Array Abstractions from Proofs}",
 booktitle    = "CAV",
 pages        = "193--206",
 doi          = "10.1007/978-3-540-73368-3\_23",
)
@book(lynch,
 author       = "Nancy A. Lynch",
 year         = "1996",
 title        = "Distributed Algorithms",
 publisher    = "Morgan Kaufmann",
)
@inproceedings(McMillan06,
 author       = "K.L. McMillan",
 year         = "2006",
 title        = "{Lazy Abstraction with Interpolants}",
 booktitle    = "CAV",
 pages        = "123--136",
 doi          = "10.1007/11817963\_14",
)
@inproceedings(toueg,
 author       = "S. Toueg and T. D. Chandra",
 year         = "1990",
 title        = "{Time and Message Efficient Reliable Broadcast}",
 booktitle    = "Proc. 4th Int. Workshop on Distributed Algorithms",
 series       = "LNCS",
 pages        = "289–--303",
 doi          = "10.1007/3-540-54099-7\_20",
)