Advertisement

Deductive Verification in Decidable Fragments with Ivy

  • Kenneth L. McMillanEmail author
  • Oded Padon
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11002)

Abstract

This paper surveys the work to date on Ivy, a language and a tool for the formal specification and verification of distributed systems. Ivy supports deductive verification using automated provers, model checking, automated testing, manual theorem proving and generation of executable code. In order to achieve greater verification productivity, a key design goal for Ivy is to allow the engineer to apply automated provers in the realm in which their performance is relatively predictable, stable and transparent. In particular Ivy focuses on the use of decidable fragments of first-order logic. We consider the rationale or Ivy’s design, the various capabilities of the tool, as well as case studies and applications.

Keywords

Deductive verification Distributed systems Safety verification Liveness verification Paxos Decidable logics Effectively propositional logic Cache coherence Model checking Specification-based testing 

Notes

Acknowledgements

We thank the many researchers that have contributed to the research agenda reviewed in this article, both as co-authors and via insightful discussions, including: Thomas Ball, Amir Ben-Amram, Nikolaj Bjørner, Tej Chajed, Constantin Enea, Yotam M. Y. Feldman, Jochen Hoenicke, Neil Immerman, Shachar Itzhaky, Ranjit Jhala, K. Rustan M. Leino, Giuliano Losa, Yuri Meshman, Leonardo de Moura, Alexander Nutz, Aurojit Panda, Bryan Parno, Andreas Podelski, Shaz Qadeer, Alexander Rabinovich, Mooly Sagiv, Sharon Shoham, Or Tamir, Zachary Tatlock, Marcelo Taube, James R. Wilcox, Doug Woos, and the anonymous referees and artifact evaluation referees of POPL, PLDI, OOPSLA, CAV, and FMCAD.

Padon was supported by Google under a PhD fellowship and by the European Research Council under the European Union’s Seventh Framework Program (FP7/2007–2013)/ERC grant agreement no. [321174-VSSC].

References

  1. 1.
    Abadi, M.: The power of temporal proofs. Theor. Comput. Sci. 65(1), 35–83 (1989).  https://doi.org/10.1016/0304-3975(89)90138-2MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Abadi, M., Lamport, L.: The existence of refinement mappings. Theor. Comput. Sci. 82(2), 253–284 (1991).  https://doi.org/10.1016/0304-3975(91)90224-PMathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825–885. IOS Press (2009).  https://doi.org/10.3233/978-1-58603-929-5-825
  4. 4.
    Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-662-07964-5CrossRefzbMATHGoogle Scholar
  5. 5.
    Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. Electr. Notes Theor. Comput. Sci. 66(2), 160–177 (2002)CrossRefGoogle Scholar
  6. 6.
    Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Technical report 11/2, Institute for Formal Models and Verification, Johannes Kepler University, July 2011Google Scholar
  7. 7.
    Black, D.L., Rashid, R.F., Golub, D.B., Hill, C.R.: Translation lookaside buffer consistency: a software approach. In: Proceedings of the Third International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS III, pp. 113–122. ACM, New York (1989).  https://doi.org/10.1145/70082.68193
  8. 8.
    Blundell, C., Giannakopoulou, D., Pasareanu, C.S.: Assume-guarantee testing. ACM SIGSOFT Softw. Eng. Notes 31(2) (2006).  https://doi.org/10.1145/1118537.1123060
  9. 9.
    Boyer, R., Moore, J.: A Computational Logic. Academic Press, New York (1979)zbMATHGoogle Scholar
  10. 10.
    Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24–40. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-14295-6_5CrossRefGoogle Scholar
  11. 11.
    Ferraiuolo, A., Baumann, A., Hawblitzel, C., Parno, B.: Komodo: using verification to disentangle secure-enclave hardware from software. In: Proceedings of the 26th Symposium on Operating Systems Principles, Shanghai, China, 28–31 October 2017, pp. 287–305 (2017)Google Scholar
  12. 12.
    Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, PLDI 2002, pp. 234–245. ACM (2002).  https://doi.org/10.1145/512529.512558
  13. 13.
    Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306–320. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-02658-4_25CrossRefGoogle Scholar
  14. 14.
    Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S.T.V., Zill, B.: Ironfleet: proving practical distributed systems correct. In: Proceedings of the 25th Symposium on Operating Systems Principles, SOSP, pp. 1–17 (2015)Google Scholar
  15. 15.
    Henriksen, J.G., Jensen, J., Jørgensen, M., Klarlund, N., Paige, R., Rauhe, T., Sandholm, A.: Mona: monadic second-order logic in practice. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 89–110. Springer, Heidelberg (1995).  https://doi.org/10.1007/3-540-60630-0_5CrossRefGoogle Scholar
  16. 16.
    Itzhaky, S.: Automatic reasoning for pointer programs using decidable logics. Ph.D. thesis, Tel Aviv University (2014)Google Scholar
  17. 17.
    Itzhaky, S., Banerjee, A., Immerman, N., Lahav, O., Nanevski, A., Sagiv, M.: Modular reasoning about heap paths via effectively propositional formulas. In: the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, pp. 385–396 (2014)Google Scholar
  18. 18.
    Itzhaky, S., Banerjee, A., Immerman, N., Nanevski, A., Sagiv, M.: Effectively-propositional reasoning about reachability in linked data structures. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 756–772. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39799-8_53CrossRefGoogle Scholar
  19. 19.
    Lamport, L.: The part-time parliament. ACM Trans. Comput. Syst. 16(2), 133–169 (1998).  https://doi.org/10.1145/279227.279229CrossRefGoogle Scholar
  20. 20.
    Lamport, L.: Paxos made simple. ACM SIGACT News 32(4), 51–58 (2001). https://www.microsoft.com/en-us/research/publication/paxos-made-simple/Google Scholar
  21. 21.
    Lamport, L., Malkhi, D., Zhou, L.: Stoppable paxos. Technical report, Microsoft Research (2008). https://www.microsoft.com/en-us/research/publication/stoppable-paxos/
  22. 22.
    Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-17511-4_20CrossRefzbMATHGoogle Scholar
  23. 23.
    Manna, Z., Pnueli, A.: Verification of concurrent programs: a temporal proof system. In: de Bakker, J.W., van Leeuwen, J. (eds.) Foundations of Computer Science: Distributed Systems, pp. 163–255. Mathematisch Centrum, Amsterdam (1983)Google Scholar
  24. 24.
    McMillan, K.L.: Eager abstraction for symbolic model checking. In: Conference on Computer-Aided Verification (CAV 2018). Springer (2018, to appear)Google Scholar
  25. 25.
    McMillan, K.L.: Ivy. http://microsoft.github.io/ivy/. Accessed 7 May 2018
  26. 26.
    McMillan, K.L.: Modular specification and verification of a cache-coherent interface. In: Piskac, R., Talupur, M. (eds.) 2016 Formal Methods in Computer-Aided Design, FMCAD 2016, Mountain View, CA, USA, 3–6 October 2016, pp. 109–116. IEEE (2016).  https://doi.org/10.1109/FMCAD.2016.7886668
  27. 27.
    de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78800-3_24CrossRefGoogle Scholar
  28. 28.
    Nelson, C.G.: Techniques for program verification. Ph.D. thesis, Stanford, CA, USA (1980). aAI8011683Google Scholar
  29. 29.
    Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979)CrossRefGoogle Scholar
  30. 30.
    Nipkow, T., Wenzel, M., Paulson, L.C.: A Proof Assistant for Higher-Order Logic Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45949-9CrossRefzbMATHGoogle Scholar
  31. 31.
    Ongaro, D., Ousterhout, J.K.: In search of an understandable consensus algorithm. In: 2014 USENIX Annual Technical Conference, USENIX ATC 2014, Philadelphia, PA, USA, 19–20 June 2014, pp. 305–319 (2014). https://www.usenix.org/conference/atc14/technical-sessions/presentation/ongaro
  32. 32.
    Padon, O.: Deductive verification of distributed protocols in first-order logic. Ph.D. thesis, Tel Aviv University (2018)Google Scholar
  33. 33.
    Padon, O., Hoenicke, J., Losa, G., Podelski, A., Sagiv, M., Shoham, S.: Reducing liveness to safety in first-order logic. PACMPL 2(POPL), 26:1–26:33 (2018).  https://doi.org/10.1145/3158114CrossRefGoogle Scholar
  34. 34.
    Padon, O., Hoenicke, J., McMillan, K.L., Podelski, A., Sagiv, M., Shoham, S.: Temporal prophecy for proving temporal properties of infinite-state systems (in preparation)Google Scholar
  35. 35.
    Padon, O., Immerman, N., Shoham, S., Karbyshev, A., Sagiv, M.: Decidability of inferring inductive invariants. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, 20–22 January 2016, pp. 217–231 (2016).  https://doi.org/10.1145/2837614.2837640
  36. 36.
    Padon, O., Losa, G., Sagiv, M., Shoham, S.: Paxos made epr: Decidable reasoning about distributed protocols. Proc. ACM Program. Lang. 1(OOPSLA), 108:1–108:31 (2017).  https://doi.org/10.1145/3140568CrossRefGoogle Scholar
  37. 37.
    Padon, O., Losa, G., Sagiv, M., Shoham, S.: Paxos made EPR: decidable reasoning about distributed protocols. CoRR abs/1710.07191 (2017). http://arxiv.org/abs/1710.07191
  38. 38.
    Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: safety verification by interactive generalization. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, 13–17 June 2016, pp. 614–630 (2016)Google Scholar
  39. 39.
    Pnueli, A., Shahar, E.: Liveness and acceleration in parameterized verification. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 328–343. Springer, Heidelberg (2000).  https://doi.org/10.1007/10722167_26CrossRefzbMATHGoogle Scholar
  40. 40.
    Swamy, N., Chen, J., Fournet, C., Strub, P., Bhargavan, K., Yang, J.: Secure distributed programming with value-dependent types. J. Funct. Program. 4(23), 402–451 (2013)MathSciNetCrossRefGoogle Scholar
  41. 41.
    Taube, M., Losa, G., McMillan, K.L., Padon, O., Sagiv, M., Shoham, S., Wilcox, J.R., Woos, D.: Modularity for decidability of deductive verification with applications to distributed systems. In: Foster, J.S., Grossman, D. (eds.) Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, 18–22 June 2018, pp. 662–677. ACM (2018).  https://doi.org/10.1145/3192366.3192414
  42. 42.
    Wilcox, J.R., Woos, D., Panchekha, P., Tatlock, Z., Wang, X., Ernst, M.D., Anderson, T.E.: Verdi: a framework for implementing and formally verifying distributed systems. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, 15–17 June 2015, pp. 357–368 (2015)Google Scholar
  43. 43.
    Woos, D., Wilcox, J.R., Anton, S., Tatlock, Z., Ernst, M.D., Anderson, T.E.: Planning for change in a formal verification of the raft consensus protocol. In: Avigad, J., Chlipala, A. (eds.) Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, 20–22 January 2016, pp. 154–165. ACM (2016).  https://doi.org/10.1145/2854065.2854081

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Microsoft ResearchRedmondUSA
  2. 2.Tel Aviv UniversityTel AvivIsrael

Personalised recommendations