Abstract
Operational models of fragments of the Java Virtual Machine and the .NET Common Language Runtime have been the focus of considerable study in recent years, and of particular interest have been specifications and machine-checked proofs of type soundness. In this paper we aim to increase the level of automation used when checking type soundness for these formalizations. We present a semi-automated technique for reducing a range of type soundness problems to a form that can be automatically checked using a decidable first-order theory. Deciding problems within this fragment is exponential in theory but is often efficient in practice, and the time required for proof checking can be controlled by further hints from the user. We have applied this technique to two case studies, both of which are type soundness properties for subsets of the .NET CLR. These case studies have in turn aided us in our informal analysis of that system.
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.
References
C. Barrett, D. Dill, and J. Levitt. Validity checking for combinations of theories with equality. In M. Srivas and A. Camilleri, editors, Formal Methods In Computer-Aided Design, volume 1166 of Lecture Notes in Computer Science, pages 187–201. Springer-Verlag, November 1996. Palo Alto, California, November 6-8.
C. Barrett, D. Dill, and A. Stump. A generalization of Shostak’s method for combining decision procedures. In Frontiers of Combining Systems (FROCOS), Lecture Notes in Artificial Intelligence. Springer-Verlag, April 2002.
A. Degtyarev and A. Voronkov. Equality reasoning in sequent-based calculi. In Handbook of Automated Reasoning, Volume I, pages 611–706. Elsevier Science and MIT Press, 2001.
A. Gordon and D. Syme. Typing a multi-language intermediate code. In 27th Annual ACM Symposium on Principles of Programming Languages, January 2001.
M.J.C. Gordon and T.F. Melham. Introduction to HOL: A theorem-proving environment for higher-order logic. Cambridge University Press, 1993.
J.G. Henriksen, J. Jensen, M. Jørgensen, N. Klarlund, B. Paige, T. Rauhe, and A. Sandholm. Mona: Monadic second-order logic in practice. In Tools and Algorithms for the Construction and Analysis of Systems, First International Workshop, TACAS’ 95, LNCS 1019, 1995.
Xavier Leroy. The Objective Caml system, documentation and user’s guide. INRIA, Rocquencourt, 1999. Available from http://caml. inria.fr.
Serge Lidin. Inside Microsoft.NET IL Assembler. Microsoft Press, 2002.
Tobias Nipkow, David von Oheimb, and Cornelia Pusch. μ Java: Embedding a programming language in a theorem prover. In F.L. Bauer and R. Steinbrüggen, editors, Foundations of Secure Computation. Proc. Int. Summer School Markto-berdorf 1999, pages 117–144. IOS Press, 2000.
M. Norrish. C formalised in HOL. PhD thesis, University of Cambridge, 1998.
C. Pusch. Proving the soundness of a Java bytecode verifier specification in Is-abelle/HOL. In TACAS’99, Lecture Notes in Computer Science. Springer Verlag, 1999.
Z. Qian. A Formal Specification of Java Virtual Machine Instructions for Objects, Methods and Subroutines. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1532 of Lecture Notes in Computer Science, pages 271–312. SpringerVerlag, 1999.
Robert Stärk, Joachim Schmid, and Egon Börger. Java and the Java Virtual Machine. Springer Verlag, 2001.
R. Stata and M. Abadi. A type system for Java bytecode subroutines. In Proceedings POPL’98, pages 149–160. ACM Press, 1998.
D. Syme. Declarative Theorem Proving for Operational Semantics. PhD thesis, University of Cambridge, 1998.
M. VanInwegen. The Machine-Assisted Proof of Programming Language Properties. PhD thesis, University of Pennsylvania, May 1996.
D. von Oheimb and T. Nipkow. Machine-checking the Java specification: Proving type-safety. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1532 of Lecture Notes in Computer Science, pages 119–156. Springer Verlag, 1999.
Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38–94, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Syme, D., Gordon, A.D. (2002). Automating Type Soundness Proofs via Decision Procedures and Guided Reductions. In: Baaz, M., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2002. Lecture Notes in Computer Science(), vol 2514. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36078-6_28
Download citation
DOI: https://doi.org/10.1007/3-540-36078-6_28
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00010-5
Online ISBN: 978-3-540-36078-0
eBook Packages: Springer Book Archive