@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},
 series       = {CONCUR'07},
 publisher    = {Springer-Verlag},
 address      = {Berlin, Heidelberg},
 pages        = {120--135},
 url          = {http://dl.acm.org/citation.cfm?id=2392200.2392211},
)
@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      = {J. 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},
)
@inbook(Cranen2013,
 author       = {S. Cranen and B. Luttik and T. A. C. Willemse},
 year         = {2013},
 title        = {Proof Graphs for Parameterised Boolean Equation Systems},
 pages        = {470--484},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 doi          = {10.1007/978-3-642-40184-8\_33},
)
@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         = {2005},
 title        = {Finite Model Theory and Its Applications (Texts in Theoretical Computer Science. An EATCS Series)},
 publisher    = {Springer-Verlag New York, Inc.},
 address      = {Secaucus, NJ, USA},
)
@inbook(Graf1997,
 author       = {S. Graf and H. Saidi},
 year         = {1997},
 title        = {Construction of abstract state graphs with PVS},
 pages        = {72--83},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 doi          = {10.1007/3-540-63166-6\_10},
)
@inbook(Groote2004,
 author       = {J. F. Groote and T. Willemse},
 year         = {2004},
 title        = {Parameterised Boolean Equation Systems},
 pages        = {308--324},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 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      = {Sci. Comput. Program.},
 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},
)
@inbook(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},
 pages        = {14--30},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 doi          = {10.1007/978-3-319-24953-7\_3},
)
@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},
)
@book(presburger1931vollständigkeit,
 author       = {M. Presburger},
 year         = {1931},
 title        = {{\"U}ber die Vollst{\"a}ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt},
 publisher    = {publisher not identified},
 url          = {https://books.google.co.jp/books?id=7agKHQAACAAJ},
)