Home
Journals
Archaeology International
Architecture_MPS
Europe and the World: A law review
Film Education Journal
History Education Research Journal
International Journal of Development Education and Global Learning
International Journal of Social Pedagogy
Jewish Historical Studies: A Journal of English-Speaking Jewry
Journal of Bentham Studies
London Review of Education
Radical Americas
Research for All
The Journal of the Sylvia Townsend Warner Society
The London Journal of Canadian Studies
About
About UCL Press
Who we are
Contact us
My ScienceOpen
Sign in
Register
Dashboard
Search
Home
Journals
Archaeology International
Architecture_MPS
Europe and the World: A law review
Film Education Journal
History Education Research Journal
International Journal of Development Education and Global Learning
International Journal of Social Pedagogy
Jewish Historical Studies: A Journal of English-Speaking Jewry
Journal of Bentham Studies
London Review of Education
Radical Americas
Research for All
The Journal of the Sylvia Townsend Warner Society
The London Journal of Canadian Studies
About
About UCL Press
Who we are
Contact us
My ScienceOpen
Sign in
Register
Dashboard
Search
63
views
5
references
Top references
cited by
15
Cite as...
0 reviews
Review
0
comments
Comment
0
recommends
+1
Recommend
0
collections
Add to
0
shares
Share
Twitter
Sina Weibo
Facebook
Email
2,242
similar
All similar
Record
: found
Abstract
: not found
Book Chapter
: not found
Certified Programs and Proofs
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
other
Author(s):
Michael Armand
,
Germain Faure
,
Benjamin Grégoire
,
Chantal Keller
,
Laurent Théry
,
Benjamin Werner
Publication date
(Print):
2011
Publisher:
Springer Berlin Heidelberg
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
BIO Integration
Most cited references
5
Record
: found
Abstract
: not found
Book Chapter
: not found
Fast LCF-Style Proof Reconstruction for Z3
Sascha Böhme
,
Tjark Weber
(2010)
0
comments
Cited
17
times
– based on
0
reviews
Bookmark
Record
: found
Abstract
: not found
Book Chapter
: not found
Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants
Pascal Fontaine
,
Jean-Yves Marion
,
Stephan Merz
…
(2006)
0
comments
Cited
13
times
– based on
0
reviews
Bookmark
Record
: found
Abstract
: not found
Book Chapter
: not found
Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
Frédéric Besson
(2007)
0
comments
Cited
10
times
– based on
0
reviews
Bookmark
All references
Author and book information
Book Chapter
Publication date (Print):
2011
Pages
: 135-150
DOI:
10.1007/978-3-642-25379-9_12
SO-VID:
be059633-9158-4811-955d-b258c5a35ce2
License:
http://www.springer.com/tdm
History
Data availability:
Comments
Comment on this book
Sign in to comment
Book chapters
pp. 183
Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL
pp. 135
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
Similar content
2,242
From Total Assignment Enumeration to Modern SAT Solver
Authors:
Alexander Nadel
,
Nachum Dershowitz
SAT-416 IGSF1 Does Not Regulate FSH Synthesis or Secretion
Authors:
Emilie Brulé
,
Yining Li
,
Gauthier Schang
…
States as Strings as Strategies: Steering Language Models with Game-Theoretic Solvers
Authors:
Ian Gemp
,
Yoram Bachrach
,
Marc Lanctot
…
See all similar
Cited by
14
Verification of a Cryptographic Primitive
Authors:
Andrew Appel
SMT proof checking using a logical framework
Authors:
Aaron Stump
,
Duckki Oe
,
Andrew Reynolds
…
SMT Solvers for Rodin
Authors:
David Déharbe
,
Pascal Fontaine
,
Yoann Guyot
…
See all cited by