Abstract
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.
Keywords
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Amazon Web Services: Provable security. https://aws.amazon.com/security/provable-security/. Accessed 5 July 2019
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)
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). https://doi.org/10.1007/978-3-540-24756-2_1
Barker-Plummer, D., Barwise, J., Etchemendy, J.: Language, Proof, and Logic, 2nd edn. Center for the Study of Language and Information/SRI, Stanford (2011)
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)
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). https://doi.org/10.1007/978-3-319-17524-9_1
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). https://doi.org/10.1007/978-3-319-96145-3_3
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). https://doi.org/10.1007/978-3-319-66197-1_11
Felleisen, M., Findler, R.B., Flatt, M., Krishnamurthi, S.: How to Design Programs, 2nd edn. MIT Press, Cambridge (2018). https://www.htdp.org/
Findler, R.B., et al.: DrScheme: a programming environment for Scheme. J. Funct. Prog. 12(2), 159–182 (2002)
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)
Fogel, A., et al.: A general approach to network configuration analysis. In: Networked Systems Design and Implementation (2015)
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)
Holt, R.C., Wortman, D.B.: A sequence of structured subsets of PL/I. SIGCSE Bull. 6(1), 129–132 (1974)
Jackson, D.: Software Abstractions: Logic, Language, and Analysis, 2nd edn. MIT Press, Cambridge (2012)
Jackson, D., Wing, J.: Lightweight formal methods. IEEE Comput. (1996)
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)
McCune, W.: Mace4 reference manual and guide. CoRR (2003). https://arxiv.org/abs/cs.SC/0310055
Milazzo, P., Varró, D., Wimmer, M. (eds.): STAF 2016. LNCS, vol. 9946. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-50230-4
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). https://doi.org/10.1007/978-3-319-19249-9_25
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)
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)
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)
Prather, J., et al.: First things first: providing metacognitive scaffolding for interpreting problem prompts. In: ACM Technical Symposium on Computer Science Education (2019)
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)
Seger, C.H.: Combining functional programming and hardware verification (abstract of invited talk). In: International Conference on Functional Programming (ICFP) (2000)
Spohrer, J.C., Soloway, E.: Simulating Student Programmers. In: IJCAI 1989, pp. 543–549. Morgan Kaufmann Publishers Inc. (1989)
Sweller, J.: The worked example effect and human cognition. Learn. Instr. 16(2), 165–169 (2006)
Vygotsky, L.S.: Mind in Society: The Development of Higher Psychological Processes. Harvard University Press, Cambridge (1978)
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)
Wood, D., Bruner, J.S., Ross, G.: The role of tutoring in problem solving. J. Child Psychol. Psychiatry 17, 89–100 (1976)
Wrenn, J., Krishnamurthi, S.: Executable examples for programming problem comprehension. In: SIGCSE International Computing Education Research Conference (2019)
Wrenn, J., Krishnamurthi, S., Fisler, K.: Who tests the testers? In: SIGCSE International Computing Education Research Conference, pp. 51–59 (2018)
Zhang, J., Zhang, H.: SEM: a system for enumerating models. In: International Joint Conference on Artificial Intelligence (1995)
Acknowledgements
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.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Krishnamurthi, S., Nelson, T. (2019). The Human in Formal Methods. In: ter Beek, M., McIver, A., Oliveira, J. (eds) Formal Methods – The Next 30 Years. FM 2019. Lecture Notes in Computer Science(), vol 11800. Springer, Cham. https://doi.org/10.1007/978-3-030-30942-8_1
Download citation
DOI: https://doi.org/10.1007/978-3-030-30942-8_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-30941-1
Online ISBN: 978-3-030-30942-8
eBook Packages: Computer ScienceComputer Science (R0)