Abstract
An ongoing challenge for computer science is the development of a tool which automatically verifies programs meet their specifications, and are free from runtime errors such as divide-by-zero, array out-of-bounds and null dereferences. Several impressive systems have been developed to this end, such as ESC/Java and Spec#, which build on existing programming languages (e.g. Java, C#). However, there remains a need for an open research platform in this area. We have developed the Whiley programming language, and its accompanying verifying compiler, as an open platform for research. Whiley has been designed from the ground up to simplify the verification process. In this paper, we introduce the Whiley language and it accompanying verifying compiler tool.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Hoare, T.: The verifying compiler: A grand challenge for computing research. Journal of the ACM 50(1), 63–69 (2003)
King, S.: A Program Verifier. PhD thesis, Carnegie-Mellon University (1969)
Peter Deutsch, L.: An interactive program verifier. Ph.d. (1973)
Good, D.I.: Mechanical proofs about computer programs. In: Mathematical Logic and Programming Languages, pp. 55–75 (1985)
Luckham, D.C., German, S.M., von Henke, F.W., Karp, R.A., Milne, P.W., Oppen, D.C., Polak, W., Scherlis, W.L.: Stanford pascal verifier user manual. Technical Report CS-TR-79-731, Stanford University, Department of Computer Science (1979)
Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: Extended static checking. SRC Research Report 159, Compaq Systems Research Center (1998)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proc. PLDI, pp. 234–245 (2002)
Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accommodates both runtime assertion checking and formal verification. Science of Computer Programming 55(1-3), 185–208 (2005)
Barnett, M., Leino, K.R.M., Schulte, W.: The spec# programming system: An overview. Technical report, Microsoft Research (2004)
Ireland, A.: A Practical Perspective on the Verifying Compiler Proposal. In: Proceedings of the Grand Challenges in Computing Research Conference (2004)
Leavens, G.T., Abrial, J., Batory, D., Butler, M., Coglio, A., Fisler, K., Hehner, E., Jones, C., Miller, D., Peyton-Jones, S., Sitaraman, M., Smith, D.R., Stump, A.: Roadmap for enhanced languages and methods to aid verification. In: Proc. of GPCE, pp. 221–235 (2006)
Pearce, D., Noble, J.: Implementing a language with flow-sensitive and structural ty** on the JVM. Electronic Notes in Computer Science 279(1), 47–59 (2011)
Pearce, D.J.: Sound and complete flow ty** with unions, intersections and negations. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 335–354. Springer, Heidelberg (2013)
Pearce, D.J.: A calculus for constraint-based flow ty**. In: Proc. FTFJP, page Article 7 (2013)
Rountev, A.: Precise identification of side-effect-free methods in Java. In: Proc. ICSM, pp. 82–91. IEEE Computer Society Press (2004)
Sălcianu, A., Rinard, M.: Purity and side effect analysis for Java programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 199–215. Springer, Heidelberg (2005)
Tobin-Hochstadt, S., Felleisen, M.: Logical types for untyped languages. In: Proc. ICFP, pp. 117–128 (2010)
Guha, A., Saftoiu, C., Krishnamurthi, S.: Ty** local control and state using flow analysis. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 256–275. Springer, Heidelberg (2011)
Barbanera, F., Caglini, M.D.-C.: Intersection and union types. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol. 526, pp. 651–674. Springer, Heidelberg (1991)
Igarashi, A., Nagira, H.: Union types for object-oriented programming. Journal of Object Technology 6(2) (2007)
Mycroft, A.: Programming language design and analysis motivated by hardware evolution. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 18–33. Springer, Heidelberg (2007)
Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.A.: Deciding bit-vector arithmetic with abstraction. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 358–372. Springer, Heidelberg (2007)
Lameed, N., Hendren, L.: Staged static techniques to efficiently implement array copy semantics in a MATLAB JIT compiler. In: Knoop, J. (ed.) CC 2011. LNCS, vol. 6601, pp. 22–41. Springer, Heidelberg (2011)
Nielson, F., Nielson, H.R., Hankin, C.L.: Principles of Program Analysis. Springer (1999)
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)
Detlefs, Nelson, Saxe: Simplify: A theorem prover for program checking. JACMÂ 52 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer International Publishing Switzerland
About this paper
Cite this paper
Pearce, D.J., Groves, L. (2013). Whiley: A Platform for Research in Software Verification. In: Erwig, M., Paige, R.F., Van Wyk, E. (eds) Software Language Engineering. SLE 2013. Lecture Notes in Computer Science, vol 8225. Springer, Cham. https://doi.org/10.1007/978-3-319-02654-1_13
Download citation
DOI: https://doi.org/10.1007/978-3-319-02654-1_13
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-02653-4
Online ISBN: 978-3-319-02654-1
eBook Packages: Computer ScienceComputer Science (R0)