The Human in Formal Methods

  • Shriram KrishnamurthiEmail author
  • Tim Nelson
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11800)


Formal methods are invaluable for reasoning about complex systems. As these techniques and tools have improved in expressiveness and scale, their adoption has grown rapidly. Sustaining this growth, however, requires attention to not only the technical but also the human side. In this paper (and accompanying talk), we discuss some of the challenges and opportunities for human factors in formal methods.


Human factors User Interfaces Education Formal methods 



This work was partially supported by the U.S. National Science Foundation. We are grateful for numerous valuable conversations with Daniel J. Dougherty, Natasha Danas, Jack Wrenn, Kathi Fisler, Daniel Jackson, and Emina Torlak.


  1. 1.
    Amazon Web Services: Provable security. Accessed 5 July 2019
  2. 2.
    Autexier, S., Benzmüller, C. (eds.): User Interfaces for Theorem Provers, Proceedings of UITP 2006, Electronic Notes in Theoretical Computer Science, vol. 174. Elsevier (2007)Google Scholar
  3. 3.
    Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and static driver verifier: technology transfer of formal methods inside microsoft. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) IFM 2004. LNCS, vol. 2999, pp. 1–20. Springer, Heidelberg (2004). Scholar
  4. 4.
    Barker-Plummer, D., Barwise, J., Etchemendy, J.: Language, Proof, and Logic, 2nd edn. Center for the Study of Language and Information/SRI, Stanford (2011)zbMATHGoogle Scholar
  5. 5.
    du Boulay, B., O’Shea, T., Monk, J.: The black box inside the glass box. Int. J. Hum.-Comput. Stud. 51(2), 265–277 (1999)CrossRefGoogle Scholar
  6. 6.
    Calcagno, C., et al.: Moving fast with software verification. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 3–11. Springer, Cham (2015). Scholar
  7. 7.
    Cook, B.: Formal reasoning about the security of amazon web services. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 38–47. Springer, Cham (2018). Scholar
  8. 8.
    Danas, N., Nelson, T., Harrison, L., Krishnamurthi, S., Dougherty, D.J.: User studies of principled model finder output. In: Cimatti, A., Sirjani, M. (eds.) SEFM 2017. LNCS, vol. 10469, pp. 168–184. Springer, Cham (2017). Scholar
  9. 9.
    Felleisen, M., Findler, R.B., Flatt, M., Krishnamurthi, S.: How to Design Programs, 2nd edn. MIT Press, Cambridge (2018). Scholar
  10. 10.
    Findler, R.B., et al.: DrScheme: a programming environment for Scheme. J. Funct. Prog. 12(2), 159–182 (2002)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Fisler, K., Krishnamurthi, S., Meyerovich, L., Tschantz, M.: Verification and change impact analysis of access-control policies. In: International Conference on Software Engineering, pp. 196–205 (2005)Google Scholar
  12. 12.
    Fogel, A., et al.: A general approach to network configuration analysis. In: Networked Systems Design and Implementation (2015)Google Scholar
  13. 13.
    Fyfe, E.R., McNeil, N.M., Son, J.Y., Goldstone, R.L.: Concreteness fading in mathematics and science instruction: a systematic review. Educ. Psychol. Rev. 26(1), 9–25 (2014)CrossRefGoogle Scholar
  14. 14.
    Holt, R.C., Wortman, D.B.: A sequence of structured subsets of PL/I. SIGCSE Bull. 6(1), 129–132 (1974)CrossRefGoogle Scholar
  15. 15.
    Jackson, D.: Software Abstractions: Logic, Language, and Analysis, 2nd edn. MIT Press, Cambridge (2012)Google Scholar
  16. 16.
    Jackson, D., Wing, J.: Lightweight formal methods. IEEE Comput. (1996)Google Scholar
  17. 17.
    Loksa, D., Ko, A.J.: The role of self-regulation in programming problem solving process and success. In: SIGCSE International Computing Education Research Conference (2016)Google Scholar
  18. 18.
    McCune, W.: Mace4 reference manual and guide. CoRR (2003).
  19. 19.
    Milazzo, P., Varró, D., Wimmer, M. (eds.): STAF 2016. LNCS, vol. 9946. Springer, Cham (2016). Scholar
  20. 20.
    Nelson, T., Ferguson, A.D., Krishnamurthi, S.: Static differential program analysis for software-defined networks. In: Bjørner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 395–413. Springer, Cham (2015). Scholar
  21. 21.
    Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How amazon web services uses formal methods. Commun. ACM 58(4), 66–73 (2015)CrossRefGoogle Scholar
  22. 22.
    Pirolli, P.L., Anderson, J.R.: The role of learning from examples in the acquisition of recursive programming skills. Canadian Journal of Psychology/Revue canadienne de psychologie 39(2), 240–272 (1985)CrossRefGoogle Scholar
  23. 23.
    Politz, J.G., Krishnamurthi, S., Fisler, K.: In-flow peer-review of tests in test-first programming. In: Conference on International Computing Education Research (2014)Google Scholar
  24. 24.
    Prather, J., et al.: First things first: providing metacognitive scaffolding for interpreting problem prompts. In: ACM Technical Symposium on Computer Science Education (2019)Google Scholar
  25. 25.
    Prather, J., Pettit, R., McMurry, K., Peters, A., Homer, J., Cohen, M.: Metacognitive difficulties faced by novice programmers in automated assessment tools. In: SIGCSE International Computing Education Research Conference (2018)Google Scholar
  26. 26.
    Seger, C.H.: Combining functional programming and hardware verification (abstract of invited talk). In: International Conference on Functional Programming (ICFP) (2000)Google Scholar
  27. 27.
    Spohrer, J.C., Soloway, E.: Simulating Student Programmers. In: IJCAI 1989, pp. 543–549. Morgan Kaufmann Publishers Inc. (1989)Google Scholar
  28. 28.
    Sweller, J.: The worked example effect and human cognition. Learn. Instr. 16(2), 165–169 (2006)CrossRefGoogle Scholar
  29. 29.
    Vygotsky, L.S.: Mind in Society: The Development of Higher Psychological Processes. Harvard University Press, Cambridge (1978)Google Scholar
  30. 30.
    Whalley, J., Kasto, N.: A qualitative think-aloud study of novice programmers’ code writing strategies. In: Conference on Innovation and Technology in Computer Science Education (2014)Google Scholar
  31. 31.
    Wood, D., Bruner, J.S., Ross, G.: The role of tutoring in problem solving. J. Child Psychol. Psychiatry 17, 89–100 (1976)CrossRefGoogle Scholar
  32. 32.
    Wrenn, J., Krishnamurthi, S.: Executable examples for programming problem comprehension. In: SIGCSE International Computing Education Research Conference (2019)Google Scholar
  33. 33.
    Wrenn, J., Krishnamurthi, S., Fisler, K.: Who tests the testers? In: SIGCSE International Computing Education Research Conference, pp. 51–59 (2018)Google Scholar
  34. 34.
    Zhang, J., Zhang, H.: SEM: a system for enumerating models. In: International Joint Conference on Artificial Intelligence (1995)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Brown UniversityProvidenceUSA

Personalised recommendations