Advertisement

Combining a Verification Condition Generator for a Bytecode Language with Static Analyses

  • Benjamin Grégoire
  • Jorge Luis Sacchini
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4912)

Abstract

In Proof-Carrying Code, the verification condition generator (VCgen) generates a set of formulas whose validity implies that the code satisfies the consumer policy. Applying a VCgen to a bytecode language with exceptions (such as Java bytecode) can result in a large number of proof obligations, due to the amount of branching instructions. We present a VCgen for Java bytecode that uses static analyses to reduce the number of proof obligations. As a result, the task of producing a proof is simpler, and the subsequent proof terms smaller. We formalize the VCgen as a deep embedding in Coq and prove soundness with respect to the Bicolano formalization of the Java bytecode semantics.

Keywords

Operational Semantic Correctness Relation Proof Obligation Exception Handler Java Virtual Machine 
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.
    Albert, E., Arenas-Sánchez, P., Puebla, G., Hermenegildo, M.V.: Reduced certificates for abstraction-carrying code. In: Etalle, S., Truszczyński, M. (eds.) ICLP 2006. LNCS, vol. 4079, pp. 163–178. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  2. 2.
    Albert, E., Puebla, G., Hermenegildo, M.V.: Abstraction-carrying code. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 380–397. Springer, Heidelberg (2005)Google Scholar
  3. 3.
    Besson, F., Jensen, T.P., Pichardie, D.: Proof-carrying code from certified abstract interpretation and fixpoint compression. Theor. Comput. Sci. 364(3), 273–291 (2006)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Besson, F., Jensen, T.P., Turpin, T.: Small witnesses for abstract interpretation-based proofs. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 268–283. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  5. 5.
    Chaieb, A.: Proof-producing program analysis. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 287–301. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  6. 6.
    Chalin, P., James, P.: Non-null references by default in java: Alleviating the nullity annotation burden. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609, Springer, Heidelberg (2007)CrossRefGoogle Scholar
  7. 7.
    Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269–282 (1979)Google Scholar
  8. 8.
    Necula, G.C.: Proof-carrying code. In: POPL, pp. 106–119 (1997)Google Scholar
  9. 9.
    Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer-Verlag New York, Inc., Secaucus, NJ, USA (1999)zbMATHGoogle Scholar
  10. 10.
    Pichardie, D.: Bicolano – Byte Code Language in Coq (2006), http://mobius.inia.fr/bicolano
  11. 11.
    Seo, S., Yang, H., Yi, K.: Automatic construction of hoare proofs from abstract interpretation results. In: Ohori, A. (ed.) APLAS 2003. LNCS, vol. 2895, pp. 230–245. Springer, Heidelberg (2003)Google Scholar
  12. 12.
    Wildmoser, M., Chaieb, A., Nipkow, T.: Bytecode analysis for proof carrying code. Electr. Notes Theor. Comput. Sci. 141(1), 19–34 (2005)CrossRefGoogle Scholar
  13. 13.
    Wildmoser, M., Nipkow, T.: Certifying machine code safety: Shallow versus deep embedding. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 305–320. Springer, Heidelberg (2004)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Benjamin Grégoire
    • 1
  • Jorge Luis Sacchini
    • 1
    • 2
  1. 1.INRIA Sophia AntipolisMéditerranéeFrance
  2. 2.FCEIAUnivesidad Nacional de RosarioArgentina

Personalised recommendations