Browse
Publications
Preprints
About
About UCL Open: Env.
Aims and Scope
Editorial Board
Indexing
APCs
How to cite
Publishing policies
Editorial policy
Peer review policy
Equality, Diversity & Inclusion
About UCL Press
Contact us
For authors
Information for authors
How it works
Benefits of publishing with us
Submit
How to submit
Preparing your manuscript
Article types
Open Data
ORCID
APCs
Contributor agreement
For reviewers
Information for reviewers
Review process
How to peer review
Peer review policy
My ScienceOpen
Sign in
Register
Dashboard
Search
Browse
Publications
Preprints
About
About UCL Open: Env.
Aims and Scope
Editorial Board
Indexing
APCs
How to cite
Publishing policies
Editorial policy
Peer review policy
Equality, Diversity & Inclusion
About UCL Press
Contact us
For authors
Information for authors
How it works
Benefits of publishing with us
Submit
How to submit
Preparing your manuscript
Article types
Open Data
ORCID
APCs
Contributor agreement
For reviewers
Information for reviewers
Review process
How to peer review
Peer review policy
My ScienceOpen
Sign in
Register
Dashboard
Search
34
views
16
references
Top references
cited by
1
Cite as...
0 reviews
Review
0
comments
Comment
0
recommends
+1
Recommend
0
collections
Add to
0
shares
Share
Twitter
Sina Weibo
Facebook
Email
3,353
similar
All similar
Record
: found
Abstract
: not found
Book Chapter
: not found
Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB
other
Author(s):
Ramana Kumar
,
Eric Mullen
,
Zachary Tatlock
,
Magnus O. Myreen
Publication date
(Online):
July 04 2018
Publisher:
Springer International Publishing
Read this book at
Publisher
Buy book
Review
Review book
Invite someone to review
Bookmark
Cite as...
There is no author summary for this book yet. Authors can add summaries to their books on ScienceOpen to make them more accessible to a non-specialist audience.
Related collections
Genomic Prediction: Software
Most cited references
16
Record
: found
Abstract
: not found
Book Chapter
: not found
A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture
Anthony Fox
,
Magnus O. Myreen
(2010)
0
comments
Cited
18
times
– based on
0
reviews
Bookmark
Record
: found
Abstract
: not found
Book Chapter
: not found
Extraction in Coq: An Overview
Pierre Letouzey
(2008)
0
comments
Cited
13
times
– based on
0
reviews
Bookmark
Record
: found
Abstract
: not found
Book Chapter
: not found
Executing Higher Order Logic
Stefan Berghofer
,
Tobias Nipkow
(2002)
0
comments
Cited
13
times
– based on
0
reviews
Bookmark
All references
Author and book information
Book Chapter
Publication date (Print):
2018
Publication date (Online):
July 04 2018
Pages
: 362-369
DOI:
10.1007/978-3-319-94821-8_21
SO-VID:
df3e1060-f33f-47fa-8e0d-dd4d670ee376
History
Data availability:
Comments
Comment on this book
Sign in to comment
Book chapters
pp. E1
Erratum to: Interactive Theorem Proving
pp. 1
Physical Addressing on Real Hardware in Isabelle/HOL
pp. 20
Towards Certified Meta-Programming with Typed Template-Coq
pp. 40
Formalizing Ring Theory in PVS
pp. 48
Software Tool Support for Modular Reasoning in Modal Logics of Actions
pp. 68
Backwards and Forwards with Separation Logic
pp. 88
A Coq Formalisation of SQL’s Execution Engines
pp. 108
A Coq Tactic for Equality Learning in Linear Arithmetic
pp. 126
The Coinductive Formulation of Common Knowledge
pp. 142
Tactics and Certificates in Meta Dedukti
pp. 160
A Formalization of the LLL Basis Reduction Algorithm
pp. 178
A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs
pp. 196
Verified Analysis of Random Binary Tree Structures
pp. 215
HOL Light QE
pp. 235
Efficient Mendler-Style Lambda-Encodings in Cedille
pp. 253
Verification of PCP-Related Computational Reductions in Coq
pp. 270
ProofWatch: Watchlist Guidance for Large Theories in E
pp. 289
Reification by Parametricity
pp. 306
Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata
pp. 324
CalcCheck: A Proof Checker for Teaching the “Logical Approach to Discrete Math”
pp. 342
Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY
pp. 362
Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB
pp. 370
Proof Pearl: Constructive Extraction of Cycle Finding Algorithms
pp. 388
Fast Machine Words in Isabelle/HOL
pp. 411
Relational Parametricity and Quotient Preservation for Modular (Co)datatypes
pp. 432
Towards Verified Handwritten Calculational Proofs
pp. 441
A Formally Verified Solver for Homogeneous Linear Diophantine Equations
pp. 459
Formalizing Implicative Algebras in Coq
pp. 477
Boosting the Reuse of Formal Specifications
pp. 495
Towards Formal Foundations for Game Theory
pp. 504
Verified Timing Transformations in Synchronous Circuits with $$\lambda \pi $$ -Ware
pp. 523
A Formal Equational Theory for Call-By-Push-Value
pp. 542
Program Verification in the Presence of Cached Address Translation
pp. 560
Verified Tail Bounds for Randomized Programs
pp. 579
Verified Memoization and Dynamic Programming
pp. 597
MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper)
pp. 604
Formalization of a Polymorphic Subtyping Algorithm
pp. 623
An Agda Formalization of Üresin & Dubois’ Asynchronous Fixed-Point Theory
Similar content
3,353
Indications, Diagnostic Yield and Complications of Endoscopic Ultrasound Guided Trucut Biopsy (EUS-TCB): Prospective Study in 77 Consecutive Patients At a Tertiary Hospital with On-Site Cytology Support
Authors:
John C Dewitt
,
Mohammad Al-Haddad
,
Lee McHenry
…
New predicted ground state and high pressure phases of TcB 3 and TcB 4 : First-principles
Authors:
Qingyu Hou
,
Erjun Zhao
,
Chun Mei Ying
…
Molecular dynamics simulations of adsorption of hydrophobic 1,2,4-trichlorobenzene (TCB) on hydrophilic TiO2 in surfactant emulsions and experimental process efficiencies of photo-degradation and -dechlorination
Authors:
Satoshi Horikoshi
,
Daiki Minami
,
Seya Ito
…
See all similar
Cited by
1
Metamath Zero: Designing a Theorem Prover Prover
Authors:
Mario Carneiro
See all cited by