% thesis.bib --- bibliography of references -*-bibtex-*-

% Copyright (C) 2020 Amin Bandali <bandali at uwaterloo.ca>

% This file is part of Amin Bandali's MMath thesis.

% This thesis is free software: you can redistribute it and/or modify
% it under the terms of the GNU General Public License as published by
% the Free Software Foundation, either version 3 of the License, or
% (at your option) any later version.

% This thesis is distributed in the hope that it will be useful,
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
% GNU General Public License for more details.

% You should have received a copy of the GNU General Public License
% along with this thesis.  If not, see <https://www.gnu.org/licenses/>.

% DBLP items under CC0 (<https://dblp.org/db/about/copyright.html>).


@string{uw-drc-scs = "David R. Cheriton School of Computer Science" }

@inproceedings{DBLP:conf/re/AbbassiBDS18,
  author    = {Ali Abbassi and
               Amin Bandali and
               Nancy A. Day and
               Jos{\'{e}} Serna},
  title     = {A Comparison of the Declarative Modelling Languages B,
                  Dash, and {TLA+}},
  booktitle = {8th {IEEE} International Model-Driven Requirements
                  Engineering Workshop, MoDRE@RE 2018, Banff, AB,
                  Canada, August 20, 2018},
  pages     = {11--20},
  year      = {2018},
  crossref  = {DBLP:conf/re/2018modre},
  url       = {https://doi.org/10.1109/MoDRE.2018.00008},
  doi       = {10.1109/MoDRE.2018.00008},
  timestamp = {Thu, 14 Feb 2019 15:07:29 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/re/AbbassiBDS18},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/re/2018modre,
  editor    = {Ana Moreira and
               Gunter Mussbacher and
               Jo{\~{a}}o Ara{\'{u}}jo and
               Pablo S{\'{a}}nchez},
  title     = {8th {IEEE} International Model-Driven Requirements
                  Engineering Workshop, MoDRE@RE 2018, Banff, AB,
                  Canada, August 20, 2018},
  publisher = {{IEEE} Computer Society},
  year      = {2018},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=8500723},
  isbn      = {978-1-5386-8406-1},
  timestamp = {Thu, 14 Feb 2019 15:07:29 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/re/2018modre},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@book{DBLP:books/daglib/0068766,
  author    = {J. Michael Spivey},
  title     = {Z Notation - a reference manual {(2.} ed.)},
  series    = {Prentice Hall International Series in Computer Science},
  publisher = {Prentice Hall},
  year      = {1992},
  isbn      = {978-0-13-978529-0},
  timestamp = {Thu, 07 Apr 2011 16:16:04 +0200},
  biburl    = {https://dblp.org/rec/bib/books/daglib/0068766},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@book{Jackson:2012:SAL:2141100,
  author    = {Jackson, Daniel},
  title     = {Software Abstractions: Logic, Language, and Analysis},
  year      = {2012},
  isbn      = {0262017156, 9780262017152},
  publisher = {The MIT Press},
}

@book{DBLP:books/aw/Lamport2002,
  author    = {Leslie Lamport},
  title     = {Specifying Systems, The {TLA+} Language and Tools for
                  Hardware and Software Engineers},
  publisher = {Addison-Wesley},
  year      = {2002},
  url       = {http://research.microsoft.com/users/lamport/tla/book.html},
  isbn      = {0-3211-4306-X},
  timestamp = {Wed, 10 Jul 2019 10:47:07 +0200},
  biburl    = {https://dblp.org/rec/bib/books/aw/Lamport2002},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/toplas/Lamport94,
  author    = {Leslie Lamport},
  title     = {The Temporal Logic of Actions},
  journal   = {{ACM} Trans. Program. Lang. Syst.},
  volume    = {16},
  number    = {3},
  pages     = {872--923},
  year      = {1994},
  url       = {https://doi.org/10.1145/177492.177726},
  doi       = {10.1145/177492.177726},
  timestamp = {Wed, 14 Nov 2018 10:30:40 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/toplas/Lamport94},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/charme/YuML99,
  author    = {Yuan Yu and
               Panagiotis Manolios and
               Leslie Lamport},
  title     = {Model Checking TLA\({}^{\mbox{+}}\) Specifications},
  booktitle = {Correct Hardware Design and Verification Methods, 10th
                  {IFIP} {WG} 10.5 Advanced Research Working
                  Conference, {CHARME} '99, Bad Herrenalb, Germany,
                  September 27-29, 1999, Proceedings},
  pages     = {54--66},
  year      = {1999},
  crossref  = {DBLP:conf/charme/1999},
  url       = {https://doi.org/10.1007/3-540-48153-2\_6},
  doi       = {10.1007/3-540-48153-2\_6},
  timestamp = {Tue, 14 May 2019 10:00:39 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/charme/YuML99},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/charme/1999,
  editor    = {Laurence Pierre and
               Thomas Kropf},
  title     = {Correct Hardware Design and Verification Methods, 10th
                  {IFIP} {WG} 10.5 Advanced Research Working
                  Conference, {CHARME} '99, Bad Herrenalb, Germany,
                  September 27-29, 1999, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1703},
  publisher = {Springer},
  year      = {1999},
  url       = {https://doi.org/10.1007/3-540-48153-2},
  doi       = {10.1007/3-540-48153-2},
  isbn      = {3-540-66559-5},
  timestamp = {Tue, 14 May 2019 10:00:39 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/charme/1999},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/cai/Merz03,
  author    = {Stephan Merz},
  title     = {On the Logic of {TLA+}},
  journal   = {Computers and Artificial Intelligence},
  volume    = {22},
  number    = {3-4},
  pages     = {351--379},
  year      = {2003},
  url       = {http://www.sav.sk/index.php?lang=en\&charset=ascii\&doc=journal\&part=list\_articles\&journal\_issue\_no=882\#abstract\_2730},
  timestamp = {Wed, 15 Dec 2010 08:04:18 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/cai/Merz03},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/lpar/ChaudhuriDLM08,
  author    = {Kaustuv Chaudhuri and
               Damien Doligez and
               Leslie Lamport and
               Stephan Merz},
  title     = {A {TLA+} Proof System},
  booktitle = {Proceedings of the {LPAR} 2008 Workshops, Knowledge
                  Exchange: Automated Provers and Proof Assistants,
                  and the 7th International Workshop on the
                  Implementation of Logics, Doha, Qatar, November 22,
                  2008},
  year      = {2008},
  crossref  = {DBLP:conf/lpar/2008w},
  url       = {http://ceur-ws.org/Vol-418/paper2.pdf},
  timestamp = {Tue, 28 May 2019 16:23:47 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/lpar/ChaudhuriDLM08},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/lpar/2008w,
  editor    = {Piotr Rudnicki and
               Geoff Sutcliffe and
               Boris Konev and
               Renate A. Schmidt and
               Stephan Schulz},
  title     = {Proceedings of the {LPAR} 2008 Workshops, Knowledge
                  Exchange: Automated Provers and Proof Assistants,
                  and the 7th International Workshop on the
                  Implementation of Logics, Doha, Qatar, November 22,
                  2008},
  series    = {{CEUR} Workshop Proceedings},
  volume    = {418},
  publisher = {CEUR-WS.org},
  year      = {2008},
  url       = {http://ceur-ws.org/Vol-418},
  urn       = {urn:nbn:de:0074-418-5},
  timestamp = {Tue, 28 May 2019 16:23:47 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/lpar/2008w},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/iandc/CoquandH88,
  author    = {Thierry Coquand and
               G{\'{e}}rard P. Huet},
  title     = {The Calculus of Constructions},
  journal   = {Inf. Comput.},
  volume    = {76},
  number    = {2/3},
  pages     = {95--120},
  year      = {1988},
  url       = {https://doi.org/10.1016/0890-5401(88)90005-3},
  doi       = {10.1016/0890-5401(88)90005-3},
  timestamp = {Wed, 14 Nov 2018 10:35:06 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/iandc/CoquandH88},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/colog/CoquandP88,
  author    = {Thierry Coquand and
               Christine Paulin},
  title     = {Inductively defined types},
  booktitle = {COLOG-88, International Conference on Computer Logic,
                  Tallinn, USSR, December 1988, Proceedings},
  pages     = {50--66},
  year      = {1988},
  crossref  = {DBLP:conf/colog/1988},
  url       = {https://doi.org/10.1007/3-540-52335-9\_47},
  doi       = {10.1007/3-540-52335-9\_47},
  timestamp = {Tue, 14 May 2019 10:00:39 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/colog/CoquandP88},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/colog/1988,
  editor    = {Per Martin{-}L{\"{o}}f and
               Grigori Mints},
  title     = {COLOG-88, International Conference on Computer Logic,
                  Tallinn, USSR, December 1988, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {417},
  publisher = {Springer},
  year      = {1990},
  url       = {https://doi.org/10.1007/3-540-52335-9},
  doi       = {10.1007/3-540-52335-9},
  isbn      = {3-540-52335-9},
  timestamp = {Tue, 14 May 2019 10:00:39 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/colog/1988},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@misc{the_coq_development_team_2019_2554024,
  author    = {The Coq Development Team},
  title     = {The Coq Proof Assistant, version 8.9.0},
  month     = jan,
  year      = 2019,
  doi       = {10.5281/zenodo.2554024},
  url       = {https://doi.org/10.5281/zenodo.2554024}
}

@inproceedings{DBLP:conf/cade/MouraKADR15,
  author    = {Leonardo Mendon{\c{c}}a de Moura and
               Soonho Kong and
               Jeremy Avigad and
               Floris van Doorn and
               Jakob von Raumer},
  title     = {The Lean Theorem Prover (System Description)},
  booktitle = {Automated Deduction - {CADE-25} - 25th International
                  Conference on Automated Deduction, Berlin, Germany,
                  August 1-7, 2015, Proceedings},
  pages     = {378--388},
  year      = {2015},
  crossref  = {DBLP:conf/cade/2015},
  url       = {https://doi.org/10.1007/978-3-319-21401-6\_26},
  doi       = {10.1007/978-3-319-21401-6\_26},
  timestamp = {Tue, 14 May 2019 10:00:39 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/MouraKADR15},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/cade/2015,
  editor    = {Amy P. Felty and
               Aart Middeldorp},
  title     = {Automated Deduction - {CADE-25} - 25th International
                  Conference on Automated Deduction, Berlin, Germany,
                  August 1-7, 2015, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {9195},
  publisher = {Springer},
  year      = {2015},
  url       = {https://doi.org/10.1007/978-3-319-21401-6},
  doi       = {10.1007/978-3-319-21401-6},
  isbn      = {978-3-319-21400-9},
  timestamp = {Tue, 14 May 2019 10:00:39 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/2015},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{DBLP:conf/asm/Newcombe14,
  author    = {Chris Newcombe},
  title     = {Why {Amazon} Chose {TLA}\({}^{\mbox{+}}\)},
  year      = 2014,
  booktitle = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} -
                  4th International Conference, {ABZ} 2014, Toulouse,
                  France, June 2-6, 2014. Proceedings},
  pages     = {25-39},
  doi       = {10.1007/978-3-662-43652-3\_3},
  url       = {https://doi.org/10.1007/978-3-662-43652-3\_3},
  crossref  = {DBLP:conf/asm/2014},
  timestamp = {Tue, 14 May 2019 10:00:50 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/asm/Newcombe14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/asm/2014,
  editor    = {Yamine A{\"{\i}}t Ameur and
               Klaus{-}Dieter Schewe},
  title     = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} -
                  4th International Conference, {ABZ} 2014, Toulouse,
                  France, June 2-6, 2014. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {8477},
  publisher = {Springer},
  year      = {2014},
  url       = {https://doi.org/10.1007/978-3-662-43652-3},
  doi       = {10.1007/978-3-662-43652-3},
  isbn      = {978-3-662-43651-6},
  timestamp = {Tue, 14 May 2019 10:00:50 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/asm/2014},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@Article{DBLP:journals/csur/HatcliffLLMP12,
  author    = {John Hatcliff and Gary T. Leavens and K. Rustan
                  M. Leino and Peter M{\"{u}}ller and Matthew
                  J. Parkinson},
  title     = {Behavioral interface specification languages},
  year      = 2012,
  volume    = 44,
  number    = 3,
  pages     = {16:1--16:58},
  doi       = {10.1145/2187671.2187678},
  url       = {https://doi.org/10.1145/2187671.2187678},
  journal   = {{ACM} Comput. Surv.},
  timestamp = {Tue, 06 Nov 2018 12:50:47 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/csur/HatcliffLLMP12},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{DBLP:conf/icfem/FrappierFCCO10,
  author    = {Marc Frappier and Beno{\^{\i}}t Fraikin and Romain
                  Chossart and Rapha{\"{e}}l Chane{-}Yack{-}Fa and
                  Mohammed Ouenzar},
  title     = {Comparison of Model Checking Tools for Information
                  Systems},
  year      = 2010,
  booktitle = {Formal Methods and Software Engineering - 12th
                  International Conference on Formal Engineering
                  Methods, {ICFEM} 2010, Shanghai, China, November
                  17-19, 2010. Proceedings},
  pages     = {581-596},
  doi       = {10.1007/978-3-642-16901-4\_38},
  url       = {https://doi.org/10.1007/978-3-642-16901-4\_38},
  crossref  = {DBLP:conf/icfem/2010},
  timestamp = {Tue, 14 May 2019 10:00:50 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/icfem/FrappierFCCO10},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/icfem/2010,
  editor    = {Jin Song Dong and
               Huibiao Zhu},
  title     = {Formal Methods and Software Engineering - 12th
                  International Conference on Formal Engineering
                  Methods, {ICFEM} 2010, Shanghai, China, November
                  17-19, 2010. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {6447},
  publisher = {Springer},
  year      = {2010},
  url       = {https://doi.org/10.1007/978-3-642-16901-4},
  doi       = {10.1007/978-3-642-16901-4},
  isbn      = {978-3-642-16900-7},
  timestamp = {Tue, 14 May 2019 10:00:50 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/icfem/2010},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@Book{DBLP:series/utcs/ORegan17a,
  author    = {Gerard O'Regan},
  title     = {Concise Guide to Formal Methods - Theory, Fundamentals
                  and Industry Applications},
  year      = 2017,
  series    = {Undergraduate Topics in Computer Science},
  publisher = {Springer},
  isbn      = {978-3-319-64020-4},
  doi       = {10.1007/978-3-319-64021-1},
  url       = {https://doi.org/10.1007/978-3-319-64021-1},
  timestamp = {Fri, 11 Aug 2017 12:11:05 +0200},
  biburl    = {https://dblp.org/rec/bib/series/utcs/ORegan17a},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@Book{Nissanke_1999,
  author    = {Nissanke, Nimal},
  title     = {Formal Specification: Techniques and Applications},
  year      = 1999,
  doi       = {10.1007/978-1-4471-0791-0},
  url       = {http://dx.doi.org/10.1007/978-1-4471-0791-0},
  isbn      = 9781447107910,
  publisher = {Springer London}
}

@Book{DBLP:series/txcs/AlagarP11,
  author    = {Vangalur S. Alagar and Kasilingam Periyasamy},
  title     = {Specification of Software Systems, Second Edition},
  year      = 2011,
  series    = {Texts in Computer Science},
  publisher = {Springer},
  isbn      = {978-0-85729-276-6},
  doi       = {10.1007/978-0-85729-277-3},
  url       = {https://doi.org/10.1007/978-0-85729-277-3},
  timestamp = {Tue, 16 May 2017 14:24:38 +0200},
  biburl    = {https://dblp.org/rec/bib/series/txcs/AlagarP11},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@Book{DBLP:series/txcs/AlagarP98,
  author    = {Vangalur S. Alagar and Kasilingam Periyasamy},
  title     = {Specification of Software Systems},
  year      = 1998,
  series    = {Graduate Texts in Computer Science},
  publisher = {Springer},
  isbn      = {978-1-4757-2922-1},
  doi       = {10.1007/978-1-4757-2920-7},
  url       = {https://doi.org/10.1007/978-1-4757-2920-7},
  timestamp = {Tue, 16 May 2017 14:24:38 +0200},
  biburl    = {https://dblp.org/rec/bib/series/txcs/AlagarP98},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@Book{DBLP:books/daglib/0016252,
  author    = {Shari Lawrence Pfleeger and Joanne M. Atlee},
  title     = {Software engineering - theory and practice {(3.}  ed.)},
  year      = 2006,
  publisher = {Ellis Horwood},
  isbn      = {978-0-13-198461-5},
  timestamp = {Wed, 23 Mar 2011 16:58:38 +0100},
  biburl    = {https://dblp.org/rec/bib/books/daglib/0016252},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@book{Lauesen:2001:SRS:773258,
 author     = {Lauesen, Soren},
 title      = {Software Requirements: Styles and Techniques},
 year       = {2001},
 isbn       = {0201745704},
 edition    = {1},
 publisher  = {Pearson Education},
}

@Article{Bjorner:2007:LSL:1349804,
  title     = {Logics of Specification Languages},
  author    = {Bj{\o}rner, Dines and Henson, Martin C.},
  year      = 2007,
  month     = {Dec},
  issn      = {2193-2069},
  doi       = {10.1007/978-3-540-74107-7},
  url       = {http://dx.doi.org/10.1007/978-3-540-74107-7},
  isbn      = 9783540741077,
  journal   = {Monographs in Theoretical Computer Science. An EATCS
                  Series},
  publisher = {Springer Berlin Heidelberg}
}

@Article{Corn_lio_2000,
  author    = {Cornélio, Márcio and Borba, Paulo},
  title     = {Structuring Mechanisms for an Object-Oriented Formal
                  Specification Language},
  year      = 2000,
  pages     = {402–419},
  issn      = {1611-3349},
  doi       = {10.1007/978-3-540-44995-9_24},
  url       = {http://dx.doi.org/10.1007/978-3-540-44995-9_24},
  isbn      = 9783540449959,
  journal   = {Lecture Notes in Computer Science},
  publisher = {Springer Berlin Heidelberg}
}

@InProceedings{DBLP:conf/amast/LopezNR06,
  author    = {Natalia L{\'{o}}pez and Manuel N{\'{u}}{\~{n}}ez and
                  Ismael Rodr{\'{\i}}guez},
  title     = {Assessing the Expressivity of Formal Specification
                  Languages},
  year      = 2006,
  booktitle = {Algebraic Methodology and Software Technology, 11th
                  International Conference, {AMAST} 2006, Kuressaare,
                  Estonia, July 5-8, 2006, Proceedings},
  pages     = {220-234},
  doi       = {10.1007/11784180\_18},
  url       = {https://doi.org/10.1007/11784180\_18},
  crossref  = {DBLP:conf/amast/2006},
  timestamp = {Tue, 14 May 2019 10:00:38 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/amast/LopezNR06},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/amast/2006,
  editor    = {Michael Johnson and
               Varmo Vene},
  title     = {Algebraic Methodology and Software Technology, 11th
                  International Conference, {AMAST} 2006, Kuressaare,
                  Estonia, July 5-8, 2006, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {4019},
  publisher = {Springer},
  year      = {2006},
  url       = {https://doi.org/10.1007/11784180},
  doi       = {10.1007/11784180},
  isbn      = {3-540-35633-9},
  timestamp = {Tue, 14 May 2019 10:00:38 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/amast/2006},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@Article{DBLP:journals/infsof/SnookH01,
  author    = {Colin F. Snook and Rachel Harrison},
  title     = {Practitioners' views on the use of formal methods: an
                  industrial survey by structured interview},
  year      = 2001,
  volume    = 43,
  number    = 4,
  pages     = {275-283},
  doi       = {10.1016/S0950-5849(00)00166-X},
  url       = {https://doi.org/10.1016/S0950-5849(00)00166-X},
  journal   = {Information {\&} Software Technology},
  timestamp = {Wed, 17 May 2017 10:55:33 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/infsof/SnookH01},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@Article{DBLP:journals/fac/Zave15,
  author    = {Pamela Zave},
  title     = {A practical comparison of {Alloy} and {Spin}},
  year      = 2015,
  volume    = 27,
  number    = 2,
  pages     = {239-253},
  doi       = {10.1007/s00165-014-0302-2},
  url       = {https://doi.org/10.1007/s00165-014-0302-2},
  journal   = {Formal Asp. Comput.},
  timestamp = {Wed, 17 May 2017 14:25:34 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/fac/Zave15},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@Article{DBLP:journals/sosym/FraikinFL05,
  author    = {Beno{\^{\i}}t Fraikin and Marc Frappier and
                  R{\'{e}}gine Laleau},
  title     = {State-based versus event-based specifications for
                  information systems: a comparison of {B} and
                  \textsc{eb}\({}^{\mbox{3}}\)},
  year      = 2005,
  volume    = 4,
  number    = 3,
  pages     = {236-257},
  doi       = {10.1007/s10270-005-0083-4},
  url       = {https://doi.org/10.1007/s10270-005-0083-4},
  journal   = {Software and Systems Modeling},
  timestamp = {Mon, 19 Aug 2019 19:38:26 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/sosym/FraikinFL05},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@Article{DBLP:journals/sttt/MazzantiFS18,
  author    = {Franco Mazzanti and Alessio Ferrari and Giorgio Oronzo
                  Spagnolo},
  title     = {Towards formal methods diversity in railways: an
                  experience report with seven frameworks},
  year      = 2018,
  volume    = 20,
  number    = 3,
  pages     = {263-288},
  doi       = {10.1007/s10009-018-0488-3},
  url       = {https://doi.org/10.1007/s10009-018-0488-3},
  journal   = {{STTT}},
  timestamp = {Fri, 30 Nov 2018 13:26:45 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/sttt/MazzantiFS18},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@techreport{douceur2011memoir,
  author    = {Douceur, John (JD) and Lorch, Jay and Parno, Bryan and
                  Mickens, James and McCune, Jonathan M.},
  title     = {Memoir---Formal Specs and Correctness Proofs},
  year      = {2011},
  month     = {February},
  abstract  = {This tech report presents formal specifications for the
                  Memoir system and proofs of the system's
                  correctness. The proofs were constructed manually
                  but have been programmatically machine-verified
                  using the TLA+ Proof System. Taken together, the
                  specifications and proofs contain 61 top-level
                  definitions, 182 LET-IN definitions, 74 named
                  theorems, and 5816 discrete proof steps. The proofs
                  address only the safety of the Memoir system, not
                  the liveness of the system. Safety is proven by
                  showing that a formal low-level specification of the
                  Memoir-Basic system implements a formal high-level
                  specification of desired behavior. The proofs then
                  show that a formal specification of the Memoir-Opt
                  system implements the Memoir-Basic system.},
  publisher = {Microsoft Research},
  url       = {https://www.microsoft.com/en-us/research/publication/memoir-formal-specs-and-correctness-proofs/},
  number    = {MSR-TR-2011-19},
}

@InProceedings{DBLP:conf/wdag/Lamport11a,
  author    = {Leslie Lamport},
  title     = {Byzantizing Paxos by Refinement},
  year      = 2011,
  booktitle = {Distributed Computing - 25th International Symposium,
                  {DISC} 2011, Rome, Italy, September 20-22,
                  2011. Proceedings},
  pages     = {211-224},
  doi       = {10.1007/978-3-642-24100-0\_22},
  url       = {https://doi.org/10.1007/978-3-642-24100-0\_22},
  crossref  = {DBLP:conf/wdag/2011},
  timestamp = {Tue, 14 May 2019 10:00:54 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/wdag/Lamport11a},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/wdag/2011,
  editor    = {David Peleg},
  title     = {Distributed Computing - 25th International Symposium,
                  {DISC} 2011, Rome, Italy, September 20-22,
                  2011. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {6950},
  publisher = {Springer},
  year      = {2011},
  url       = {https://doi.org/10.1007/978-3-642-24100-0},
  doi       = {10.1007/978-3-642-24100-0},
  isbn      = {978-3-642-24099-7},
  timestamp = {Tue, 14 May 2019 10:00:54 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/wdag/2011},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{DBLP:conf/forte/LuMW11,
  author    = {Tianxiang Lu and Stephan Merz and Christoph Weidenbach},
  title     = {Towards Verification of the Pastry Protocol Using
                  TLA\({}^{\mbox{ + }}\)},
  year      = 2011,
  booktitle = {Formal Techniques for Distributed Systems - Joint 13th
                  {IFIP} {WG} 6.1 International Conference, {FMOODS}
                  2011, and 31st {IFIP} {WG} 6.1 International
                  Conference, {FORTE} 2011, Reykjavik, Iceland, June
                  6-9, 2011. Proceedings},
  pages     = {244-258},
  doi       = {10.1007/978-3-642-21461-5\_16},
  url       = {https://doi.org/10.1007/978-3-642-21461-5\_16},
  crossref  = {DBLP:conf/forte/2011},
  timestamp = {Sun, 02 Jun 2019 21:14:32 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/forte/LuMW11},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/forte/2011,
  editor    = {Roberto Bruni and
               J{\"{u}}rgen Dingel},
  title     = {Formal Techniques for Distributed Systems - Joint 13th
                  {IFIP} {WG} 6.1 International Conference, {FMOODS}
                  2011, and 31st {IFIP} {WG} 6.1 International
                  Conference, {FORTE} 2011, Reykjavik, Iceland, June
                  6-9, 2011. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {6722},
  publisher = {Springer},
  year      = {2011},
  url       = {https://doi.org/10.1007/978-3-642-21461-5},
  doi       = {10.1007/978-3-642-21461-5},
  isbn      = {978-3-642-21460-8},
  timestamp = {Sun, 02 Jun 2019 21:14:32 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/forte/2011},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{DBLP:conf/ictac/Lamport09,
  author    = {Leslie Lamport},
  title     = {The PlusCal Algorithm Language},
  year      = 2009,
  booktitle = {Theoretical Aspects of Computing - {ICTAC} 2009, 6th
                  International Colloquium, Kuala Lumpur, Malaysia,
                  August 16-20, 2009. Proceedings},
  pages     = {36-60},
  doi       = {10.1007/978-3-642-03466-4\_2},
  url       = {https://doi.org/10.1007/978-3-642-03466-4\_2},
  crossref  = {DBLP:conf/ictac/2009},
  timestamp = {Tue, 14 May 2019 10:00:38 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/ictac/Lamport09},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/ictac/2009,
  editor    = {Martin Leucker and
               Carroll Morgan},
  title     = {Theoretical Aspects of Computing - {ICTAC} 2009, 6th
                  International Colloquium, Kuala Lumpur, Malaysia,
                  August 16-20, 2009. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {5684},
  publisher = {Springer},
  year      = {2009},
  url       = {https://doi.org/10.1007/978-3-642-03466-4},
  doi       = {10.1007/978-3-642-03466-4},
  isbn      = {978-3-642-03465-7},
  timestamp = {Tue, 14 May 2019 10:00:38 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/ictac/2009},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{DBLP:conf/cade/ChaudhuriDLM10,
  author    = {Kaustuv Chaudhuri and Damien Doligez and Leslie Lamport
                  and Stephan Merz},
  title     = {Verifying Safety Properties with the {TLA+} Proof
                  System},
  year      = 2010,
  booktitle = {Automated Reasoning, 5th International Joint
                  Conference, {IJCAR} 2010, Edinburgh, UK, July 16-19,
                  2010. Proceedings},
  pages     = {142-148},
  doi       = {10.1007/978-3-642-14203-1\_12},
  url       = {https://doi.org/10.1007/978-3-642-14203-1\_12},
  crossref  = {DBLP:conf/cade/2010},
  timestamp = {Tue, 14 May 2019 10:00:39 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/ChaudhuriDLM10},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/cade/2010,
  editor    = {J{\"{u}}rgen Giesl and
               Reiner H{\"{a}}hnle},
  title     = {Automated Reasoning, 5th International Joint
                  Conference, {IJCAR} 2010, Edinburgh, UK, July 16-19,
                  2010. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {6173},
  publisher = {Springer},
  year      = {2010},
  url       = {https://doi.org/10.1007/978-3-642-14203-1},
  doi       = {10.1007/978-3-642-14203-1},
  isbn      = {978-3-642-14202-4},
  timestamp = {Tue, 14 May 2019 10:00:39 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/2010},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@techreport{ostroff2017,
  author      = {Jonathan S. Ostroff},
  title       = {Validating Software via Abstract State Specifications},
  year        = {2017},
  number      = {EECS-2017-02},
  institution = {York University},
  url         = {http://www.eecs.yorku.ca/research/techreports/2017/?abstract=EECS-2017-02}
}

@mastersthesis{farheen2018,
  author    = {{Farheen, Sabria}},
  title     = {{Improvements to Transitive-Closure-based Model
                  Checking in Alloy}},
  school    = uw-drc-scs,
  year      = {2018},
  publisher = "UWSpace",
  url       = {http://hdl.handle.net/10012/12900}
}

@InProceedings{DBLP:conf/sigmod/YanYZLWSB18,
  author    = {Xinan Yan and Linguan Yang and Hongbo Zhang and Xiayue
                  Charles Lin and Bernard Wong and Kenneth Salem and
                  Tim Brecht},
  title     = {Carousel: Low-Latency Transaction Processing for
                  Globally-Distributed Data},
  year      = 2018,
  booktitle = {Proceedings of the 2018 International Conference on
                  Management of Data, {SIGMOD} Conference 2018,
                  Houston, TX, USA, June 10-15, 2018},
  pages     = {231-243},
  doi       = {10.1145/3183713.3196912},
  url       = {https://doi.org/10.1145/3183713.3196912},
  crossref  = {DBLP:conf/sigmod/2018},
  timestamp = {Wed, 21 Nov 2018 12:44:08 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/sigmod/YanYZLWSB18},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/sigmod/2018,
  editor    = {Gautam Das and
               Christopher M. Jermaine and
               Philip A. Bernstein},
  title     = {Proceedings of the 2018 International Conference on
                  Management of Data, {SIGMOD} Conference 2018,
                  Houston, TX, USA, June 10-15, 2018},
  publisher = {{ACM}},
  year      = {2018},
  url       = {https://doi.org/10.1145/3183713},
  doi       = {10.1145/3183713},
  timestamp = {Wed, 21 Nov 2018 12:44:08 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/sigmod/2018},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@Article{DBLP:journals/scp/Harel87,
  author    = {David Harel},
  title     = {Statecharts: {A} Visual Formalism for Complex Systems},
  year      = 1987,
  volume    = 8,
  number    = 3,
  pages     = {231-274},
  doi       = {10.1016/0167-6423(87)90035-9},
  url       = {https://doi.org/10.1016/0167-6423(87)90035-9},
  journal   = {Sci. Comput. Program.},
  timestamp = {Wed, 14 Nov 2018 10:21:28 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/scp/Harel87},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{DBLP:conf/asm/BoniolW14,
  author    = {Fr{\'{e}}d{\'{e}}ric Boniol and Virginie Wiels},
  title     = {The Landing Gear System Case Study},
  year      = 2014,
  booktitle = {{ABZ} 2014: The Landing Gear Case Study - Case Study
                  Track, Held at the 4th International Conference on
                  Abstract State Machines, Alloy, B, TLA, VDM, and Z,
                  Toulouse, France, June 2-6, 2014. Proceedings},
  pages     = {1-18},
  doi       = {10.1007/978-3-319-07512-9\_1},
  url       = {https://doi.org/10.1007/978-3-319-07512-9\_1},
  crossref  = {DBLP:conf/asm/2014cst},
  timestamp = {Tue, 07 May 2019 12:19:36 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/asm/BoniolW14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/asm/2014cst,
  editor    = {Fr{\'{e}}d{\'{e}}ric Boniol and Virginie Wiels and
                  Yamine A{\"{\i}}t Ameur and Klaus{-}Dieter Schewe},
  title     = {{ABZ} 2014: The Landing Gear Case Study - Case Study
                  Track, Held at the 4th International Conference on
                  Abstract State Machines, Alloy, B, TLA, VDM, and Z,
                  Toulouse, France, June 2-6, 2014. Proceedings},
  series    = {Communications in Computer and Information Science},
  volume    = {433},
  publisher = {Springer},
  year      = {2014},
  url       = {https://doi.org/10.1007/978-3-319-07512-9},
  doi       = {10.1007/978-3-319-07512-9},
  isbn      = {978-3-319-07511-2},
  timestamp = {Tue, 07 May 2019 12:18:03 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/asm/2014cst},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@techreport{SeDa18,
  author      = {Jose Serna and Nancy A. Day and and Shahram
                  Esmaeilsabzali},
  title       = {Dash: Declarative modelling with control state
                  hierarchy (preliminary version)},
  number      = {CS-2018-04},
  institution = uw-drc-scs,
  year        = 2018
}

@misc{xtext,
  year         = {2017},
  title        = {{Xtext}},
  note         = {[Online; accessed June 15, 2018]},
  howpublished = {\url{https://eclipse.org/Xtext/}},
}

@InProceedings{DBLP:conf/sigsoft/EdwardsJT04,
  author    = {Jonathan Edwards and Daniel Jackson and Emina Torlak},
  title     = {A type system for object models},
  year      = 2004,
  booktitle = {Proceedings of the 12th {ACM} {SIGSOFT} International
                  Symposium on Foundations of Software Engineering,
                  2004, Newport Beach, CA, USA, October 31 - November
                  6, 2004},
  pages     = {189-199},
  doi       = {10.1145/1029894.1029921},
  url       = {https://doi.org/10.1145/1029894.1029921},
  crossref  = {DBLP:conf/sigsoft/2004},
  timestamp = {Tue, 06 Nov 2018 16:59:22 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/sigsoft/EdwardsJT04},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/sigsoft/2004,
  editor    = {Richard N. Taylor and Matthew B. Dwyer},
  title     = {Proceedings of the 12th {ACM} {SIGSOFT} International
                  Symposium on Foundations of Software Engineering,
                  2004, Newport Beach, CA, USA, October 31 - November
                  6, 2004},
  publisher = {{ACM}},
  year      = {2004},
  isbn      = {1-58113-855-5},
  timestamp = {Mon, 29 Nov 2004 15:56:34 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/sigsoft/2004},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@Book{DBLP:books/daglib/0020982,
  author    = {Gerard J. Holzmann},
  title     = {The {SPIN} Model Checker - primer and reference manual},
  year      = 2004,
  publisher = {Addison-Wesley},
  isbn      = {978-0-321-22862-8},
  timestamp = {Thu, 14 Apr 2011 14:43:24 +0200},
  biburl    = {https://dblp.org/rec/bib/books/daglib/0020982},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@Article{DBLP:journals/tse/ArdisCJMPSO96,
  author    = {Mark A. Ardis and John A. Chaves and Lalita Jategaonkar
                  Jagadeesan and Peter Mataga and Carlos Puchol and
                  Mark G. Staskauskas and James Von Olnhausen},
  title     = {A Framework for Evaluating Specification Methods for
                  Reactive Systems Experience Report},
  year      = 1996,
  volume    = 22,
  number    = 6,
  pages     = {378-389},
  doi       = {10.1109/32.508312},
  url       = {https://doi.org/10.1109/32.508312},
  journal   = {{IEEE} Trans. Software Eng.},
  timestamp = {Wed, 17 May 2017 10:56:35 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/tse/ArdisCJMPSO96},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@Article{DBLP:journals/toplas/LamportP99,
  author    = {Leslie Lamport and Lawrence C. Paulson},
  title     = {Should your specification language be typed},
  year      = 1999,
  volume    = 21,
  number    = 3,
  pages     = {502-526},
  doi       = {10.1145/319301.319317},
  url       = {https://doi.org/10.1145/319301.319317},
  journal   = {{ACM} Trans. Program. Lang. Syst.},
  timestamp = {Tue, 06 Nov 2018 12:51:29 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/toplas/LamportP99},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{DBLP:conf/sqamia/SullivanWKM17,
  author    = {Allison Sullivan and Kaiyuan Wang and Sarfraz Khurshid
                  and Darko Marinov},
  title     = {Evaluating State Modeling Techniques in Alloy},
  year      = 2017,
  booktitle = {Proceedings of the Sixth Workshop on Software Quality
                  Analysis, Monitoring, Improvement, and Applications,
                  Belgrade, Serbia, September 11-13, 2017},
  url       = {http://ceur-ws.org/Vol-1938/paper-sul.pdf},
  crossref  = {DBLP:conf/sqamia/2017},
  timestamp = {Tue, 28 May 2019 16:23:27 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/sqamia/SullivanWKM17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/sqamia/2017,
  editor    = {Zoran Budimac},
  title     = {Proceedings of the Sixth Workshop on Software Quality
                  Analysis, Monitoring, Improvement, and Applications,
                  Belgrade, Serbia, September 11-13, 2017},
  series    = {{CEUR} Workshop Proceedings},
  volume    = {1938},
  publisher = {CEUR-WS.org},
  year      = {2017},
  url       = {http://ceur-ws.org/Vol-1938},
  urn       = {urn:nbn:de:0074-1938-4},
  timestamp = {Tue, 28 May 2019 16:23:27 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/sqamia/2017},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@Book{DBLP:books/daglib/0067105,
  author    = {Clifford B. Jones},
  title     = {Systematic software development using {VDM} {(2.}
                  ed.)},
  year      = 1991,
  series    = {Prentice Hall International Series in Computer Science},
  publisher = {Prentice Hall},
  isbn      = {978-0-13-880733-7},
  timestamp = {Thu, 07 Apr 2011 16:16:03 +0200},
  biburl    = {https://dblp.org/rec/bib/books/daglib/0067105},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@Book{DBLP:books/sp/BorgerS2003,
  author    = {Egon B{\"{o}}rger and Robert F. St{\"{a}}rk},
  title     = {Abstract State Machines. {A} Method for High-Level
                  System Design and Analysis},
  year      = 2003,
  publisher = {Springer},
  isbn      = 3540007024,
  url       = {http://www.springer.com/computer/swe/book/978-3-540-00702-9},
  timestamp = {Wed, 31 May 2017 10:38:21 +0200},
  biburl    = {https://dblp.org/rec/bib/books/sp/BorgerS2003},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@Book{DBLP:books/daglib/0024570,
  author    = {Jean{-}Raymond Abrial},
  title     = {Modeling in Event-B - System and Software Engineering},
  year      = 2010,
  publisher = {Cambridge University Press},
  isbn      = {978-0-521-89556-9},
  doi       = {10.1017/CBO9781139195881},
  url       = {https://doi.org/10.1017/CBO9781139195881},
  timestamp = {Tue, 23 Jul 2019 16:10:34 +0200},
  biburl    = {https://dblp.org/rec/bib/books/daglib/0024570},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{DBLP:conf/b/Sekerinski98,
  author    = {Emil Sekerinski},
  title     = {Graphical Design of Reactive Systems},
  year      = 1998,
  booktitle = {B'98: Recent Advances in the Development and Use of the
                  {B} Method, Second International {B} Conference,
                  Montpellier, France, April 22-24, 1998, Proceedings},
  pages     = {182-197},
  doi       = {10.1007/BFb0053361},
  url       = {https://doi.org/10.1007/BFb0053361},
  crossref  = {DBLP:conf/b/1998},
  timestamp = {Tue, 14 May 2019 10:00:35 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/b/Sekerinski98},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/b/1998,
  editor    = {Didier Bert},
  title     = {B'98: Recent Advances in the Development and Use of the
                  {B} Method, Second International {B} Conference,
                  Montpellier, France, April 22-24, 1998, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1393},
  publisher = {Springer},
  year      = {1998},
  url       = {https://doi.org/10.1007/BFb0053349},
  doi       = {10.1007/BFb0053349},
  isbn      = {3-540-64405-9},
  timestamp = {Tue, 14 May 2019 10:00:35 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/b/1998},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@misc{uml,
  title        = {{OMG} Unified Modeling Language},
  year         = "2015",
  howpublished = "\url{http://www.omg.org/spec/UML/2.5/PDF/}",
  note         = "[Online; accessed June 15, 2018]"
}

@misc{ocl,
  title        = {{OMG} Object Constraint Specification ({OCL})
                  specification},
  howpublished = "\url{http://www.omg.org/spec/OCL/2.4/PDF}",
  note         = "[Online; accessed June 15, 2018]",
  year         = 2014
}

@Article{McMillan_1993,
  author    = {McMillan, Kenneth L.},
  title     = {The SMV System},
  year      = 1993,
  pages     = {61–85},
  doi       = {10.1007/978-1-4615-3190-6_4},
  url       = {http://dx.doi.org/10.1007/978-1-4615-3190-6_4},
  isbn      = 9781461531906,
  journal   = {Symbolic Model Checking},
  publisher = {Springer US}
}
@InProceedings{DBLP:conf/cav/CavadaCDGMMMRT14,
  author    = {Roberto Cavada and Alessandro Cimatti and Michele
                  Dorigatti and Alberto Griggio and Alessandro
                  Mariotti and Andrea Micheli and Sergio Mover and
                  Marco Roveri and Stefano Tonetta},
  title     = {The nuXmv Symbolic Model Checker},
  year      = 2014,
  booktitle = {Computer Aided Verification - 26th International
                  Conference, {CAV} 2014, Held as Part of the Vienna
                  Summer of Logic, {VSL} 2014, Vienna, Austria, July
                  18-22, 2014. Proceedings},
  pages     = {334-342},
  doi       = {10.1007/978-3-319-08867-9\_22},
  url       = {https://doi.org/10.1007/978-3-319-08867-9\_22},
  crossref  = {DBLP:conf/cav/2014},
  timestamp = {Sun, 02 Jun 2019 21:10:36 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cav/CavadaCDGMMMRT14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/cav/2014,
  editor    = {Armin Biere and
               Roderick Bloem},
  title     = {Computer Aided Verification - 26th International
                  Conference, {CAV} 2014, Held as Part of the Vienna
                  Summer of Logic, {VSL} 2014, Vienna, Austria, July
                  18-22, 2014. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {8559},
  publisher = {Springer},
  year      = {2014},
  url       = {https://doi.org/10.1007/978-3-319-08867-9},
  doi       = {10.1007/978-3-319-08867-9},
  isbn      = {978-3-319-08866-2},
  timestamp = {Tue, 14 May 2019 10:00:43 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cav/2014},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{DBLP:conf/icse/ChangJ06,
  author    = {Felix Sheng{-}Ho Chang and Daniel Jackson},
  title     = {Symbolic model checking of declarative relational
                  models},
  year      = 2006,
  booktitle = {28th International Conference on Software Engineering
                  {(ICSE} 2006), Shanghai, China, May 20-28, 2006},
  pages     = {312-320},
  doi       = {10.1145/1134285.1134329},
  url       = {https://doi.org/10.1145/1134285.1134329},
  crossref  = {DBLP:conf/icse/2006},
  timestamp = {Mon, 26 Nov 2018 12:14:46 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/icse/ChangJ06},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/icse/2006,
  editor    = {Leon J. Osterweil and H. Dieter Rombach and Mary Lou
                  Soffa},
  title     = {28th International Conference on Software Engineering
                  {(ICSE} 2006), Shanghai, China, May 20-28, 2006},
  publisher = {{ACM}},
  year      = {2006},
  url       = {https://doi.org/10.1145/1134285},
  doi       = {10.1145/1134285},
  isbn      = {1-59593-375-1},
  timestamp = {Tue, 06 Nov 2018 11:06:56 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/icse/2006},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@book{rodin-handbook,
  author    = {Jastram, Michael and Butler, Prof Michael},
  title     = {Rodin User's Handbook: Covers {R}odin v.2.8},
  year      = 2014,
  publisher = {CreateSpace Independent Publishing Platform},
  address   = {USA},
  isbn      = {1495438147, 9781495438141},
  keywords  = {Event-B},
  url       = {https://www3.hhu.de/stups/handbook/rodin/}
}

@book{b-manref,
  author    = {ClearSy},
  title     = {{B} Language Reference Manual, version 1.8.6},
  year      = 2007,
  keywords  = {Atelier-B},
  url       = {https://www.atelierb.eu/wp-content/uploads/sites/3/ressources/manref1.8.6.fr.zip}
}

@InProceedings{DBLP:conf/sam/Sherratt12,
  author    = {Edel Sherratt},
  title     = {Relativity and Abstract State Machines},
  year      = 2012,
  booktitle = {System Analysis and Modeling: Theory and Practice - 7th
                  International Workshop, {SAM} 2012, Innsbruck,
                  Austria, October 1-2, 2012. Revised Selected Papers},
  pages     = {105-120},
  doi       = {10.1007/978-3-642-36757-1\_7},
  url       = {https://doi.org/10.1007/978-3-642-36757-1\_7},
  crossref  = {DBLP:conf/sam/2012},
  timestamp = {Tue, 14 May 2019 10:00:54 +0200},
  biburl    = {https://dblp.org/rec/conf/sam/Sherratt12.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/sam/2012,
  editor    = {{\O}ystein Haugen and Rick Reed and Reinhard Gotzhein},
  title     = {System Analysis and Modeling: Theory and Practice - 7th
                  International Workshop, {SAM} 2012, Innsbruck,
                  Austria, October 1-2, 2012. Revised Selected Papers},
  series    = {Lecture Notes in Computer Science},
  volume    = {7744},
  publisher = {Springer},
  year      = {2013},
  url       = {https://doi.org/10.1007/978-3-642-36757-1},
  doi       = {10.1007/978-3-642-36757-1},
  isbn      = {978-3-642-36756-4},
  timestamp = {Tue, 14 May 2019 10:00:54 +0200},
  biburl    = {https://dblp.org/rec/conf/sam/2012.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{DBLP:conf/compsac/ZhangGS10,
  author    = {Hehua Zhang and Ming Gu and Xiaoyu Song},
  title     = {Specifying Time-Sensitive Systems with {TLA+}},
  year      = 2010,
  booktitle = {Proceedings of the 34th Annual {IEEE} International
                  Computer Software and Applications Conference,
                  {COMPSAC} 2010, Seoul, Korea, 19-23 July 2010},
  pages     = {425-430},
  doi       = {10.1109/COMPSAC.2010.50},
  url       = {https://doi.org/10.1109/COMPSAC.2010.50},
  crossref  = {DBLP:conf/compsac/2010},
  timestamp = {Wed, 16 Oct 2019 14:14:53 +0200},
  biburl    = {https://dblp.org/rec/conf/compsac/ZhangGS10.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/compsac/2010,
  editor    = {Sheikh Iqbal Ahamed and Doo{-}Hwan Bae and Sung Deok
                  Cha and Carl K. Chang and Rajesh Subramanyan and
                  Eric Wong and Hen{-}I Yang},
  title     = {Proceedings of the 34th Annual {IEEE} International
                  Computer Software and Applications Conference,
                  {COMPSAC} 2010, Seoul, Korea, 19-23 July 2010},
  publisher = {{IEEE} Computer Society},
  year      = {2010},
  url       = {https://ieeexplore.ieee.org/xpl/conhome/5676249/proceeding},
  isbn      = {978-0-7695-4085-6},
  timestamp = {Wed, 16 Oct 2019 14:14:53 +0200},
  biburl    = {https://dblp.org/rec/conf/compsac/2010.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{DBLP:conf/charme/Lamport05,
  author    = {Leslie Lamport},
  title     = {Real-Time Model Checking Is Really Simple},
  year      = 2005,
  booktitle = {Correct Hardware Design and Verification Methods, 13th
                  {IFIP} {WG} 10.5 Advanced Research Working
                  Conference, {CHARME} 2005, Saarbr{\"{u}}cken,
                  Germany, October 3-6, 2005, Proceedings},
  pages     = {162-175},
  doi       = {10.1007/11560548\_14},
  url       = {https://doi.org/10.1007/11560548\_14},
  crossref  = {DBLP:conf/charme/2005},
  timestamp = {Tue, 14 May 2019 10:00:39 +0200},
  biburl    = {https://dblp.org/rec/conf/charme/Lamport05.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/charme/2005,
  editor    = {Dominique Borrione and Wolfgang J. Paul},
  title     = {Correct Hardware Design and Verification Methods, 13th
                  {IFIP} {WG} 10.5 Advanced Research Working
                  Conference, {CHARME} 2005, Saarbr{\"{u}}cken,
                  Germany, October 3-6, 2005, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {3725},
  publisher = {Springer},
  year      = {2005},
  url       = {https://doi.org/10.1007/11560548},
  doi       = {10.1007/11560548},
  isbn      = {3-540-29105-9},
  timestamp = {Tue, 14 May 2019 10:00:39 +0200},
  biburl    = {https://dblp.org/rec/conf/charme/2005.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@misc{standardlibraryasm,
  year         = {2020},
  title        = {{StandardLibrary.asm}},
  note         = {[Online; accessed May 18, 2020]},
  howpublished = {\url{https://sourceforge.net/p/asmeta/code/HEAD/tree/asm_examples/STDL/StandardLibrary.asm}},
}

@mastersthesis{serna2019,
  author    = {{Serna, Jose}},
  title     = {{Dash: Declarative Behavioural Modelling in Alloy}},
  school    = uw-drc-scs,
  year      = {2019},
  publisher = "UWSpace",
  url       = {http://hdl.handle.net/10012/14424}
}

@Article{Maraee_2020,
  author    = {Maraee, Azzam and Sturm, Arnon},
  title     = {Imperative versus declarative constraint specification
                  languages: a controlled experiment},
  year      = 2020,
  month     = {May},
  issn      = {1619-1374},
  doi       = {10.1007/s10270-020-00796-4},
  url       = {http://dx.doi.org/10.1007/s10270-020-00796-4},
  journal   = {Software and Systems Modeling},
  publisher = {Springer Science and Business Media LLC}
}

@misc{alloy-private,
  title        = {{\alloycode{private} namespace in \alloy}},
  note         = {[Online; accessed May 21, 2020]},
  howpublished = {\url{https://alloytools.org/quickguide/private.html}},
}

@Book{DBLP:books/daglib/0015096,
  author    = {Jean{-}Raymond Abrial},
  title     = {The B-book - assigning programs to meanings},
  year      = 1996,
  publisher = {Cambridge University Press},
  isbn      = {978-0-521-02175-3},
  doi       = {10.1017/CBO9780511624162},
  url       = {https://doi.org/10.1017/CBO9780511624162},
  timestamp = {Tue, 23 Jul 2019 12:44:35 +0200},
  biburl    = {https://dblp.org/rec/books/daglib/0015096.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@misc{freesw,
  title        = {{What is free software?}},
  howpublished = {\url{https://www.gnu.org/philosophy/free-sw.html}},
  note         = {[Online; accessed May 22, 2020]},
}

@misc{gplv2,
  title        = {{GNU General Public License, version 2}},
  howpublished = {\url{https://www.gnu.org/licenses/gpl-2.0.html}},
  note         = {[Online; accessed May 22, 2020]},
}

@misc{gplv3,
  title        = {{GNU General Public License, version 3}},
  howpublished = {\url{https://www.gnu.org/licenses/gpl-3.0.html}},
  note         = {[Online; accessed May 22, 2020]},
}

@misc{asmeta-license,
  title        = {{Asmeta - License}},
  howpublished = {\url{http://asmeta.sourceforge.net/download/license.html}},
  note         = {[Online; accessed May 22, 2020]},
}

@misc{b-toolkit-license,
  title        = {{The B-Toolkit - License}},
  howpublished = {\url{https://github.com/edwardcrichton/BToolkit#license}},
  note         = {[Online; accessed May 22, 2020]},
}

@InProceedings{DBLP:conf/fm/LeuschelB03,
  author    = {Michael Leuschel and Michael J. Butler},
  title     = {{ProB}: {A} Model Checker for {B}},
  year      = 2003,
  booktitle = {{FME} 2003: Formal Methods, International Symposium of
                  Formal Methods Europe, Pisa, Italy, September 8-14,
                  2003, Proceedings},
  pages     = {855-874},
  doi       = {10.1007/978-3-540-45236-2\_46},
  url       = {https://doi.org/10.1007/978-3-540-45236-2\_46},
  crossref  = {DBLP:conf/fm/2003},
  timestamp = {Tue, 14 May 2019 10:00:46 +0200},
  biburl    = {https://dblp.org/rec/conf/fm/LeuschelB03.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/fm/2003,
  editor    = {Keijiro Araki and Stefania Gnesi and Dino Mandrioli},
  title     = {{FME} 2003: Formal Methods, International Symposium of
                  Formal Methods Europe, Pisa, Italy, September 8-14,
                  2003, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {2805},
  publisher = {Springer},
  year      = {2003},
  url       = {https://doi.org/10.1007/b13229},
  doi       = {10.1007/b13229},
  isbn      = {3-540-40828-2},
  timestamp = {Tue, 14 May 2019 10:00:46 +0200},
  biburl    = {https://dblp.org/rec/conf/fm/2003.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@misc{prob-license,
  title        = {{ProB Licence}},
  howpublished = {\url{https://www3.hhu.de/stups/prob/index.php/ProBLicence}},
  note         = {[Online; accessed May 22, 2020]},
}

@Article{DBLP:journals/sttt/AbrialBHHMV10,
  author    = {Jean{-}Raymond Abrial and Michael J. Butler and Stefan
                  Hallerstede and Thai Son Hoang and Farhad Mehta and
                  Laurent Voisin},
  title     = {Rodin: an open toolset for modelling and reasoning in
                  Event-B},
  year      = 2010,
  volume    = 12,
  number    = 6,
  pages     = {447-466},
  doi       = {10.1007/s10009-010-0145-y},
  url       = {https://doi.org/10.1007/s10009-010-0145-y},
  journal   = {Int. J. Softw. Tools Technol. Transf.},
  timestamp = {Thu, 02 Apr 2020 08:37:20 +0200},
  biburl    = {https://dblp.org/rec/journals/sttt/AbrialBHHMV10.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@misc{rodin-license,
  title        = {{Rodin Licence - Event-B.org}},
  howpublished = {\url{http://www.event-b.org/install.html}},
  note         = {[Online; accessed May 22, 2020]},
}

@InProceedings{DBLP:conf/icse/KemberTGD19,
  author    = {Mitchell Kember and Lynn Tran and George Gao and Nancy
                  A. Day},
  title     = {Extracting counterexamples from
                  transitive-closure-based model checking},
  year      = 2019,
  booktitle = {Proceedings of the 11th International Workshop on
                  Modelling in Software Engineerings, MiSE@ICSE 2019,
                  Montreal, QC, Canada, May 26-27, 2019},
  pages     = {47-54},
  doi       = {10.1109/MiSE.2019.00015},
  url       = {https://doi.org/10.1109/MiSE.2019.00015},
  crossref  = {DBLP:conf/icse/2019mise},
  timestamp = {Tue, 22 Oct 2019 12:51:22 +0200},
  biburl    = {https://dblp.org/rec/conf/icse/KemberTGD19.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/icse/2019mise,
  editor    = {Marsha Chechik and Daniel Str{\"{u}}ber and
                  D{\'{a}}niel Varr{\'{o}}},
  title     = {Proceedings of the 11th International Workshop on
                  Modelling in Software Engineerings, MiSE@ICSE 2019,
                  Montreal, QC, Canada, May 26-27, 2019},
  publisher = {{ACM}},
  year      = {2019},
  url       = {https://ieeexplore.ieee.org/xpl/conhome/8870905/proceeding},
  isbn      = {978-1-7281-2231-1},
  timestamp = {Tue, 22 Oct 2019 12:51:22 +0200},
  biburl    = {https://dblp.org/rec/conf/icse/2019mise.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@PhdThesis{DBLP:phd/basesearch/Vakili16,
  author    = {Amirhossein Vakili},
  title     = {Temporal Logic Model Checking as Automated Theorem
                  Proving},
  school    = {University of Waterloo, Ontario, Canada},
  year      = 2016,
  url       = {http://hdl.handle.net/10012/10163},
  timestamp = {Fri, 02 Jun 2017 13:52:41 +0200},
  biburl    = {https://dblp.org/rec/phd/basesearch/Vakili16.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{DBLP:conf/asm/VakiliD12,
  author    = {Amirhossein Vakili and Nancy A. Day},
  title     = {Temporal Logic Model Checking in Alloy},
  year      = 2012,
  booktitle = {Abstract State Machines, Alloy, B, VDM, and {Z} - Third
                  International Conference, {ABZ} 2012, Pisa, Italy,
                  June 18-21, 2012. Proceedings},
  pages     = {150-163},
  doi       = {10.1007/978-3-642-30885-7\_11},
  url       = {https://doi.org/10.1007/978-3-642-30885-7\_11},
  crossref  = {DBLP:conf/asm/2012},
  timestamp = {Sun, 02 Jun 2019 21:23:59 +0200},
  biburl    = {https://dblp.org/rec/conf/asm/VakiliD12.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/asm/2012,
  editor    = {John Derrick and John S. Fitzgerald and Stefania Gnesi
                  and Sarfraz Khurshid and Michael Leuschel and Steve
                  Reeves and Elvinia Riccobene},
  title     = {Abstract State Machines, Alloy, B, VDM, and {Z} - Third
                  International Conference, {ABZ} 2012, Pisa, Italy,
                  June 18-21, 2012. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {7316},
  publisher = {Springer},
  year      = {2012},
  url       = {https://doi.org/10.1007/978-3-642-30885-7},
  doi       = {10.1007/978-3-642-30885-7},
  isbn      = {978-3-642-30884-0},
  timestamp = {Sun, 02 Jun 2019 21:23:59 +0200},
  biburl    = {https://dblp.org/rec/conf/asm/2012.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@Article{DBLP:journals/sosym/FarheenDVA20,
  author    = {Sabria Farheen and Nancy A. Day and Amirhossein Vakili
                  and Ali Abbassi},
  title     = {Transitive-closure-based model checking {(TCMC)} in
                  Alloy},
  year      = 2020,
  volume    = 19,
  number    = 3,
  pages     = {721-740},
  doi       = {10.1007/s10270-019-00763-8},
  url       = {https://doi.org/10.1007/s10270-019-00763-8},
  journal   = {Software and Systems Modeling},
  timestamp = {Tue, 28 Apr 2020 11:51:42 +0200},
  biburl    = {https://dblp.org/rec/journals/sosym/FarheenDVA20.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@misc{aldb-src,
  title        = {{ALDB - A debugger for transition systems modelled
                  in \alloy}},
  howpublished = {\url{https://github.com/WatForm/aldb}},
  note         = {[Online; accessed May 25, 2020]},
}

@mastersthesis{abbassi2018,
  author    = {{Abbassi, Ali}},
  title     = {{Astra: Evaluating Translations from Alloy to SMT-LIB}},
  school    = uw-drc-scs,
  year      = {2018},
  publisher = "UWSpace",
  url       = {http://hdl.handle.net/10012/14286}
}

@unpublished{lamportslf2019,
  author    = {{Leslie Lamport}},
  title     = {{Safety, Liveness, and Fairness}},
  year      = {2019},
  month     = {May},
  note      = {\url{https://lamport.azurewebsites.net/tla/safety-liveness.pdf}}
}

@Article{DBLP:journals/scp/AptO83,
  author    = {Krzysztof R. Apt and Ernst{-}R{\"{u}}diger Olderog},
  title     = {Proof Rules and Transformations Dealing with Fairness},
  year      = 1983,
  volume    = 3,
  number    = 1,
  pages     = {65-100},
  doi       = {10.1016/0167-6423(83)90004-7},
  url       = {https://doi.org/10.1016/0167-6423(83)90004-7},
  journal   = {Sci. Comput. Program.},
  timestamp = {Sat, 27 May 2017 14:22:55 +0200},
  biburl    = {https://dblp.org/rec/journals/scp/AptO83.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@Article{DBLP:journals/tosem/Jackson02,
  author    = {Daniel Jackson},
  title     = {Alloy: a lightweight object modelling notation},
  year      = 2002,
  volume    = 11,
  number    = 2,
  pages     = {256-290},
  doi       = {10.1145/505145.505149},
  url       = {https://doi.org/10.1145/505145.505149},
  journal   = {{ACM} Trans. Softw. Eng. Methodol.},
  timestamp = {Wed, 14 Nov 2018 10:16:56 +0100},
  biburl    = {https://dblp.org/rec/journals/tosem/Jackson02.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{DBLP:conf/re/SernaDF17,
  author    = {Jos{\'{e}} Serna and Nancy A. Day and Sabria Farheen},
  title     = {{DASH:} {A} New Language for Declarative Behavioural
                  Requirements with Control State Hierarchy},
  year      = 2017,
  booktitle = {{IEEE} 25th International Requirements Engineering
                  Conference Workshops, {RE} 2017 Workshops, Lisbon,
                  Portugal, September 4-8, 2017},
  pages     = {64-68},
  doi       = {10.1109/REW.2017.70},
  url       = {https://doi.org/10.1109/REW.2017.70},
  crossref  = {DBLP:conf/re/2017w},
  timestamp = {Wed, 16 Oct 2019 14:14:56 +0200},
  biburl    = {https://dblp.org/rec/conf/re/SernaDF17.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/re/2017w,
  title     = {{IEEE} 25th International Requirements Engineering
                  Conference Workshops, {RE} 2017 Workshops, Lisbon,
                  Portugal, September 4-8, 2017},
  publisher = {{IEEE} Computer Society},
  year      = {2017},
  url       = {https://ieeexplore.ieee.org/xpl/conhome/8053951/proceeding},
  isbn      = {978-1-5386-3488-2},
  timestamp = {Wed, 16 Oct 2019 14:14:56 +0200},
  biburl    = {https://dblp.org/rec/conf/re/2017w.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@manual{pluscal-c-syntax,
  title     = {A {PlusCal} User's Manual ({C}-Syntax)},
  author    = {Leslie Lamport},
  edition   = {Version 1.8},
  month     = {August},
  year      = 2018,
  note      = {\url{https://lamport.azurewebsites.net/tla/c-manual.pdf}}
}

@manual{pluscal-p-syntax,
  title     = {A {PlusCal} User's Manual ({P}-Syntax)},
  author    = {Leslie Lamport},
  edition   = {Version 1.8},
  month     = {August},
  year      = 2018,
  note      = {\url{https://lamport.azurewebsites.net/tla/p-manual.pdf}}
}

@InProceedings{DBLP:conf/asm/ScandurraGGGR05,
  author    = {Patrizia Scandurra and Angelo Gargantini and Claudia
                  Genovese and Tiziana Genovese and Elvinia Riccobene},
  title     = {A Concrete Syntax Derived From the Abstract State
                  Machine Metamodel},
  year      = 2005,
  booktitle = {Proceedings of the 12th International Workshop on
                  Abstract State Machines, {ASM} 2005, March 8-11,
                  2005, Paris, France},
  pages     = {345-368},
  url       = {https://cs.unibg.it/gargantini/research/papers/asm05.pdf},
  crossref  = {DBLP:conf/asm/2005},
  timestamp = {Thu, 26 Jul 2007 15:03:11 +0200},
  biburl    = {https://dblp.org/rec/conf/asm/ScandurraGGGR05.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/asm/2005,
  title     = {Proceedings of the 12th International Workshop on
                  Abstract State Machines, {ASM} 2005, March 8-11,
                  2005, Paris, France},
  year      = {2005},
  timestamp = {Thu, 26 Jul 2007 15:03:11 +0200},
  biburl    = {https://dblp.org/rec/conf/asm/2005.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{conf/3m4mda/GargantiniRS06,
  title     = {Deriving a textual notation from a metamodel: an
                  experience on bridging Modelware and Grammarware},
  author    = {Gargantini, Angelo and Riccobene, Elvinia and
                  Scandurra, Patrizia},
  year      = 2006,
  booktitle = {Milestones, Models and Mappings for Model-Driven
                  Architecture: European Workshop on Milestones,
                  Models and Mappings for Model-Driven Architecture
                  (3M4MDA), Bilbao, Spain, July 11, 2006. Proceedings},
  pages     = {33-47},
  url       = {https://cs.unibg.it/gargantini/research/papers/3M4MDA_2006.pdf},
  crossref  = {conf/3m4mda/2006},
}

@proceedings{conf/3m4mda/2006,
  title     = "Milestones, Models and Mappings for Model-Driven
                  Architecture: European Workshop on Milestones,
                  Models and Mappings for Model-Driven Architecture
                  (3M4MDA), Bilbao, Spain, July 11, 2006. Proceedings",
  abstract  = "This volume contains the proceedings of the European
                  Workshop on Milestones, Models and Mappings for
                  Model-Driven Architecture (3M4MDA) held on 11 July
                  2006 in Bilbao, Spain, in conjunction with the
                  European Conference on Model Driven Architecture -
                  Foundations and Applications (ECMDA-FA 2006). The
                  3M4MDA 2006 workshop aims at helping the convergence
                  of the research and practical application, by
                  focusing on the milestones in the model-driven
                  development process, the models to be used, and
                  mappings to be established between these
                  models. Many issues have risen from the practical
                  application of the model-driven approach, most
                  notably those that relate to the purpose and the
                  characteristics of the system under design and that
                  translate to requirements on milestones, models and
                  mappings to be applied in the model-driven
                  development process. These issues should be taken
                  into account in the next generation of model-driven
                  methods and modelling techniques.",
  keywords  = "IR-67480, EWI-15479",
  editor    = "{Andrade Almeida}, Jo{\~a}o and {Ferreira Pires}, Luis
                  and {van Sinderen}, {Marten J.}",
  year      = "2006",
  language  = "English",
  series    = "CTIT Workshop Proceedings Series",
  publisher = "Centre for Telematics and Information Technology (CTIT)",
  number    = "02",
  address   = "Netherlands",
  url       = {https://research.utwente.nl/en/publications/milestones-models-and-mappings-for-model-driven-architecture-euro}
}

@Article{DBLP:journals/jucs/GargantiniRS08,
  author    = {Angelo Gargantini and Elvinia Riccobene and Patrizia
                  Scandurra},
  title     = {A Metamodel-based Language and a Simulation Engine for
                  Abstract State Machines},
  year      = 2008,
  volume    = 14,
  number    = 12,
  pages     = {1949-1983},
  doi       = {10.3217/jucs-014-12-1949},
  url       = {https://doi.org/10.3217/jucs-014-12-1949},
  journal   = {J. {UCS}},
  timestamp = {Wed, 17 May 2017 14:25:45 +0200},
  biburl    = {https://dblp.org/rec/journals/jucs/GargantiniRS08.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@techreport{gurevich1984,
  author      = {Yuri Gurevich},
  title       = {Reconsidering Turing's thesis (toward more realistic
                  semantics of programs)},
  year        = {1984},
  month       = {September},
  number      = {CRL-TR-36-84},
  institution = {University of Michigan},
  url         = {http://hdl.handle.net/2027.42/5237}
}

@InCollection{merz:inria-00338330,
  author      = {Merz, Stephan},
  title       = {{The Specification Language TLA+}},
  year        = 2008,
  booktitle   = {{Logics of specification languages}},
  editor      = {Dines Bj{{\o}}rner and Martin Henson},
  series      = {Monographs in Theoretical Computer Science},
  publisher   = {{Springer}},
  pages       = {401-452},
  url         = {https://hal.inria.fr/inria-00338330},
  hal_id      = {inria-00338330},
  hal_version = {v1}
}

@techreport{lamport1996,
  author      = {Leslie Lamport},
  title       = {The Module Structure of {TLA+}},
  year        = {1996},
  month       = {September},
  number      = {SRC-TN-1996-002A},
  institution = {{Digital Equipment Corporation (DEC)}},
  url         = {https://www.hpl.hp.com/techreports/Compaq-DEC/SRC-TN-1996-002A.pdf}
}

@Article{DBLP:journals/jcss/DeutschSV07,
  author    = {Alin Deutsch and Liying Sui and Victor Vianu},
  title     = {Specification and verification of data-driven Web
                  applications},
  year      = 2007,
  volume    = 73,
  number    = 3,
  pages     = {442-474},
  doi       = {10.1016/j.jcss.2006.10.006},
  url       = {https://doi.org/10.1016/j.jcss.2006.10.006},
  journal   = {J. Comput. Syst. Sci.},
  timestamp = {Sat, 20 May 2017 00:25:54 +0200},
  biburl    = {https://dblp.org/rec/journals/jcss/DeutschSV07.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@PhdThesis{DBLP:phd/dnb/Spielmann00,
  author    = {Marc Spielmann},
  title     = {Abstract state machines: verification problems and
                  complexity},
  school    = {{RWTH} Aachen University, Germany},
  year      = 2000,
  url       = {http://sylvester.bth.rwth-aachen.de/dissertationen/2001/008/01\_008.pdf},
  timestamp = {Wed, 12 Feb 2020 16:40:40 +0100},
  biburl    = {https://dblp.org/rec/phd/dnb/Spielmann00.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{DBLP:conf/tools/AydalUW08,
  author    = {Emine Gokce Aydal and Mark Utting and Jim Woodcock},
  title     = {A Comparison of State-Based Modelling Tools for Model
                  Validation},
  year      = 2008,
  booktitle = {Objects, Components, Models and Patterns, 46th
                  International Conference, {TOOLS} {EUROPE} 2008,
                  Zurich, Switzerland, June 30 - July 4, 2008.
                  Proceedings},
  pages     = {278-296},
  doi       = {10.1007/978-3-540-69824-1\_16},
  url       = {https://doi.org/10.1007/978-3-540-69824-1\_16},
  crossref  = {DBLP:conf/tools/46-2008},
  timestamp = {Fri, 27 Mar 2020 08:51:51 +0100},
  biburl    = {https://dblp.org/rec/conf/tools/AydalUW08.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/tools/46-2008,
  editor    = {Richard F. Paige and Bertrand Meyer},
  title     = {Objects, Components, Models and Patterns, 46th
                  International Conference, {TOOLS} {EUROPE} 2008,
                  Zurich, Switzerland, June 30 - July 4, 2008.
                  Proceedings},
  series    = {Lecture Notes in Business Information Processing},
  volume    = {11},
  publisher = {Springer},
  year      = {2008},
  isbn      = {978-3-540-69823-4},
  timestamp = {Mon, 30 Oct 2017 11:35:08 +0100},
  biburl    = {https://dblp.org/rec/conf/tools/46-2008.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@Article{DBLP:journals/cj/HuynhFPML19,
  author    = {Nghi Huynh and Marc Frappier and Herman Pooda and Amel
                  Mammar and R{\'{e}}gine Laleau},
  title     = {{SGAC:} {A} Multi-Layered Access Control Model with
                  Conflict Resolution Strategy},
  year      = 2019,
  volume    = 62,
  number    = 12,
  pages     = {1707-1733},
  doi       = {10.1093/comjnl/bxz039},
  url       = {https://doi.org/10.1093/comjnl/bxz039},
  journal   = {Comput. J.},
  timestamp = {Thu, 09 Jan 2020 09:16:11 +0100},
  biburl    = {https://dblp.org/rec/journals/cj/HuynhFPML19.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@misc{bruel2019,
    title   = {The role of formalism in system requirements (full
                  version)},
    author  = {Jean-Michel Bruel and Sophie Ebersold and Florian
                  Galinier and Alexandr Naumchev and Manuel Mazzara
                  and Bertrand Meyer},
    year    = {2019},
    eprint  = {1911.02564},
    archivePrefix = {arXiv},
    primaryClass  = {cs.SE}
}

@InProceedings{DBLP:conf/asm/LeuschelS14,
  author    = {Michael Leuschel and David Schneider},
  title     = {Towards {B} as a High-Level Constraint Modelling
                  Language - Solving the Jobs Puzzle Challenge},
  year      = 2014,
  booktitle = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} -
                  4th International Conference, {ABZ} 2014, Toulouse,
                  France, June 2-6, 2014. Proceedings},
  pages     = {101-116},
  doi       = {10.1007/978-3-662-43652-3\_8},
  url       = {https://doi.org/10.1007/978-3-662-43652-3\_8},
  crossref  = {DBLP:conf/asm/2014},
  timestamp = {Tue, 14 May 2019 10:00:50 +0200},
  biburl    = {https://dblp.org/rec/conf/asm/LeuschelS14.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{SaWiBeLe09,
  author    = {Mireille Samia and Harald Wiegard and Jens Bendisposto
                  and Michael Leuschel},
  title     = {High-Level versus Low-Level Specifications: Comparing
                  {B} with {Promela} and {ProB} with {Spin}},
  year      = {2009},
  month     = {June},
  booktitle = {Proceedings TFM-B 2009},
  pages     = {49-61},
  publisher = {APCB},
  editor    = {Attiogbe and Mery},
  url       = {https://www3.hhu.de/stups/downloads/pdf/SaWiBeLe09_307.pdf}
}

@InProceedings{DBLP:conf/tacas/TorlakJ07,
  author    = {Emina Torlak and Daniel Jackson},
  title     = {Kodkod: {A} Relational Model Finder},
  year      = 2007,
  booktitle = {Tools and Algorithms for the Construction and Analysis
                  of Systems, 13th International Conference, {TACAS}
                  2007, Held as Part of the Joint European Conferences
                  on Theory and Practice of Software, {ETAPS} 2007
                  Braga, Portugal, March 24 - April 1, 2007,
                  Proceedings},
  pages     = {632-647},
  doi       = {10.1007/978-3-540-71209-1\_49},
  url       = {https://doi.org/10.1007/978-3-540-71209-1\_49},
  crossref  = {DBLP:conf/tacas/2007},
  timestamp = {Tue, 14 May 2019 10:00:53 +0200},
  biburl    = {https://dblp.org/rec/conf/tacas/TorlakJ07.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/tacas/2007,
  editor    = {Orna Grumberg and
               Michael Huth},
  title     = {Tools and Algorithms for the Construction and Analysis
                  of Systems, 13th International Conference, {TACAS}
                  2007, Held as Part of the Joint European Conferences
                  on Theory and Practice of Software, {ETAPS} 2007
                  Braga, Portugal, March 24 - April 1, 2007,
                  Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {4424},
  publisher = {Springer},
  year      = {2007},
  url       = {https://doi.org/10.1007/978-3-540-71209-1},
  doi       = {10.1007/978-3-540-71209-1},
  isbn      = {978-3-540-71208-4},
  timestamp = {Tue, 14 May 2019 10:00:53 +0200},
  biburl    = {https://dblp.org/rec/conf/tacas/2007.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@unpublished{EWD:EWD249,
  author    = "Edsger W. Dijkstra",
  title     = "Notes on {S}tructured {P}rogramming",
  month     = apr,
  year      = "1970",
  note      = "circulated privately",
  url       = "http://www.cs.utexas.edu/users/EWD/ewd02xx/EWD249.PDF",
  fileSize  = "2054 KB"
}

@InProceedings{DBLP:conf/sigsoft/MacedoBCCK16,
  author    = {Nuno Macedo and Julien Brunel and David Chemouil and
                  Alcino Cunha and Denis Kuperberg},
  title     = {Lightweight specification and analysis of dynamic
                  systems with rich configurations},
  year      = 2016,
  booktitle = {Proceedings of the 24th {ACM} {SIGSOFT} International
                  Symposium on Foundations of Software Engineering,
                  {FSE} 2016, Seattle, WA, USA, November 13-18, 2016},
  pages     = {373-383},
  doi       = {10.1145/2950290.2950318},
  url       = {https://doi.org/10.1145/2950290.2950318},
  crossref  = {DBLP:conf/sigsoft/2016},
  timestamp = {Tue, 06 Nov 2018 16:59:23 +0100},
  biburl    = {https://dblp.org/rec/conf/sigsoft/MacedoBCCK16.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/sigsoft/2016,
  editor    = {Thomas Zimmermann and Jane Cleland{-}Huang and Zhendong
                  Su},
  title     = {Proceedings of the 24th {ACM} {SIGSOFT} International
                  Symposium on Foundations of Software Engineering,
                  {FSE} 2016, Seattle, WA, USA, November 13-18, 2016},
  publisher = {{ACM}},
  year      = {2016},
  url       = {https://doi.org/10.1145/2950290},
  doi       = {10.1145/2950290},
  isbn      = {978-1-4503-4218-6},
  timestamp = {Tue, 06 Nov 2018 16:59:23 +0100},
  biburl    = {https://dblp.org/rec/conf/sigsoft/2016.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{DBLP:conf/kbse/BrunelCCM18,
  author       = {Julien Brunel and David Chemouil and Alcino Cunha
                  and Nuno Macedo},
  title        = {The electrum analyzer: model checking relational
                  first-order temporal specifications},
  year         = 2018,
  booktitle    = {Proceedings of the 33rd {ACM/IEEE} International
                  Conference on Automated Software Engineering, {ASE}
                  2018, Montpellier, France, September 3-7, 2018},
  pages        = {884-887},
  doi          = {10.1145/3238147.3240475},
  url          = {https://doi.org/10.1145/3238147.3240475},
  crossref     = {DBLP:conf/kbse/2018},
  timestamp    = {Mon, 16 Sep 2019 15:30:05 +0200},
  biburl       = {https://dblp.org/rec/conf/kbse/BrunelCCM18.bib},
  bibsource    = {dblp computer science bibliography,
                  https://dblp.org}
}

@proceedings{DBLP:conf/kbse/2018,
  editor    = {Marianne Huchard and
               Christian K{\"{a}}stner and
               Gordon Fraser},
  title     = {Proceedings of the 33rd {ACM/IEEE} International Conference on Automated
               Software Engineering, {ASE} 2018, Montpellier, France, September 3-7,
               2018},
  publisher = {{ACM}},
  year      = {2018},
  url       = {https://doi.org/10.1145/3238147},
  doi       = {10.1145/3238147},
  timestamp = {Wed, 21 Nov 2018 12:44:20 +0100},
  biburl    = {https://dblp.org/rec/conf/kbse/2018.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@Article{DBLP:journals/sttt/CunhaM20,
  author    = {Alcino Cunha and Nuno Macedo},
  title     = {Validating the Hybrid {ERTMS/ETCS} Level 3 concept with
                  Electrum},
  year      = 2020,
  volume    = 22,
  number    = 3,
  pages     = {281-296},
  doi       = {10.1007/s10009-019-00540-4},
  url       = {https://doi.org/10.1007/s10009-019-00540-4},
  journal   = {Int. J. Softw. Tools Technol. Transf.},
  timestamp = {Mon, 15 Jun 2020 16:56:45 +0200},
  biburl    = {https://dblp.org/rec/journals/sttt/CunhaM20.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
