Bytecode Analysis for Proof Carrying Code | Zendy

Martin Wildmoser | Zendy; Amine Chaieb | Zendy; Tobias Nipkow | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Bytecode Analysis for Proof Carrying Code

Author(s) -

Martin Wildmoser,

Amine Chaieb,

Tobias Nipkow

Publication year - 2005

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2005.02.040

Subject(s) - bytecode , computer science , hol , programming language , construct (python library) , code (set theory) , java bytecode , proof assistant , model checking , generator (circuit theory) , static analysis , theoretical computer science , java , mathematics , mathematical proof , power (physics) , physics , geometry , set (abstract data type) , java applet , quantum mechanics , java annotation

Out of annotated programs proof carrying code systems construct and prove verification conditions that guarantee a given safety policy. The annotations may come from various program analyzers and must not be trusted as they need to be verified. A generic verification condition generator can be utilized such that a combination of annotations is verified incrementally. New annotations may be verified by using previously verified ones as trusted facts. We show how results from a trusted type analyzer may be combined with untrusted interval analysis to automatically verify that bytecode programs do not overflow. All trusted components are formalized and verified in Isabelle/HOL

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research