References

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