Reasoning About Iteration and Recursion Uniformly Based on Big-Step Semantics

1. The Coq proof assistant. https://coq.inria.fr/

2. Michelson - the language of Tezos. https://www.michelson.org/

3. The move language. https://developers.libra-china.org/docs/crates/move-language/index.html

4. A sequential imperative programming language - syntax, semantics, Hoare logics and verification environment. https://www.isa-afp.org/entries/Simpl.html

5. Solidity. https://docs.soliditylang.org/en/v0.8.0/

6. VCC: A verifier for concurrent C. https://www.microsoft.com/en-us/research/project/vcc-a-verifier-for-concurrent-c/

7. Yul. https://docs.soliditylang.org/en/v0.8.0/yul.html

8. Formalization of the verification technique in Coq (2021). https://github.com/lixm/ind-verify/tree/master

9. Ahrendt, W., Beckert, B., Bubel, R. (eds.): Deductive Software Verification - The KeY Book. From Theory to Practice. Lecture Notes in Computer Science, vol. 10001. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-319-49812-6

   Book  Google Scholar 

10. Appel, A.W.: Verified Software Toolchain - (invited talk). In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 1–17. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19718-5_1

    Chapter  Google Scholar 

11. Blazy, S., Leroy, X.: Mechanized semantics for the Clight subset of the C language. J. Autom. Reason. 43(3), 263–288 (2009)

    Article  MathSciNet  Google Scholar 

12. Bodin, M., Gardner, P., Jensen, T.P., Schmitt, A.: Skeletal semantics and their interpretations. Proc. ACM Program. Lang. 3(POPL), 44:1–44:31 (2019)

    Google Scholar 

13. Bodin, M., Jensen, T.P., Schmitt, A.: Certified abstract interpretation with pretty-big-step semantics. In: Proceedings of the 2015 Conference on Certified Programs and Proofs (CPP), pp. 29–40 (2015)

    Google Scholar 

14. Cavalcanti, A., Wellings, A., Woodcock, J.: The safety-critical Java memory model: a formal account. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 246–261. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21437-0_20

    Chapter  Google Scholar 

15. Clément, D., Despeyroux, J., Despeyroux, T., Kahn, G.: A simple applicative language: mini-ML. In: Proceedings of the 1986 ACM Conference on LISP and Functional Programming (LFP), pp. 13–27 (1986)

    Google Scholar 

16. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Fourth ACM Symposium on Principles of Programming Languages (POPL), pp. 238–252 (1977)

    Google Scholar 

17. Hirai, Y., et al.: Defining the ethereum virtual machine for interactive theorem provers. In: Brenner, M. (ed.) FC 2017. LNCS, vol. 10323, pp. 520–535. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-70278-0_33

    Chapter  Google Scholar 

18. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)

    Article  Google Scholar 

19. Hoare, C.A.R., He, J.: Unifying Theories of Programming. Pearson College Div (1998)

    Google Scholar 

20. Jung, R., Krebbers, R., Jourdan, J., et al.: Iris from the ground up: a modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28, e20 (2018)

    Article  MathSciNet  Google Scholar 

21. Kahn, G.: Natural semantics. In: Brandenburg, F.J., Vidal-Naquet, G., Wirsing, M. (eds.) STACS 1987. LNCS, vol. 247, pp. 22–39. Springer, Heidelberg (1987). https://doi.org/10.1007/BFb0039592

    Chapter  Google Scholar 

22. Ke, W., Li, X., Liu, Z., Stolz, V.: rCOS: a formal model-driven engineering method for component-based software. Front. Comput. Sci. China 6(1), 17–39 (2012)

    MathSciNet  MATH  Google Scholar 

23. Klein, G., Nipkow, T.: Jinja is not Java. Arch. Formal Proofs (2005)

    Google Scholar 

24. McCarthy, J.: Towards a mathematical science of computation. In: Proceedings of the 2nd IFIP Congress on Information Processing, pp. 21–28 (1962)

    Google Scholar 

25. Moore, B., Peña, L., Rosu, G.: Program verification by coinduction. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 589–618. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89884-1_21

    Chapter  Google Scholar 

26. Moore, J.S.: Inductive assertions and operational semantics. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 289–303. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-39724-3_27

    Chapter  Google Scholar 

27. Nielson, H.R., Nielson, F.: Semantics with Applications: An Appetizer. Undergraduate Topics in Computer Science, Springer, Heidelberg (2007). https://doi.org/10.1007/978-1-84628-692-6

    Book  MATH  Google Scholar 

28. Nipkow, T., von Oheimb, D.: Java\({}_{light}\) is type-safe - definitely. In: Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 161–170 (1998)

    Google Scholar 

29. Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP semantics for Circus. Formal Aspects Comput. 21(1–2), 3–32 (2009)

    Article  Google Scholar 

30. Pierce, B.C.: The science of deep specification (keynote). In: Visser, E. (ed.) Companion Proceedings of the 2016 ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH), p. 1 (2016)

    Google Scholar 

31. Plotkin, G.D.: A structural approach to operational semantics. Lecture notes, DAIMI FN-19 (1981)

    Google Scholar 

32. Qin, S., Dong, J.S., Chin, W.-N.: A semantic foundation for TCOZ in unifying theories of programming. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 321–340. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45236-2_19

    Chapter  Google Scholar 

33. Reynolds, J.C.: Theories of Programming Languages. Cambridge University Press, Cambridge (1998)

    Book  Google Scholar 

34. Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceeding of 17th IEEE Symposium on Logic in Computer Science (LICS), pp. 55–74 (2002)

    Google Scholar 

35. Schmidt, D.A.: Natural-semantics-based abstract interpretation (preliminary version). In: Mycroft, A. (ed.) SAS 1995. LNCS, vol. 983, pp. 1–18. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-60360-3_28

    Chapter  Google Scholar 

36. Sergey, I., Nagaraj, V., Johannsen, J., et al.: Safer smart contract programming with Scilla. Proc. ACM Program. Lang. 3(OOPSLA), 185:1–185:30 (2019)

    Google Scholar 

37. Sewell, T.A.L., Myreen, M.O., Klein, G.: Translation validation for a verified OS kernel. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 471–482 (2013)

    Google Scholar 

38. Sheng, F., Zhu, H., He, J., et al.: Theoretical and practical approaches to the denotational semantics for MDESL based on UTP. Formal Aspects Comput. 32(2–3), 275–314 (2020)

    Article  MathSciNet  Google Scholar 

39. Sozeau, M., Anand, A., Boulier, S., et al.: The MetaCoq project. J. Autom. Reason. 64(5), 947–999 (2020)

    Article  MathSciNet  Google Scholar 

40. Stefanescu, A., Park, D., Yuwen, S., et al.: Semantics-based program verifiers for all languages. In: 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pp. 74–91 (2016)

    Google Scholar 

41. Wood, G.: Ethereum: a secure decentralised generlised transaction ledger. https://gavwood.com/paper.pdf

42. Yang, Z., Lei, H.: Lolisa: formal syntax and semantics for a subset of the Solidity programming language. CoRR, abs/1803.09885 (2018)

    Google Scholar 

Download references