Advertisement

Developing Verified Software Using Leon

  • Viktor KuncakEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9058)

Abstract

We present Leon, a system for developing functional Scala programs annotated with contracts. Contracts in Leon can themselves refer to recursively defined functions. Leon aims to find counterexamples when functions do not meet the specifications, and proofs when they do. Moreover, it can optimize run-time checks by eliminating statically checked parts of contracts and doing memoization. For verification Leon uses an incremental function unfolding algorithm (which could be viewed as k-induction) and SMT solvers. For counterexample finding it uses these techniques and additionally specification-based test generation. Leon can also execute specifications (e.g. functions given only by postconditions), by invoking a constraint solver at run time. To make this process more efficient and predictable, Leon supports deductive synthesis of functions from specifications, both interactively and in an automated mode. Synthesis in Leon is currently based on a custom deductive synthesis framework incorporating, for example, syntax-driven rules, rules supporting synthesis procedures, and a form of counterexample-guided synthesis. We have also developed resource bound invariant inference for Leon and used it to check abstract worst-case execution time. We have also explored within Leon a compilation technique that transforms real-valued program specifications into finite-precision code while enforcing the desired end-to-end error bounds. Recent work enables Leon to perform program repair when the program does not meet the specification, using error localization, synthesis guided by the original expression, and counterexample-guided synthesis of expressions similar to a given one. Leon is open source and can also be tried from its web environment at leon.epfl.ch.

Keywords

Constraint Solver Incremental Function Program Repair Algebraic Data Type Functional Synthesis 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Blanc, R.W., Kneuss, E., Kuncak, V., Suter, P.: An overview of the leon verification system: verification by translation to recursive functions. In: Scala Workshop (2013)Google Scholar
  2. 2.
    Darulova, E.: Programming with Numerical Uncertainties. PhD thesis, EPFL (2014)Google Scholar
  3. 3.
    Darulova, E., Kuncak, V.: Sound compilation of reals. In: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL) (2014)Google Scholar
  4. 4.
    de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008) CrossRefGoogle Scholar
  5. 5.
    de Moura, L., Bjørner, N.: Generalized, efficient array decision procedures. In: Formal Methods in Computer-Aided Design, November 2009Google Scholar
  6. 6.
    Hindley, R.: The principal type-scheme of an object in combinatory logic. Transactions of the American Mathematical Society 146, 29–60 (1969)zbMATHMathSciNetGoogle Scholar
  7. 7.
    Jacobs, S., Kuncak, V., Suter, P.: Reductions for synthesis procedures. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 88–107. Springer, Heidelberg (2013) CrossRefGoogle Scholar
  8. 8.
    Kaufmann, M., Moore, J.S., Manolios, P.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Norwell (2000) Google Scholar
  9. 9.
    Kneuss, E., Koukoutos, M., Kuncak, V.: On deductive program repair in Leon. Technical Report EPFL-REPORT-205054, EPFL, February 2014Google Scholar
  10. 10.
    Kneuss, E., Kuncak, V., Kuraj, I., Suter, P.: Synthesis modulo recursive functions. In: OOPSLA (2013)Google Scholar
  11. 11.
    Köksal, A., Kuncak, V., Suter, P.: Constraints as control. In: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL) (2012)Google Scholar
  12. 12.
    Koukoutos, E., Kuncak, V.: Checking data structure properties orders of magnitude faster. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 263–268. Springer, Heidelberg (2014) CrossRefGoogle Scholar
  13. 13.
    Kuncak, V., Kneuss, E., Suter, P.: Executing specifications using synthesis and constraint solving. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 1–20. Springer, Heidelberg (2013) CrossRefGoogle Scholar
  14. 14.
    Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. In: ACM SIGPLAN Conf., Programming Language Design and Implementation (PLDI) (2010)Google Scholar
  15. 15.
    Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Software synthesis procedures. Communications of the ACM (2012)Google Scholar
  16. 16.
    Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Functional synthesis for linear arithmetic and sets. Software Tools for Technology Transfer (STTT) 15(5–6), 455–474 (2013)CrossRefGoogle Scholar
  17. 17.
    Kuraj, I., Kuncak, V.: SciFe: scala framework for effcient enumeration of data structures with invariants. In: Scala Workshop (2014)Google Scholar
  18. 18.
    Madhavan, R., Kuncak, V.: Symbolic resource bound inference for functional programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 762–778. Springer, Heidelberg (2014) CrossRefGoogle Scholar
  19. 19.
    Milner, R.: A theory of type polymorphism in programming. JCSS 17(3), 348–375 (1978)zbMATHMathSciNetGoogle Scholar
  20. 20.
    Odersky, M.: Contracts for scala. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 51–57. Springer, Heidelberg (2010) CrossRefGoogle Scholar
  21. 21.
    Odersky, M., Spoon, L., Venners, B.: Programming in scala: a comprehensive step-by-step guide. Artima Press (2008)Google Scholar
  22. 22.
    Reynolds, A., Kuncak, V.: Induction for SMT solvers. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 80–98. Springer, Heidelberg (2015) CrossRefGoogle Scholar
  23. 23.
    Reynolds, A., Tinelli, C., de Moura, L.M.: Finding conflicting instances of quantified formulas in SMT. In: FMCAD, pp. 195–202. IEEE (2014)Google Scholar
  24. 24.
    Suter, P.: Programming with Specifications. PhD thesis, EPFL, December 2012Google Scholar
  25. 25.
    Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. In: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL) (2010)Google Scholar
  26. 26.
    Suter, P., Köksal, A.S., Kuncak, V.: Satisfiability modulo recursive programs. In: Yahav, E. (ed.) Static Analysis. LNCS, vol. 6887, pp. 298–315. Springer, Heidelberg (2011) CrossRefGoogle Scholar
  27. 27.
    Vazou, N., Rondon, P.M., Jhala, R.: Abstract refinement types. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 209–228. Springer, Heidelberg (2013) CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.École Polytechnique Fédérale de Lausanne (EPFL)LausanneSwitzerland

Personalised recommendations