Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
1 | Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero |
A Coq formal proof of the LaxMilgram theorem. |
CPP |
2017 |
DBLP DOI BibTeX RDF |
|
1 | Mitsuharu Yamamoto, Shogo Sekine, Saki Matsumoto |
Formalization of Karp-Miller tree construction on petri nets. |
CPP |
2017 |
DBLP DOI BibTeX RDF |
|
1 | Jesper Cockx, Dominique Devriese |
Lifting proof-relevant unification to higher dimensions. |
CPP |
2017 |
DBLP DOI BibTeX RDF |
|
1 | Reuben N. S. Rowe, James Brotherston |
Automatic cyclic termination proofs for recursive procedures in separation logic. |
CPP |
2017 |
DBLP DOI BibTeX RDF |
|
1 | Steven Schäfer, Sigurd Schneider, Gert Smolka |
Axiomatic semantics for compiler verification. |
CPP |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Tahina Ramananandro, Paul Mountcastle, Benoît Meister, Richard Lethin |
A unified Coq framework for verifying C programs with floating-point computations. |
CPP |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Peter Lammich |
Refinement based verification of imperative data structures. |
CPP |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Floris van Doorn |
Constructing the propositional truncation using non-recursive HITs. |
CPP |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Nathan Fulton, André Platzer |
A logic of proofs for differential dynamic logic: toward independently checkable proof certificates for dynamic logics. |
CPP |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Sandrine Blazy, Alix Trieu |
Formal verification of control-flow graph flattening. |
CPP |
2016 |
DBLP DOI BibTeX RDF |
|
1 | René Thiemann, Akihisa Yamada 0002 |
Formalizing jordan normal forms in Isabelle/HOL. |
CPP |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Michel St-Martin, Amy P. Felty |
A verified algorithm for detecting conflicts in XACML access control rules. |
CPP |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Arthur Charguéraud |
Higher-order representation predicates in separation logic. |
CPP |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, Thomas E. Anderson |
Planning for change in a formal verification of the raft consensus protocol. |
CPP |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Harvey M. Friedman |
Perspectives on formal verification (invited talk). |
CPP |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Cyril Cohen, Boris Djalal |
Formalization of a newton series representation of polynomials. |
CPP |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Evgenii Kotelnikov, Laura Kovács, Giles Reger, Andrei Voronkov |
The vampire and the FOOL. |
CPP |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Lukasz Czajka 0001 |
Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions. |
CPP |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Vincent Rahli, Mark Bickford |
A nominal exploration of intuitionism. |
CPP |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Leonardo Mendonça de Moura |
Dependent type practice (invited talk). |
CPP |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Cezary Kaliszyk, Karol Pak, Josef Urban |
Towards a mizar environment for isabelle: foundations and language. |
CPP |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Johannes Åman Pohjola, Joachim Parrow |
Bisimulation up-to techniques for psi-calculi. |
CPP |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Sophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub |
Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials. |
CPP |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Jeremy Avigad, Adam Chlipala (eds.) |
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016 |
CPP |
2016 |
DBLP BibTeX RDF |
|
1 | Wenda Li, Lawrence C. Paulson |
A modular, efficient formalisation of real algebraic numbers. |
CPP |
2016 |
DBLP DOI BibTeX RDF |
|
1 | Andrea Asperti |
The Speedup Theorem in a Primitive Recursive Framework. |
CPP |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Tahina Ramananandro, Zhong Shao, Shu-Chun Weng, Jérémie Koenig, Yuchen Fu |
A Compositional Semantics for Verified Separate Compilation and Linking. |
CPP |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Steven Schäfer, Gert Smolka, Tobias Tebbi |
Completeness and Decidability of de Bruijn Substitution Algebra in Coq. |
CPP |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Yves Bertot |
Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations. |
CPP |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Ondrej Kuncar |
Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading in Proof Assistants. |
CPP |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Martin Bodin, Thomas P. Jensen, Alan Schmitt |
Certified Abstract Interpretation with Pretty-Big-Step Semantics. |
CPP |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Zhong Shao |
Clean-Slate Development of Certified OS Kernels. |
CPP |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Xiao Jia 0001, Wei Li, Viktor Vafeiadis |
Proving Lock-Freedom Easily and Automatically. |
CPP |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Manuel Eberl |
A Decision Procedure for Univariate Real Polynomials in Isabelle/HOL. |
CPP |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Kaustuv Chaudhuri, Matteo Cimini, Dale Miller 0001 |
A Lightweight Formalization of the Metatheory of Bisimulation-Up-To. |
CPP |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Denis Firsov, Tarmo Uustalu |
Certified Normalization of Context-Free Grammars. |
CPP |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Sandrine Blazy, André Maroneze, David Pichardie |
Verified Validation of Program Slicing. |
CPP |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Fabian Immler |
A Verified Algorithm for Geometric Zonotope/Hyperplane Intersection. |
CPP |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Xavier Leroy, Alwen Tiu (eds.) |
Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015 |
CPP |
2015 |
DBLP BibTeX RDF |
|
1 | Robbert Krebbers, Freek Wiedijk |
A Typed C11 Semantics for Interactive Theorem Proving. |
CPP |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Sternagel, Sarah Winkler, Harald Zankl |
Recording Completion for Certificates in Equational Reasoning. |
CPP |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Jingyuan Cao, Ming Fu, Xinyu Feng 0001 |
Practical Tactics for Verifying C Programs in Coq. |
CPP |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Viktor Vafeiadis |
Formal Reasoning about the C11 Weak Memory Model. |
CPP |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Cezary Kaliszyk, Josef Urban, Jirí Vyskocil |
Certified Connection Tableaux Proofs for HOL Light and TPTP. |
CPP |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Peter Lammich, René Neumann |
A Framework for Verifying Depth-First Search Algorithms. |
CPP |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Thibault Gauthier, Cezary Kaliszyk |
Premise Selection and External Provers for HOL4. |
CPP |
2015 |
DBLP DOI BibTeX RDF |
|
1 | Brian Huffman, Ondrej Kuncar |
Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL. |
CPP |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Robbert Krebbers |
Aliasing Restrictions of C11 Formalized in Coq. |
CPP |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Andrea Asperti |
A Formal Proof of Borodin-Trakhtenbrot's Gap Theorem. |
CPP |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Daniel Huang 0001, Greg Morrisett |
Formalizing the SAFECode Type System. |
CPP |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Denis Firsov, Tarmo Uustalu |
Certified Parsing of Regular Languages. |
CPP |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Olivier Savary Bélanger, Stefan Monnier, Brigitte Pientka |
Programming Type-Safe Transformations Using Higher-Order Abstract Syntax. |
CPP |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Cyril Cohen, Maxime Dénès, Anders Mörtberg |
Refinements for Free! |
CPP |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Christian Sternagel |
Certified Kruskal's Tree Theorem. |
CPP |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Georges Gonthier, Michael Norrish (eds.) |
Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings |
CPP |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Christian Doczkal, Jan-Oliver Kaiser, Gert Smolka |
A Constructive Theory of Regular Languages in Coq. |
CPP |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Christian J. Bell |
Certifiably Sound Parallelizing Transformations. |
CPP |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Daniel R. Licata, Guillaume Brunerie |
π n (S n ) in Homotopy Type Theory. |
CPP |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Dale Miller 0001, Alwen Tiu |
Extracting Proofs from Tabled Proof Search. |
CPP |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Andrei Popescu 0001, Johannes Hölzl, Tobias Nipkow |
Formalizing Probabilistic Noninterference. |
CPP |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Magnus O. Myreen, Gregorio Curello |
Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code. |
CPP |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Gordon Stewart 0001 |
Computational Verification of Network Programs in Coq. |
CPP |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Narges Khakpour, Oliver Schwarz, Mads Dam |
Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties. |
CPP |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Chunhan Wu, Xingyuan Zhang, Christian Urban |
A Formal Model and Correctness Proof for an Access Control Policy Framework. |
CPP |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Josiah Dodds, Andrew W. Appel |
Mostly Sound Type System Improves a Foundational Program Verifier. |
CPP |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Andreas Schropp, Andrei Popescu 0001 |
Nonfree Datatypes in Isabelle/HOL - Animating a Many-Sorted Metatheory. |
CPP |
2013 |
DBLP DOI BibTeX RDF |
|
1 | Andrei Popescu 0001, Johannes Hölzl, Tobias Nipkow |
Proving Concurrent Noninterference. |
CPP |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Christian Doczkal, Gert Smolka |
Constructive Completeness for Modal Logic with Transitive Closure. |
CPP |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Naoki Kobayashi 0001 |
Program Certification by Higher-Order Model Checking. |
CPP |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Pierre Neron |
A Formal Proof of Square Root and Division Elimination in Embedded Programs. |
CPP |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Lukas Bulwahn |
The New Quickcheck for Isabelle - Random, Exhaustive and Symbolic Testing under One Roof. |
CPP |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Alexander Vaynberg, Zhong Shao |
Compositional Verification of a Baby Virtual Memory Manager. |
CPP |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Dominic P. Mulligan, Claudio Sacerdoti Coen |
On the Correctness of an Optimising Assembler for the Intel MCS-51 Microprocessor. |
CPP |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Xavier Leroy |
Mechanized Semantics for Compiler Verification. |
CPP |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Sylvie Boldo, Catherine Lelay, Guillaume Melquiond |
Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives. |
CPP |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Jianzhou Zhao, Steve Zdancewic |
Mechanized Verification of Computing Dominators for Formalizing Compilers. |
CPP |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Gerwin Klein |
Noninterference for Operating System Kernels. |
CPP |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Greg Morrisett |
Scalable Formal Machine Models. |
CPP |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Thierry Coquand, Anders Mörtberg, Vincent Siles |
Coherent and Strongly Discrete Rings in Type Theory. |
CPP |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Kaustuv Chaudhuri |
Compact Proof Certificates for Linear Logic. |
CPP |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Hing-Lun Chan, Michael Norrish |
A String of Pearls: Proofs of Fermat's Little Theorem. |
CPP |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Keisuke Nakano 0001 |
Shall We Juggle, Coinductively? |
CPP |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Gilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella Béguelin |
Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs. |
CPP |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Brian Campbell 0001 |
An Executable Semantics for CompCert C. |
CPP |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Andrea Asperti, Wilmer Ricciotti |
Rating Disambiguation Errors. |
CPP |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Chris Hawblitzel, Dale Miller 0001 (eds.) |
Certified Programs and Proofs - Second International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings |
CPP |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Pierre-Nicolas Tollitte, David Delahaye, Catherine Dubois |
Producing Certified Functional Code from Inductive Specifications. |
CPP |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Valentin Robert, Xavier Leroy |
A Formally-Verified Alias Analysis. |
CPP |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Beniamino Accattoli |
Proof Pearl: Abella Formalization of λ-Calculus Cube Property. |
CPP |
2012 |
DBLP DOI BibTeX RDF |
|
1 | Jean-Pierre Jouannaud, Zhong Shao (eds.) |
Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Tom Ridge |
Simple, Functional, Sound and Complete Parsing for All Context-Free Grammars. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
1 | James Cheney, Christian Urban |
Mechanizing the Metatheory of mini-XQuery. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Mathieu Boespflug, Maxime Dénès, Benjamin Grégoire |
Full Reduction at Full Throttle. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Sorin Stratulat, Vincent Demange |
Automated Certification of Implicit Induction Proofs. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Thierry Coquand, Vincent Siles |
A Decision Procedure for Regular Expression Equivalence in Type Theory. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Michael Backes 0001, Catalin Hritcu, Thorsten Tarrach |
Automatically Verifying Typing Constraints for a Data Processing Language. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Xiaomu Shi, Jean-François Monin, Frédéric Tuong, Frédéric Blanqui |
First Steps towards the Certification of an ARM Simulator Using Compcert. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Martin Henz, Aquinas Hobor |
Teaching Experience: Logic and Formal Methods with Coq. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Andrew W. Appel |
VeriSmall: Verified Smallfoot Shape Analysis. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|
1 | Christian Doczkal, Gert Smolka |
Constructive Formalization of Hybrid Logic with Eventualities. |
CPP |
2011 |
DBLP DOI BibTeX RDF |
|