Oracle-based checking of untrusted software

DOI10.1145/360204.360216MaRDI QIDQ5178881zbMATH OpenOpenAlexFDO

Authors George C. Necula, Shree P. Rahul

Publication date 17 March 2015

Published in Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/360204.360216

Mathematics Subject Classification ID

Theory of programming languages (68N15) Cryptography (94A60) Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functional programming and lambda calculus (68N18)

Recommendations

• A trustworthy proof checker
• scientific article; zbMATH DE number 2110618
• scientific article; zbMATH DE number 2090287
• scientific article; zbMATH DE number 1962754
• scientific article; zbMATH DE number 1330435

Cited in

(11)

• Abstraction-carrying code: a model for mobile code safety
• A formally verified compiler back-end
• Proof checking and logic programming
• How to get more out of your oracles
• Proof-carrying code from certified abstract interpretation and fixpoint compression
• Type systems equivalent to data-flow analyses for imperative languages
• Every bit counts: the binary representation of typed data and programs
• ANF preserves dependent types up to extensional equality
• SMT proof checking using a logical framework
• A semantic framework for proof evidence
• A trustworthy proof checker

This page was built for publication: Oracle-based checking of untrusted software

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5178881)