Certificate size reduction in abstraction-carrying code

DOI10.1017/S1471068410000487zbMath1247.68042arXiv1010.4533OpenAlexW2111662649MaRDI QIDQ2909518

Puri Arenas, Elvira Albert, Manuel V. Hermenegildo, Germán Puebla

Publication date: 30 August 2012

Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1010.4533

zbMATH Keywords

static analysisproof-carrying codemobile codeabstraction-carrying codereduced certificates

Mathematics Subject Classification ID

Logic programming (68N17) Theory of software (68N99)

Uses Software

• Coq
• CiaoPP

Cites Work

• Unnamed Item
• Unnamed Item
• Abstraction-carrying code: a model for mobile code safety
• Java bytecode verification: Algorithms and formalizations
• Lightweight bytecode verification
• Verified bytecode verifiers.
• Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor)
• Compile-time derivation of variable dependency using abstract interpretation
• A framework for defining logics
• Verification, Model Checking, and Abstract Interpretation
• A practical framework for theabstract interpretation of logic programs

This page was built for publication: Certificate size reduction in abstraction-carrying code