@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(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(cilc16,
 author       = {F. Alberti and S. Ghilardi and A. Orsini and E. Pagani},
 year         = {2016},
 title        = {{Counter Abstractions in Model Checking of Distributed Broadcast Algorithms: Some Case Studies}},
 booktitle    = {{Proc. CILC}},
 series       = {{CEUR Proceedings}},
 pages        = {102--117},
 url          = {http://ceur-ws.org/Vol-1645/paper_4.pdf},
)
@inproceedings(arca,
 author       = {F. Alberti and S. Ghilardi and E. Pagani},
 year         = {2016},
 title        = {{Counting Constraints in Flat Array Fragments}},
 booktitle    = {{Proc. IJCAR}},
 series       = {{Lecture Notes in Computer Science}},
 volume       = {9706},
 pages        = {65--81},
 doi          = {10.1007/978-3-319-40229-1_6},
)
@article(fmsd17,
 author       = {F. Alberti and S. Ghilardi and E. Pagani},
 year         = {2017},
 title        = {{Cardinality Constraints for Arrays (decidability results and applications)}},
 journal      = {Formal Methods in System Design},
 doi          = {10.1007/s10703-017-0279-6},
 note         = {To appear},
)
@article(JAR15,
 author       = {F. Alberti and S. Ghilardi and N. Sharygina},
 year         = {2015},
 title        = {{Decision Procedures for Flat Array Properties}},
 journal      = {Journal of Automated Reasoning},
 volume       = {54},
 number       = {4},
 pages        = {327--352},
 doi          = {10.1007/s10817-015-9323-7},
)
@book(Andrews,
 author       = {Peter B. Andrews},
 year         = {2002},
 title        = {{An introduction to mathematical logic and type theory: to truth through proof}},
 edition      = {2nd},
 series       = {{Applied Logic Series}},
 volume       = {27},
 publisher    = {Kluwer Academic Publishers},
 address      = {Dordrecht},
 doi          = {10.1007/978-94-015-9934-4},
)
@inproceedings(Biely07,
 author       = {M. Biely and Charron-Bost, B. and A. Gaillard and M. Hutle and A. Schiper and J. Widder},
 year         = {2007},
 title        = {{Tolerating corrupted communication}},
 booktitle    = {{Proc. PODC}},
 pages        = {244--253},
 doi          = {10.1145/1281100.1281136},
)
@inproceedings(sharpie,
 author       = {Bj{\o}rner, N. and K. von Gleissenthall and A. Rybalchenko},
 year         = {2016},
 title        = {{Cardinalities and Universal Quantifiers for Verifying Parameterized Systems}},
 booktitle    = {{Proc. of PLDI}},
 doi          = {10.1145/2980983.2908129},
)
@inproceedings(nuXmv,
 author       = {R. Cavada and A. Cimatti and M. Dorigatti and A. Griggio and A. Mariotti and A. Micheli and S. Mover and M. Roveri and S. Tonetta},
 year         = {2014},
 title        = {{The nuXmv Symbolic Model Checker}},
 booktitle    = {{CAV}},
 pages        = {334--342},
 doi          = {10.1007/978-3-319-08867-9_22},
)
@inproceedings(merz,
 author       = {Charron-Bost, B. and H. Debrat and S. Merz},
 year         = {2011},
 title        = {{Formal Verification of Consensus Algorithms Tolerating Malicious Faults}},
 booktitle    = {{Stabilization, Safety, and Security of Distributed Systems}},
 publisher    = {Springer LNCS},
 pages        = {120--134},
 doi          = {10.1007/978-3-642-24550-3_11},
)
@article(heardof,
 author       = {Charron-Bost, B. and A. Schiper},
 year         = {2009},
 title        = {{The heard-of model: computing in distributed systems with benign faults}},
 journal      = {Distributed Computing},
 pages        = {49--71},
 doi          = {10.1007/s00446-009-0084-6},
)
@inproceedings(ic3-tn,
 author       = {A. Cimatti and A. Griggio},
 year         = {2012},
 title        = {{Software model checking via {IC3}}},
 booktitle    = {{CAV}},
 pages        = {277--293},
 doi          = {10.1007/978-3-642-31424-7_23},
)
@article(delzannoFMSD,
 author       = {G. Delzanno},
 year         = {2003},
 title        = {{Constraint-Based Verification of Parameterized Cache Coherence Protocols}},
 journal      = {Formal Methods in System Design},
 volume       = {23},
 number       = {3},
 pages        = {257--301},
 doi          = {10.1023/A:1026276129010},
)
@inproceedings(bro2,
 author       = {G. Delzanno and J. Esparza and A. Podelski},
 year         = {1999},
 title        = {{Constraint-Based Analysis of Broadcast Protocols}},
 booktitle    = {{Proc. of CSL}},
 series       = {{LNCS}},
 volume       = {1683},
 pages        = {50--66},
 doi          = {10.1007/3-540-48168-0_5},
)
@inproceedings(dragoj,
 author       = {C. Dragoj and T. Henzinger and H. Veith and J. Widder and D. Zufferey},
 year         = {2014},
 title        = {{A Logic-based Framework for Verifying Consensus Algorithms}},
 booktitle    = {{Proc. of VMCAI}},
 doi          = {10.1007/978-3-642-54013-4_10},
)
@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(FlanaganQ02,
 author       = {C. Flanagan and S. Qadeer},
 year         = {2002},
 title        = {{Predicate abstraction for software verification}},
 booktitle    = {{POPL}},
 pages        = {191--202},
 doi          = {10.1145/565816.503291},
)
@techreport(prep,
 author       = {S. Ghilardi and E. Pagani},
 year         = {2017},
 title        = {{Second Order Quantifier Elimination: towards Verification Applications}},
 type         = {Technical Report},
 note         = {In preparation},
)
@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      = {Logical Methods in Computer Science},
 volume       = {6},
 number       = {4},
 doi          = {10.2168/LMCS-6(4:10)2010},
)
@inproceedings(GhilardiR10,
 author       = {S. Ghilardi and S. Ranise},
 year         = {2010},
 title        = {{MCMT: A Model Checker Modulo Theories}},
 booktitle    = {{IJCAR}},
 pages        = {22--29},
 doi          = {10.1007/978-3-642-14203-1_3},
)
@inproceedings(seahorn,
 author       = {Arie Gurfinkel and Temesghen Kahsai and Anvesh Komuravelli and Jorge A. Navas},
 year         = {2015},
 title        = {{The SeaHorn Verification Framework}},
 booktitle    = {{CAV}},
 pages        = {343--361},
 doi          = {10.1007/978-3-319-21690-4_20},
)
@inproceedings(pdr,
 author       = {K. Hoder and Bj{\o}rner, N.},
 year         = {2012},
 title        = {{Generalized Property Directed Reachability}},
 booktitle    = {{SAT}},
 pages        = {157--171},
 doi          = {10.1007/978-3-642-31612-8_13},
)
@inproceedings(muZ,
 author       = {K. Hoder and Bj{\o}rner, N. and L. deMoura},
 year         = {2011},
 title        = {{$\mu${Z}-- An Efficient Engine for Fixed Points with Constraints}},
 booktitle    = {{CAV}},
 pages        = {457--462},
 doi          = {10.1007/978-3-642-22110-1_36},
)
@inproceedings(konnov2013A,
 author       = {A. John and I. Konnov and U. Schmid and H. Veith and J. Widder},
 year         = {2013},
 title        = {{Parameterized model checking of fault-tolerant distributed algorithms by abstraction}},
 booktitle    = {{Proc. FMCAD}},
 pages        = {201--209},
 doi          = {10.1109/FMCAD.2013.6679411},
)
@inproceedings(konnov2013B,
 author       = {A. John and I. Konnov and U. Schmid and H. Veith and J. Widder},
 year         = {2013},
 title        = {{Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms}},
 booktitle    = {{Proc. SPIN }},
 volume       = {7976},
 pages        = {209--226},
 doi          = {10.1007/978-3-642-39176-7_14},
)
@inproceedings(KonnovVW15,
 author       = {I. Konnov and H. Veith and J. Widder},
 year         = {2015},
 title        = {{What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms}},
 booktitle    = {{ {PSI} }},
 pages        = {6--21},
 doi          = {10.1007/978-3-319-41579-6_2},
)
@article(KonnovVW17,
 author       = {I.. Konnov and H. Veith and J. Widder},
 year         = {2017},
 title        = {{On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability}},
 journal      = {Inf. Comput.},
 volume       = {252},
 pages        = {95--109},
 doi          = {10.1007/978-3-662-44584-6_10},
)
@article(KunkakJAR,
 author       = {Viktor Kuncak and Huu Hai Nguyen and Martin Rinard},
 year         = {2006},
 title        = {{Deciding {B}oolean {A}lgebra with {P}resburger {A}rithmetic}},
 journal      = {Journal of Automated Reasoning},
 volume       = {36},
 number       = {3},
 doi          = {10.1007/s10817-006-9042-1},
)
@book(LambekScott,
 author       = {J. Lambek and P. J. Scott},
 year         = {1988},
 title        = {{Introduction to higher order categorical logic}},
 series       = {{Cambridge Studies in Advanced Mathematics}},
 volume       = {7},
 publisher    = {Cambridge University Press},
 address      = {Cambridge},
)
@inproceedings(reynolds15,
 author       = {Andrew Reynolds and Morgan Deters and Viktor Kuncak and Cesare Tinelli and Clark W. Barrett},
 year         = {2015},
 title        = {Counterexample-Guided Quantifier Instantiation for Synthesis in {SMT}},
 booktitle    = {Proc. {CAV}},
 pages        = {198--216},
 doi          = {10.1007/978-3-319-21668-3_12},
)
@article(Srikanth87,
 author       = {T.K. Srikanth and S. Toueg},
 year         = {1987},
 title        = {{Optimal Clock Synchronization}},
 journal      = {Journal of the ACM},
 volume       = {34(3)},
 pages        = {626--645},
 doi          = {10.1145/28869.28876},
)
@article(toueg87,
 author       = {T.K. Srikanth and S. Toueg},
 year         = {1987},
 title        = {{Simulating authenticated broadcasts to derive simple fault-tolerant algorithms}},
 journal      = {Distributed Computing},
 volume       = {2},
 number       = {2},
 pages        = {80--94},
 doi          = {10.1007/BF01667080},
)