Function extraction

DOI10.1016/J.SCICO.2010.10.001MaRDI QIDQ436372zbMATH OpenOpenAlexFDO

Authors Magnus O. Myreen, Michael J. C. Gordon

Publication date 20 July 2012

Published in Science of Computer Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.scico.2010.10.001

zbMATH Keywords

theorem provingprogram verificationproof automation

Mathematics Subject Classification ID

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1690149
• scientific article; zbMATH DE number 549951
• Towards a Theory of Extractable Functions
• scientific article; zbMATH DE number 2353879
• Theory and Applications of Satisfiability Testing

Cites work

• scientific article; zbMATH DE number 1692950 (Why is no real title available?)
• scientific article; zbMATH DE number 2087445 (Why is no real title available?)
• scientific article; zbMATH DE number 3359806 (Why is no real title available?)
• scientific article; zbMATH DE number 3410595 (Why is no real title available?)
• A Brief Overview of HOL4
• A Formalisation of Smallfoot in HOL
• An axiomatic basis for computer programming
• Automated proofs of object code for a widely used microprocessor
• Avoiding exponential explosion: generating compact verification conditions
• Certified assembly programming with embedded code pointers
• Computer Science Logic
• Efficient weakest preconditions
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Partial functions in ACL2
• Proving Theorems about LISP Functions
• Stack-based typed assembly language
• Theorem Proving in Higher Order Logics
• Transforming programs into recursive functions
• Types, bytes, and separation logic
• Using XCAP to Certify Realistic Systems Code: Machine Context Management
• Verification Condition Generation Via Theorem Proving
• Verification of non-functional programs using interpretations in type theory
• Verified just-in-time compiler on x86

Cited in

(4)

• scientific article; zbMATH DE number 1690149 (Why is no real title available?)
• scientific article; zbMATH DE number 1692950 (Why is no real title available?)
• Semantics-preserving procedure extraction
• Towards a Theory of Extractable Functions

Describes a project that uses

Uses Software

• TALx86
• HOL
• ACL2

This page was built for publication: Function extraction

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