@inproceedings(Chen:2007:ECI:2392200.2392211,
 author       = {T. Chen and B. Ploeger and J. van de Pol and T. A. C. Willemse},
 year         = {2007},
 title        = {Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems},
 booktitle    = {Proceedings of the 18th International Conference on Concurrency Theory (CONCUR'07)},
 series       = {LNCS},
 volume       = {4703},
 publisher    = {Springer},
 address      = {Berlin, Heidelberg},
 pages        = {120--135},
 doi          = {10.1007/978-3-540-74407-8\_9},
)
@article(Clarke:2003:CAR:876638.876643,
 author       = {E. Clarke and O. Grumberg and S. Jha and Y. Lu and H. Veith},
 year         = {2003},
 title        = {Counterexample-guided Abstraction Refinement for Symbolic Model Checking},
 journal      = {Journal of ACM},
 volume       = {50},
 number       = {5},
 pages        = {752--794},
 doi          = {10.1145/876638.876643},
)
@book(Clarke:2000:MC:332656,
 author       = {E. M. Clarke, Jr. and O. Grumberg and D. A. Peled},
 year         = {1999},
 title        = {Model Checking},
 publisher    = {MIT Press},
 address      = {Cambridge, MA, USA},
)
@inproceedings(Cranen2013,
 author       = {S. Cranen and B. Luttik and T. A. C. Willemse},
 year         = {2013},
 title        = {Proof Graphs for Parameterised Boolean Equation Systems},
 booktitle    = {Proc. of the 24th International Conference on Concurrency Theory, (CONCUR 2013)},
 series       = {LNCS},
 volume       = {8052},
 publisher    = {Springer},
 pages        = {470--484},
 doi          = {10.1007/978-3-642-40184-8\_33},
)
@inproceedings(DeMoura:2008:ZES:1792734.1792766,
 author       = {De Moura, L. and Bj{\o}rner, N.},
 year         = {2008},
 title        = {Z3: An Efficient SMT Solver},
 booktitle    = {Proc. of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08)},
 series       = {LNCS},
 volume       = {4963},
 publisher    = {Springer},
 address      = {Berlin, Heidelberg},
 pages        = {337--340},
 doi          = {10.1007/978-3-540-78800-3\_24},
)
@inproceedings(emerson1991tree,
 author       = {E. A. Emerson and C. S. Jutla},
 year         = {1991},
 title        = {Tree automata, mu-calculus and determinacy},
 booktitle    = {Foundations of Computer Science, 1991. Proceedings, 32nd Annual Symposium on},
 organization = {IEEE},
 pages        = {368--377},
 doi          = {10.1109/SFCS.1991.185392},
)
@manual(parityGame,
 author       = {O. Friedmann and M. Lange},
 year         = {2017},
 title        = {The PGSolver Collection of Parity Game Solvers},
 url          = {https://github.com/tcsprojects/pgsolver/blob/master/doc/pgsolver.pdf},
)
@book(Gradel:2005:FMT:1206819,
 author       = {E. Gr\"{a}del and P. G. Kolaitis and L. Libkin and M. Marx and J. Spencer and M. Y. Vardi and Y. Venema and S. Weinstein},
 year         = {2007},
 title        = {Finite Model Theory and Its Applications},
 series       = {Texts in Theoretical Computer Science. An EATCS Series},
 publisher    = {Springer},
 doi          = {10.1007/3-540-68804-8},
)
@inproceedings(Graf1997,
 author       = {S. Graf and H. Saidi},
 year         = {1997},
 title        = {Construction of Abstract State Graphs with PVS},
 booktitle    = {Proc. of the 9th International Conference Computer Aided Verification (CAV'97)},
 series       = {LNCS},
 volume       = {1254},
 publisher    = {Springer},
 pages        = {72--83},
 doi          = {10.1007/3-540-63166-6\_10},
)
@incollection(Groote2004,
 author       = {J. F. Groote and T. Willemse},
 year         = {2004},
 title        = {Parameterised {B}oolean Equation Systems},
 booktitle    = {Proc. of 15th International Conference on Concurrency Theory (CONCUR 2004)},
 series       = {LNCS},
 volume       = {3170},
 publisher    = {Springer},
 pages        = {308--324},
 doi          = {10.1007/978-3-540-28644-8\_20},
)
@article(Groote:2005:MPD:1099102.1099103,
 author       = {J. F. Groote and T. A. C. Willemse},
 year         = {2005},
 title        = {Model-checking Processes with Data},
 journal      = {Science of Computer Programming},
 volume       = {56},
 number       = {3},
 pages        = {251--273},
 doi          = {10.1016/j.scico.2004.08.002},
)
@article(GROOTE2005332,
 author       = {J. F. Groote and T. A. C. Willemse},
 year         = {2005},
 title        = {Parameterised Boolean Equation Systems},
 journal      = {Theoretical Computer Science},
 volume       = {343},
 number       = {3},
 pages        = {332--369},
 doi          = {10.1016/j.tcs.2005.06.016},
)
@incollection(Groote2004a,
 author       = {J. F. Groote and T. A. C. Willemse},
 year         = {2004},
 title        = {A Checker for Modal Formulae for Processes with Data},
 booktitle    = {Proc. of the 2nd International Symposium on Formal Methods for Components and Objects (FMCO 2003)},
 series       = {LNCS},
 volume       = {3188},
 publisher    = {Springer},
 pages        = {223--239},
 doi          = {10.1007/978-3-540-30101-1\_10},
)
@inproceedings(Koolen2015,
 author       = {R. P. J. Koolen and T. A. C. Willemse and H. Zantema},
 year         = {2015},
 title        = {Using SMT for Solving Fragments of Parameterised Boolean Equation Systems},
 booktitle    = {Proc. of the 13th International Symposium on Automated Technology for Verification and Analysis (ATVA 2015)},
 series       = {LNCS},
 volume       = {9364},
 publisher    = {Springer},
 pages        = {14--30},
 doi          = {10.1007/978-3-319-24953-7\_3},
)
@article(Nagae2016,
 author       = {Y. Nagae and M. Sakai and H. Seki},
 year         = {2017},
 title        = {An Extension of Proof Graphs for Disjunctive Parameterised Boolean Equation Systems},
 journal      = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {235},
 pages        = {46--61},
 doi          = {10.4204/EPTCS.235.4},
)
@inproceedings(invariants,
 author       = {S. Orzan and W. Wesselink and T. A. C. Willemse},
 year         = {2009},
 title        = {Static Analysis Techniques for Parameterised Boolean Equation Systems},
 booktitle    = {Proc. of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009)},
 series       = {LNCS},
 volume       = {5505},
 publisher    = {Springer},
 pages        = {230--245},
 doi          = {10.1007/978-3-642-00768-2\_22},
)
@article(PLOEGER2011637,
 author       = {B. Ploeger and J. W. Wesselink and T. A. C. Willemse},
 year         = {2011},
 title        = {Verification of Reactive Systems via Instantiation of Parameterised Boolean Equation Systems},
 journal      = {Information and Computation},
 volume       = {209},
 number       = {4},
 pages        = {637--663},
 doi          = {10.1016/j.ic.2010.11.025},
)
@inproceedings(presburger1931vollstandigkeit,
 author       = {M. Presburger},
 year         = {1929},
 title        = {{\"U}ber die Vollst{\"a}ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen},
 booktitle    = {welchem die Addition als einzige Operation hervortritt, C. R. ler congr\`es des Math\'ematiciens des pays slaves, Warszawa},
 pages        = {92--101},
)