# Formal Methods

Several authors have proposed formal models of FaaS. Jangda et al. [1] and Obetz et al. [2] both introduce formal models of FaaS and event-driven computation. Gabrielli et al. [3] propose the Serverless Kernel Calculus, which is similar and includes a stateful extension. Burckhardt et al. [4] analyze durable functions in the context of a formal model, providing one demonstration of the value of these techniques.

- [1]Abhinav Jangda, Donald Pinckney, Yuriy Brun, and Arjun Guha. 2019. Formal Foundations of Serverless Computing.
*Proceedings of the ACM on Programming Languages*3, OOPSLA (2019), 1–26. - [2]Matthew Obetz, Anirban Das, Timothy Castiglia, Stacy Patterson, and Ana Milanova. 2020. Formalizing Event-Driven Behavior of Serverless Applications. In
*European Conference on Service-Oriented and Cloud Computing*, Springer, 19–29. - [3]Maurizio Gabbrielli, Saverio Giallorenzo, Ivan Lanese, Fabrizio Montesi, Marco Peressotti, and Stefano Pio Zingaro. 2019. No More, No Less - A Formal Model for Serverless Computing. In
*International Conference on Coordination Languages and Models*, Springer, 148–157. - [4]Sebastian Burckhardt, Chris Gillum, David Justo, Konstantinos Kallas, Connor McMahon, and Christopher S. Meiklejohn. 2021. Durable Functions: Semantics for Stateful Serverless.
*Proceedings of the ACM on Programming Languages*5, OOPSLA (2021), 1–27.