|
|
|
|
Venues (Conferences, Journals, ...)
|
|
|
GrowBag graphs for keyword ? (Num. hits/coverage)
Group by:
No Growbag Graphs found.
|
|
|
|
|
Results
Found 318 publication records. Showing 318 according to the selection in the facets
| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Thomas Braibant |
Coquet: A Coq Library for Verifying Hardware.  |
CPP  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Nikolaj S. Bjørner |
Engineering Theories with Z3. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas Braibant, Damien Pous |
Tactics for Reasoning Modulo AC in Coq. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, Benjamin Werner |
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Frank Pfenning, Luís Caires, Bernardo Toninho |
Proof-Carrying Code in a Session-Typed Process Calculus. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Sascha Böhme, Anthony C. J. Fox, Thomas Sewell, Tjark Weber |
Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Cezary Kaliszyk, Henk Barendregt |
Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Jinjiang Lei, Zongyan Qiu |
Verification of Scalable Synchronous Queue. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Vladimir Voevodsky |
Univalent Semantics of Constructive Type Theories. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Pierre Corbineau, Mathilde Duclos, Yassine Lakhnech |
Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Dale Miller 0001 |
A Proposal for Broad Spectrum Proof Certificates. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter W. O'Hearn |
Algebra, Logic, Locality, Concurrency. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie |
Modular SMT Proofs for Fast Reflexive Checking Inside Coq. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Jieung Kim, Sukyoung Ryu |
Coq Mechanization of Featherweight Fortress with Multiple Dispatch and Multiple Inheritance. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Thi Minh Tuyen Nguyen, Claude Marché |
Hardware-Dependent Proofs of Numerical Programs. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Dongchen Jiang, Tobias Nipkow |
Proof Pearl: The Marriage Theorem. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Wolfram Kahl |
The Teaching Tool CalcCheck A Proof-Checker for Gries and Schneider's "Logical Approach to Discrete Math". |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Jean-David Génevaux, Julien Narboux, Pascal Schreck |
Formalization of Wu's Simple Method in Coq. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
Displaying result #301 - #318 of 318 (100 per page; Change: ) Pages: [ <<][ 1][ 2][ 3][ 4] |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license