Oracle-based checking of untrusted software

DOI10.1145/360204.360216zbMath1323.68222OpenAlexW2114925693MaRDI QIDQ5178881

Shree P. Rahul, George C. Necula

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

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

Related Items (9)

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

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