Skip to main content
SpringerLink
Log in

The Human in Formal Methods

  • Conference paper
  • First Online:
Formal Methods – The Next 30 Years (FM 2019)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11800))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Amazon Web Services: Provable security. https://aws.amazon.com/security/provable-security/. Accessed 5 July 2019

  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. 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

    Chapter  Google Scholar 

  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)

    MATH  Google Scholar 

  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)

    Article  Google Scholar 

  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). https://doi.org/10.1007/978-3-319-17524-9_1

    Chapter  Google Scholar 

  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). https://doi.org/10.1007/978-3-319-96145-3_3

    Chapter  Google Scholar 

  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). https://doi.org/10.1007/978-3-319-66197-1_11

    Chapter  Google Scholar 

  9. Felleisen, M., Findler, R.B., Flatt, M., Krishnamurthi, S.: How to Design Programs, 2nd edn. MIT Press, Cambridge (2018). https://www.htdp.org/

    MATH  Google Scholar 

  10. Findler, R.B., et al.: DrScheme: a programming environment for Scheme. J. Funct. Prog. 12(2), 159–182 (2002)

    Article  MathSciNet  Google Scholar 

  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. Fogel, A., et al.: A general approach to network configuration analysis. In: Networked Systems Design and Implementation (2015)

    Google Scholar 

  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)

    Article  Google Scholar 

  14. Holt, R.C., Wortman, D.B.: A sequence of structured subsets of PL/I. SIGCSE Bull. 6(1), 129–132 (1974)

    Article  Google Scholar 

  15. Jackson, D.: Software Abstractions: Logic, Language, and Analysis, 2nd edn. MIT Press, Cambridge (2012)

    Google Scholar 

  16. Jackson, D., Wing, J.: Lightweight formal methods. IEEE Comput. (1996)

    Google Scholar 

  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. McCune, W.: Mace4 reference manual and guide. CoRR (2003). https://arxiv.org/abs/cs.SC/0310055

  19. 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

    Book  Google Scholar 

  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). https://doi.org/10.1007/978-3-319-19249-9_25

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Article  Google Scholar 

  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. 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. 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. Seger, C.H.: Combining functional programming and hardware verification (abstract of invited talk). In: International Conference on Functional Programming (ICFP) (2000)

    Google Scholar 

  27. Spohrer, J.C., Soloway, E.: Simulating Student Programmers. In: IJCAI 1989, pp. 543–549. Morgan Kaufmann Publishers Inc. (1989)

    Google Scholar 

  28. Sweller, J.: The worked example effect and human cognition. Learn. Instr. 16(2), 165–169 (2006)

    Article  Google Scholar 

  29. Vygotsky, L.S.: Mind in Society: The Development of Higher Psychological Processes. Harvard University Press, Cambridge (1978)

    Google Scholar 

  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. Wood, D., Bruner, J.S., Ross, G.: The role of tutoring in problem solving. J. Child Psychol. Psychiatry 17, 89–100 (1976)

    Article  Google Scholar 

  32. Wrenn, J., Krishnamurthi, S.: Executable examples for programming problem comprehension. In: SIGCSE International Computing Education Research Conference (2019)

    Google Scholar 

  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. Zhang, J., Zhang, H.: SEM: a system for enumerating models. In: International Joint Conference on Artificial Intelligence (1995)

    Google Scholar 

Download references

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

  1. Brown University, Providence, RI, USA

    Shriram Krishnamurthi & Tim Nelson

Authors
  1. Shriram Krishnamurthi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Tim Nelson
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Shriram Krishnamurthi .

Editor information

Editors and Affiliations

  1. Consiglio Nazionale delle Ricerche, Pisa, Italy

    Maurice H. ter Beek

  2. Macquarie University, Sydney, NSW, Australia

    Annabelle McIver

  3. University of Minho, Braga, Portugal

    José N. Oliveira

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

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)

Publish with us

Policies and ethics

Search

Navigation