Abstraction-carrying code: a model for mobile code safety

DOI10.1007/s00354-008-0039-7zbMath1169.68356OpenAlexW2024535452MaRDI QIDQ949170

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

Publication date: 20 October 2008

Published in: New Generation Computing (Search for Journal in Brave)

Full work available at URL: http://oa.upm.es/11150/

zbMATH Keywords

static analysislogic programmingabstract interpretationproof-carrying code

Mathematics Subject Classification ID

Logic programming (68N17)

Related Items

An overview of Ciao and its design philosophy, Certificate size reduction in abstraction-carrying code, Kripke semantics for higher-order type theory applied to constraint logic programming languages

Uses Software

• Coq
• SAS
• Ciao
• CiaoPP
• TALx86

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proof-carrying code from certified abstract interpretation and fixpoint compression
• Java bytecode verification: Algorithms and formalizations
• Lightweight bytecode verification
• Abstract interpretation based verification of logic programs
• Compile-time derivation of variable dependency using abstract interpretation
• Efficient run-time type checking of typed logic programs
• Stack-based typed assembly language
• Oracle-based checking of untrusted software
• Programming Languages and Systems
• Reduced Certificates for Abstraction-Carrying Code
• Theorem Proving in Higher Order Logics
• Program Development in Computational Logic
• A practical framework for theabstract interpretation of logic programs