@misc(rv-match-url,
 note         = {\url{https://runtimeverification.com/match/}},
)
@misc(k-framework-c-semantics-url,
 note         = {\url{https://github.com/kframework/c-semantics}},
)
@misc(k-framework-url,
 note         = {\url{http://kframework.org/}},
)
@misc(cerberus-url,
 note         = {\url{https://cerberus.cl.cam.ac.uk/}},
)
@misc(Coq-url,
 note         = {\url{https://coq.inria.fr/}},
)
@inproceedings(future,
 author       = {Henry G. Baker and Carl E. Hewitt},
 year         = {1977},
 title        = {The Incremental Garbage Collection of Processes},
 booktitle    = {Proceeding of the Symposium on Artificial Intelligence Programming Languages},
 series       = {SIGPLAN Notices},
 volume       = {12},
 pages        = {11},
 doi          = {10.1145/872734.806932},
)
@misc(Barrett2010TheSS,
 author       = {Clark W. Barrett and Aaron Stump and Cesare Tinelli},
 year         = {2010},
 title        = {The SMT-LIB Standard Version 2.0},
 note         = {Https://homepage.cs.uiowa.edu/~tinelli/papers/BarST-SMT-10.pdf},
)
@misc(acsl,
 author       = {Patrick Baudin and Pascal Cuoq and Jean-Christophe Filliâtre and Claude Marché and Benjamin Monate and Yannick Moy and Virgile Prevosto},
 year         = {2018},
 title        = {{ACSL: ANSI/ISO C} Specification Language Version 1.14},
 note         = {\url{https://frama-c.com/acsl.html}},
)
@article(boer,
 author       = {Frank S. de Boer and Vlad Serbanescu and Reiner H{\"{a}}hnle and Ludovic Henrio and Justine Rochas and Crystal Chang Din and Einar Broch Johnsen and Marjan Sirjani and Ehsan Khamespanah and Fernandez{-}Reyes, Kiko and Albert Mingkun Yang},
 year         = {2017},
 title        = {A Survey of Active Object Languages},
 journal      = {{ACM} Comput. Surv.},
 volume       = {50},
 number       = {5},
 pages        = {76:1--76:39},
 doi          = {10.1145/3122848},
)
@inproceedings(BubelHT19,
 author       = {Richard Bubel and Reiner H{\"{a}}hnle and {Heydari Tabar}, Asmae},
 year         = {2019},
 title        = {A Program Logic for Dependence Analysis},
 booktitle    = {{IFM}},
 series       = {{LNCS}},
 volume       = {11918},
 pages        = {83--100},
 doi          = {10.1007/978-3-030-34968-4\_5},
)
@misc(framamanual,
 author       = {David B{\"u}hler and Pascal Cuoq and Boris Yakobowski},
 year         = {2020},
 title        = {Eva – The Evolved Value Analysis plug-in, Manual v21.1},
 url          = {https://frama-c.com/download/frama-c-eva-manual.pdf},
)
@inproceedings(CEGAR,
 author       = {Edmund Clarke and Orna Grumberg and Somesh Jha and Yuan Lu and Helmut Veith},
 year         = {2000},
 title        = {Counterexample-Guided Abstraction Refinement},
 editor       = {E. Allen Emerson and Aravinda Prasad Sistla},
 booktitle    = {{CAV}},
 publisher    = {Springer},
 pages        = {154--169},
 doi          = {10.1007/10722167\_15},
)
@inproceedings(framac,
 author       = {Pascal Cuoq and Florent Kirchner and Nikolai Kosmatov and Virgile Prevosto and Julien Signoles and Boris Yakobowski},
 year         = {2012},
 title        = {Frama-C: A Software Analysis Perspective},
 booktitle    = {{SEFM}},
 publisher    = {Springer-Verlag},
 pages        = {233–247},
 doi          = {10.1007/978-3-642-33826-7\_16},
)
@misc(fred,
 author       = {Crystal Chang Din and Richard Bubel and Reiner H{\"a}hnle and Elena Giachino and Cosimo Laneve and Michael Lienhardt},
 year         = {2015},
 title        = {{Deliverable D3.2 Verification of project FP7-610582 (ENVISAGE)}},
 url          = {http://www.envisage-project.eu},
)
@article(DinO15,
 author       = {Crystal Chang Din and Olaf Owe},
 year         = {2015},
 title        = {Compositional reasoning about active objects with shared futures},
 journal      = {Formal Asp. Comput.},
 volume       = {27},
 number       = {3},
 pages        = {551--572},
 doi          = {10.1007/s00165-014-0322-y},
)
@inproceedings(ellison2012,
 author       = {Chucky Ellison and Grigore Rosu},
 year         = {2012},
 title        = {An executable formal semantics of {C} with applications},
 booktitle    = {{POPL}'12},
 publisher    = {{ACM}},
 pages        = {533--544},
 doi          = {10.1145/2103656.2103719},
)
@inproceedings(FruminGK19,
 author       = {Dan Frumin and L{\'{e}}on Gondelman and Robbert Krebbers},
 year         = {2019},
 title        = {Semi-automated Reasoning About Non-determinism in {C} Expressions},
 booktitle    = {{ESOP}},
 series       = {{LNCS}},
 volume       = {11423},
 pages        = {60--87},
 doi          = {10.1007/978-3-030-17184-1\_3},
)
@inproceedings(HahnleTMNS020,
 author       = {Reiner H{\"{a}}hnle and {Heydari Tabar}, Asmae and Arya Mazaheri and Mohammad Norouzi and Dominic Steinh{\"{o}}fel and Felix Wolf},
 year         = {2020},
 title        = {Safer Parallelization},
 booktitle    = {ISoLA {(2)}},
 series       = {Lecture Notes in Computer Science},
 volume       = {12477},
 publisher    = {Springer},
 pages        = {117--137},
 doi          = {10.1007/978-3-030-61470-6\_8},
)
@inproceedings(k-framework-c-semantics,
 author       = {Chris Hathhorn and Chucky Ellison and Ro\c{s}u, Grigore},
 year         = {2015},
 title        = {Defining the Undefinedness of C},
 booktitle    = {Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'15)},
 publisher    = {ACM},
 pages        = {336--345},
 doi          = {10.1145/2813885.2737979},
)
@inproceedings(lam1,
 author       = {Ludovic Henrio and Cosimo Laneve and Vincenzo Mastandrea},
 year         = {2017},
 title        = {Analysis of Synchronisations in Stateful Active Objects},
 editor       = {Nadia Polikarpova and Steve Schneider},
 booktitle    = {Integrated Formal Methods},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {195--210},
 doi          = {10.1007/978-3-319-66845-1\_13},
)
@inproceedings(actor,
 author       = {Carl Hewitt and Peter Bishop and Richard Steiger},
 year         = {1973},
 title        = {A universal modular {ACTOR} formalism for artificial intelligence},
 booktitle    = {IJCAI'73},
 publisher    = {Morgan Kaufmann Publishers Inc.},
 pages        = {235--245},
 url          = {http://dl.acm.org/citation.cfm?id=1624775.1624804},
)
@article(HolzmannS02,
 author       = {Gerard J. Holzmann and Margaret H. Smith},
 year         = {2002},
 title        = {An Automated Verification Method for Distributed Systems Software Based on Model Extraction},
 journal      = {{IEEE} Trans.\ Software Eng.},
 volume       = {28},
 number       = {4},
 pages        = {364--377},
 doi          = {10.1109/TSE.2002.995426},
)
@misc(ISO:C99,
 author       = {ISO},
 year         = {1999},
 title        = {{ISO} {C} Standard 1999},
 url          = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1124.pdf},
 note         = {ISO/IEC 9899:1999 draft},
)
@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    = {FMCO 2010},
 series       = {{LNCS}},
 volume       = {6957},
 publisher    = {Springer},
 pages        = {142--164},
 doi          = {10.1007/978-3-642-25271-6\_8},
)
@article(avocs,
 author       = {Eduard Kamburjan},
 year         = {2018},
 title        = {Detecting Deadlocks in Formal System Models with Condition Synchronization},
 journal      = {{ECEASST}},
 volume       = {76},
 doi          = {10.14279/tuj.eceasst.76.1070},
)
@inproceedings(Kamburjan19,
 author       = {Eduard Kamburjan},
 year         = {2019},
 title        = {Behavioral Program Logic},
 booktitle    = {{TABLEAUX}},
 series       = {{LNCS}},
 volume       = {11714},
 publisher    = {Springer},
 pages        = {391--408},
 doi          = {10.1007/978-3-030-29026-9\_22},
)
@misc(soa,
 author       = {Eduard Kamburjan and Crystal Chang Din and Reiner H{\"{a}}hnle and Einar Broch Johnsen},
 year         = {2020},
 title        = {Behavioral Contracts for Cooperative Scheduling},
 doi          = {10.1007/978-3-030-64354-6\_4},
)
@inproceedings(wao,
 author       = {Eduard Kamburjan and Reiner H{\"{a}}hnle},
 year         = {2018},
 title        = {Prototyping Formal System Models with Active Objects},
 booktitle    = {{ICE}},
 series       = {{EPTCS}},
 volume       = {279},
 pages        = {52--67},
 doi          = {10.4204/EPTCS.279.7},
)
@article(arxivmarco,
 author       = {Eduard Kamburjan and Marco Scaletta and Nils Rollshausen},
 year         = {2021},
 title        = {Crowbar: Behavioral Symbolic Execution for Deductive Verification of Active Objects},
 journal      = {CoRR},
 volume       = {abs/2102.10127},
 url          = {https://arxiv.org/abs/2102.10127},
)
@inproceedings(Krebbers14,
 author       = {Robbert Krebbers},
 year         = {2014},
 title        = {An operational and axiomatic semantics for non-determinism and sequence points in {C}},
 booktitle    = {{POPL}'14},
 publisher    = {{ACM}},
 pages        = {101--112},
 doi          = {10.1145/2535838.2535878},
)
@inproceedings(gianluca,
 author       = {Torgeir Lebesbye and Jacopo Mauro and Gianluca Turin and Ingrid Chieh Yu},
 year         = {2021},
 title        = {Boreas - {A} Service Scheduler for Optimal Kubernetes Deployment},
 booktitle    = {{ICSOC}},
 series       = {Lecture Notes in Computer Science},
 volume       = {13121},
 publisher    = {Springer},
 pages        = {221--237},
 doi          = {10.1007/978-3-030-91431-8\_14},
)
@article(yarn,
 author       = {Jia{-}Chun Lin and Ming{-}Chang Lee and Ingrid Chieh Yu and Einar Broch Johnsen},
 year         = {2020},
 title        = {A configurable and executable model of Spark Streaming on Apache YARN},
 journal      = {International Journal of Grid and Utility Computing},
 volume       = {11},
 number       = {2},
 pages        = {185--195},
 doi          = {10.1504/IJGUC.2020.105531},
)
@inproceedings(cerberus,
 author       = {Kayvan Memarian and Justus Matthiesen and James Lingard and Kyndylan Nienhuis and David Chisnall and Robert N. M. Watson and Peter Sewell},
 year         = {2016},
 title        = {Into the depths of {C:} elaborating the de facto standards},
 booktitle    = {37th PLDI},
 publisher    = {{ACM}},
 pages        = {1--15},
 doi          = {10.1145/2908080.2908081},
)
@techreport(norrish1998,
 author       = {Michael Norrish},
 year         = {1998},
 title        = {{C formalised in HOL}},
 type         = {Technical Report},
 number       = {UCAM-CL-TR-453},
 institution  = {University of Cambridge, Computer Laboratory},
 url          = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-453.pdf},
)
@article(papaspyrou2001,
 author       = {Nikolaos S Papaspyrou},
 year         = {2001},
 title        = {Denotational semantics of {ANSI C}},
 journal      = {Computer Standards \& Interfaces},
 volume       = {23},
 number       = {3},
 pages        = {169--185},
 doi          = {10.1016/S0920-5489(01)00059-9},
)
@article(k-framework,
 author       = {Ro{\c s}u, Grigore and {\c S}erb{\u a}nu{\c t}{\u a}, Traian Florin},
 year         = {2010},
 title        = {An Overview of the {K} Semantic Framework},
 journal      = {Journal of Logic and Algebraic Programming},
 volume       = {79},
 number       = {6},
 pages        = {397--434},
 doi          = {10.1016/j.jlap.2010.03.012},
)
@inproceedings(WasserHH19,
 author       = {Nathan Wasser and {Heydari Tabar}, Asmae and Reiner H{\"{a}}hnle},
 year         = {2019},
 title        = {Modeling Non-deterministic {C} Code with Active Objects},
 booktitle    = {{FSEN}},
 series       = {{LNCS}},
 volume       = {11761},
 pages        = {213--227},
 doi          = {10.1007/978-3-030-34968-4\_5},
)
@article(WasserHH21,
 author       = {Nathan Wasser and {Heydari Tabar}, Asmae and Reiner Hähnle},
 year         = {2021},
 title        = {Automated model extraction: From non-deterministic C code to active objects},
 journal      = {Science of Computer Programming},
 volume       = {204},
 pages        = {102597},
 doi          = {10.1016/j.scico.2020.102597},
)