@article(adve,
 author       = {Sarita V. Adve and Kourosh Gharachorloo},
 year         = {1996},
 title        = {Shared Memory Consistency Models: {A} Tutorial},
 journal      = {{IEEE} Computer},
 volume       = {29},
 number       = {12},
 pages        = {66--76},
 doi          = {10.1109/2.546611},
)
@inproceedings(costabs,
 author       = {Elvira Albert and Puri Arenas and Samir Genaim and G\'{o}mez-Zamalloa, Miguel and Germ\'{a}n Puebla},
 year         = {2012},
 title        = {{COSTABS}: A Cost and Termination Analyzer for {ABS}},
 booktitle    = {Proc.\ ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation},
 publisher    = {ACM},
 pages        = {151--154},
 doi          = {10.1145/2103746.2103774},
)
@inproceedings(apet,
 author       = {Elvira Albert and Puri Arenas and G{\'{o}}mez{-}Zamalloa, Miguel and Peter Y. H. Wong},
 year         = {2013},
 title        = {aPET: a test case generation tool for concurrent objects},
 editor       = {Bertrand Meyer and Luciano Baresi and Mira Mezini},
 booktitle    = {Joint Meeting of the European Software Engineering Conference and the {ACM} {SIGSOFT} Symposium on the Foundations of Software Engineering, ESEC/FSE'13},
 publisher    = {{ACM}},
 pages        = {595--598},
 doi          = {10.1145/2491411.2494590},
)
@article(future,
 author       = {Henry C. Baker, Jr. and Carl Hewitt},
 year         = {1977},
 title        = {The Incremental Garbage Collection of Processes},
 journal      = {SIGART Bull.},
 number       = {64},
 pages        = {55--59},
 doi          = {10.1145/872736.806932},
)
@inproceedings(Bijo,
 author       = {Shiji Bijo and Einar Broch Johnsen and Ka I. Pun and S. Lizeth Tapia Tarifa},
 year         = {2016},
 title        = {An Operational Semantics of Cache Coherent Multicore Architectures},
 booktitle    = {Proceedings of the 31st Annual ACM Symposium on Applied Computing},
 series       = {SAC '16},
 publisher    = {ACM},
 pages        = {1219--1224},
 doi          = {10.1145/2851613.2851718},
)
@inproceedings(Boudol,
 author       = {G{\'{e}}rard Boudol and Gustavo Petri and Bernard P. Serpette},
 year         = {2012},
 title        = {Relaxed Operational Semantics of Concurrent Programming Languages},
 editor       = {Bas Luttik and Michel A. Reniers},
 booktitle    = {{EXPRESS/SOS}, Proc.},
 series       = {{EPTCS}},
 volume       = {89},
 pages        = {19--33},
 doi          = {10.4204/EPTCS.89.3},
)
@inproceedings(Axiom,
 author       = {Sebastian Burckhardt and Madanlal Musuvathi and Vasu Singh},
 year         = {2010},
 title        = {Verifying Local Transformations on Relaxed Memory Models},
 editor       = {Rajiv Gupta},
 booktitle    = {Compiler Construction: 19th Intl.\ Conf.\tmspace+\thinmuskip{.1667em} CC},
 publisher    = {Springer},
 pages        = {104--123},
 doi          = {10.1007/978-3-642-11970-5\_7},
)
@book(maude,
 author       = {Manuel Clavel and Francisco Dur\'{a}n and Steven Eker and Patrick Lincoln and Mart\'{\i}-Oliet, Narciso and Jos{\'e} Meseguer and Carolyn Talcott},
 year         = {2007},
 title        = {All About Maude - a High-performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic},
 publisher    = {Springer-Verlag},
 doi          = {10.1007/978-3-540-71999-1},
)
@inproceedings(damitrait,
 author       = {Ferruccio Damiani and Reiner H{\"{a}}hnle and Eduard Kamburjan and Michael Lienhardt},
 year         = {2017},
 title        = {A Unified and Formal Programming Model for Deltas and Traits},
 editor       = {Marieke Huisman and Julia Rubin},
 booktitle    = {Fundamental Approaches to Software Engineering - 20th International Conference, {FASE} 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2017},
 series       = {Lecture Notes in Computer Science},
 volume       = {10202},
 publisher    = {Springer},
 pages        = {424--441},
 doi          = {10.1007/978-3-662-54494-5\_25},
)
@inproceedings(keyabs,
 author       = {Crystal Chang Din and Richard Bubel and Reiner H{\"{a}}hnle},
 year         = {2015},
 title        = {{KeY}-{ABS}: {A} Deductive Verification Tool for the Concurrent Modelling Language {ABS}},
 editor       = {Amy P. Felty and Aart Middeldorp},
 booktitle    = {Intl.\ Conference on Automated Deduction},
 series       = {LNCS},
 volume       = {9195},
 publisher    = {Springer},
 pages        = {517--526},
 doi          = {10.1007/978-3-319-21401-6\_35},
)
@article(ding,
 author       = {Crystal Chang Din and Olaf Owe},
 year         = {2015},
 title        = {Compositional reasoning about active objects with shared futures},
 journal      = {Formal Aspects of Computing},
 volume       = {27},
 number       = {3},
 pages        = {551--572},
 doi          = {10.1007/s00165-014-0322-y},
)
@inproceedings(noc,
 author       = {Crystal Chang Din and Silvia Lizeth Tapia Tarifa and Reiner H{\"{a}}hnle and Einar Broch Johnsen},
 year         = {2015},
 title        = {History-Based Specification and Verification of Scalable Concurrent and Distributed Systems},
 editor       = {Michael J. Butler and Sylvain Conchon and Za{\"{\i}}di, Fatiha},
 booktitle    = {17th International Conference on Formal Engineering Methods, {ICFEM} 2015, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {9407},
 publisher    = {Springer},
 pages        = {217--233},
 doi          = {10.1007/978-3-319-25423-4\_14},
)
@inproceedings(dead,
 author       = {Flores{-}Montoya, Antonio and Elvira Albert and Samir Genaim},
 year         = {2013},
 title        = {May-Happen-in-Parallel Based Deadlock Analysis for Concurrent Objects},
 booktitle    = {Formal Techniques for Distributed Systems, {FMOODS/FORTE}},
 pages        = {273--288},
 doi          = {10.1007/978-3-642-38592-6\_19},
)
@inproceedings(tut,
 author       = {Reiner H{\"{a}}hnle},
 year         = {2012},
 title        = {The Abstract Behavioral Specification Language: {A} Tutorial Introduction},
 editor       = {Elena Giachino and Reiner H{\"{a}}hnle and Frank S. de Boer and Marcello M. Bonsangue},
 booktitle    = {Formal Methods for Components and Objects, 11th Intl.\ Symp., {FMCO}, Bertinoro, Italy},
 pages        = {1--37},
 doi          = {10.1007/978-3-642-40615-7\_1},
)
@inproceedings(actor,
 author       = {Carl Hewitt and Peter Bishop and Richard Steiger},
 year         = {1973},
 title        = {A universal modular {ACTOR} formalism for artificial intelligence},
 booktitle    = {Proceedings of the 3rd International Joint Conference on Artificial Intelligence},
 series       = {IJCAI'73},
 publisher    = {Morgan Kaufmann Publishers Inc.},
 pages        = {235--245},
 url          = {http://dl.acm.org/citation.cfm?id=1624775.1624804},
)
@book(promela,
 author       = {Gerard J. Holzmann},
 year         = {1991},
 title        = {Design and Validation of Computer Protocols},
 publisher    = {Prentice-Hall, Inc.},
)
@inproceedings(ABS,
 author       = {Einar Broch Johnsen and Reiner H{\"{a}}hnle and Jan Sch{\"{a}}fer and Rudolf Schlatte and Martin Steffen},
 year         = {2010},
 title        = {{ABS:} {A} Core Language for Abstract Behavioral Specification},
 editor       = {Bernhard K. Aichernig and Frank S. de Boer and Marcello M. Bonsangue},
 booktitle    = {Formal Methods for Components and Objects, 9th Intl.\ Symp., {FMCO}},
 pages        = {142--164},
 doi          = {10.1007/978-3-642-25271-6\_8},
)
@inproceedings(avocs,
 author       = {Eduard Kamburjan},
 year         = {2018},
 title        = {Detecting Deadlocks in Formal System Models with Condition Synchronization},
 booktitle    = {Accepted for Publication at AVoCS'18},
)
@inproceedings(ftscs,
 author       = {Eduard Kamburjan and Reiner H{\"a}hnle},
 year         = {2017},
 title        = {Uniform Modeling of Railway Operations},
 editor       = {Cyrille Artho and Peter Csaba {\"O}lveczky},
 booktitle    = {Formal Techniques for Safety-Critical Systems: 5th Intl.\ Workshop, FTSCS, Revised Selected Papers},
 publisher    = {Springer},
 pages        = {55--71},
 doi          = {10.1007/978-3-319-53946-1\_4},
)
@inproceedings(cyber1,
 author       = {Ehsan Khamespanah and Kirill Mechitov and Marjan Sirjani and Gul A. Agha},
 year         = {2016},
 title        = {Schedulability Analysis of Distributed Real-Time Sensor Network Applications Using Actor-Based Model Checking},
 editor       = {Dragan Bosnacki and Anton Wijs},
 booktitle    = {Model Checking Software, 23rd Intl.\ Symp., {SPIN}},
 pages        = {165--181},
 doi          = {10.1007/978-3-319-32582-8\_11},
)
@article(lamport,
 author       = {Leslie Lamport},
 year         = {1979},
 title        = {How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs},
 journal      = {{IEEE} Trans. Computers},
 volume       = {28},
 number       = {9},
 pages        = {690--691},
 doi          = {10.1109/TC.1979.1675439},
)
@inproceedings(hadoop,
 author       = {Jia{-}Chun Lin and Ingrid Chieh Yu and Einar Broch Johnsen and Ming{-}Chang Lee},
 year         = {2016},
 title        = {{ABS-YARN:} {A} Formal Framework for Modeling Hadoop {YARN} Clusters},
 editor       = {Perdita Stevens and Andrzej Wasowski},
 booktitle    = {Fundamental Approaches to Software Engineering, 19th Intl.\ Conf., {FASE}},
 pages        = {49--65},
 doi          = {10.1007/978-3-662-49665-7\_4},
)
@inproceedings(Mantel,
 author       = {Heiko Mantel and Matthias Perner and Jens Sauer},
 year         = {2014},
 title        = {Noninterference under Weak Memory Models},
 booktitle    = {{IEEE} 27th Computer Security Foundations Symp., {CSF}},
 publisher    = {{IEEE} Computer Society},
 pages        = {80--94},
 doi          = {10.1109/CSF.2014.14},
)
@inproceedings(absspl,
 author       = {Radu Muschevici and Dave Clarke and Proen{\c{c}}a, Jos{\'{e}}},
 year         = {2013},
 title        = {Executable modelling of dynamic software product lines in the {ABS} language},
 editor       = {Andreas Classen and Norbert Siegmund},
 booktitle    = {5th Intl.\ Workshop on Feature-Oriented Software Development, {FOSD}},
 pages        = {17--24},
 doi          = {10.1145/2528265.2528266},
)
@inproceedings(cafe,
 author       = {Shin Nakajima and Kokichi Futatsugi},
 year         = {1997},
 title        = {An Object-Oriented Modeling Method for Algebraic Specifications in {CafeOBJ}},
 editor       = {W. Richards Adrion and Alfonso Fuggetta and Richard N. Taylor and Anthony I. Wasserman},
 booktitle    = {Pulling Together, Proc.\ 19th Int.\ Conf.\ on Software Engineering},
 pages        = {34--44},
 doi          = {10.1145/253228.253238},
)
@book(isabelle,
 author       = {Tobias Nipkow and Markus Wenzel and Lawrence C. Paulson},
 year         = {2002},
 title        = {Isabelle/HOL: A Proof Assistant for Higher-order Logic},
 publisher    = {Springer},
 doi          = {10.1007/3-540-45949-9},
)
@book(splbook,
 author       = {Klaus Pohl and G{\"{u}}nter B{\"{o}}ckle and Frank van der Linden},
 year         = {2005},
 title        = {Software Product Line Engineering - Foundations, Principles, and Techniques},
 publisher    = {Springer},
 doi          = {10.1007/3-540-28901-1},
)
@book(variable,
 author       = {Klaus Pohl and G\"{u}nter B\"{o}ckle and Frank J. van der Linden},
 year         = {2005},
 title        = {Software Product Line Engineering: Foundations, Principles and Techniques},
 publisher    = {Springer-Verlag New York, Inc.},
 doi          = {10.1007/3-540-28901-1},
)
@inproceedings(Axiom2,
 author       = {Vijay A. Saraswat and Radha Jagadeesan and Maged Michael and Christoph von Praun},
 year         = {2007},
 title        = {A Theory of Memory Models},
 booktitle    = {Proceedings of the 12th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming},
 series       = {PPoPP '07},
 publisher    = {ACM},
 pages        = {161--172},
 doi          = {10.1145/1229428.1229469},
)
@inproceedings(Sarkar,
 author       = {Susmit Sarkar and Peter Sewell and Jade Alglave and Luc Maranget and Derek Williams},
 year         = {2011},
 title        = {Understanding {POWER} multiprocessors},
 editor       = {Mary W. Hall and David A. Padua},
 booktitle    = {Proceedings of the 32nd {ACM} {SIGPLAN} Conference on Programming Language Design and Implementation, {PLDI} 2011},
 publisher    = {{ACM}},
 pages        = {175--186},
 doi          = {10.1145/1993498.1993520},
)
@article(Schaefer2012,
 author       = {Ina Schaefer and Rick Rabiser and Dave Clarke and Lorenzo Bettini and David Benavides and Goetz Botterweck and Animesh Pathak and Salvador Trujillo and Karina Villela},
 year         = {2012},
 title        = {Software diversity: state of the art and perspectives},
 journal      = {International Journal on Software Tools for Technology Transfer},
 volume       = {14},
 number       = {5},
 pages        = {477--495},
 doi          = {10.1007/s10009-012-0253-y},
)
@inbook(kmaude,
 author       = {{\c{S}}erb{\u{a}}nu{\c{t}}{\u{a}}, Traian Florin and Ro{\c{s}}u, Grigore},
 year         = {2010},
 title        = {K-Maude: A Rewriting Based Tool for Semantics of Programming Languages},
 pages        = {104--122},
 publisher    = {Springer Berlin Heidelberg},
 doi          = {10.1007/978-3-642-16310-4\_8},
)
@article(xtso,
 author       = {Peter Sewell and Susmit Sarkar and Scott Owens and Francesco Zappa Nardelli and Magnus O. Myreen},
 year         = {2010},
 title        = {{X86-TSO}: A Rigorous and Usable Programmer's Model for x86 Multiprocessors},
 journal      = {Commun. ACM},
 volume       = {53},
 number       = {7},
 pages        = {89--97},
 doi          = {10.1145/1785414.1785443},
)
@article(noc2,
 author       = {Zeinab Sharifi and Mahdi Mosaffa and Siamak Mohammadi and Marjan Sirjani},
 year         = {2013},
 title        = {Functional and Performance Analysis of Network-on-Chips Using Actor-based Modeling and Formal Verification},
 journal      = {{ECEASST}},
 volume       = {66},
 url          = {http://dx.doi.org/10.14279/tuj.eceasst.66.890},
)
@article(rebeca,
 author       = {Marjan Sirjani and Ali Movaghar and Amin Shali and Frank S. de Boer},
 year         = {2004},
 title        = {Modeling and Verification of Reactive Systems using Rebeca},
 journal      = {Fundam. Inform.},
 volume       = {63},
 number       = {4},
 pages        = {385--410},
 url          = {http://content.iospress.com/articles/fundamenta-informaticae/fi63-4-05},
)
@manual(coq,
 author       = {{The Coq development team}},
 year         = {2004},
 title        = {The Coq proof assistant reference manual},
 organization = {LogiCal Project},
 url          = {http://coq.inria.fr},
 note         = {Version 8.0},
)
@mastersthesis(weber,
 author       = {Alexandra Weber},
 year         = {2014},
 title        = {Comparison of an operational and an axiomatic model of execution for multi-threaded programs},
 school       = {{TU Darmstadt}},
 url          = {https://hds.hebis.de/ulbda/Record/HEB350072914},
)