Search results for "CPP"

Hits ?▲	Authors	Title	Venue	Year	Link
44	Johannes Hölzl	Markov processes in Isabelle/HOL.	CPP	2017	DBLP DOI BibTeX RDF
44	Xinyu Feng 0001	Mechanized verification of preemptive OS kernels (invited talk).	CPP	2017	DBLP DOI BibTeX RDF
44	Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada 0002	A formalization of the Berlekamp-Zassenhaus factorization algorithm.	CPP	2017	DBLP DOI BibTeX RDF
44	Lawrence C. Paulson	Porting the HOL light analysis library: some lessons (invited talk).	CPP	2017	DBLP DOI BibTeX RDF
44	Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah, Joseph Tuong	Complx: a verification framework for concurrent imperative programs.	CPP	2017	DBLP DOI BibTeX RDF
44	William Mansky, Yuanfeng Peng, Steve Zdancewic, Joseph Devietti	Verifying dynamic race detection.	CPP	2017	DBLP DOI BibTeX RDF
44	Reynald Affeldt, Cyril Cohen	Formal foundations of 3D geometry to model robot manipulators.	CPP	2017	DBLP DOI BibTeX RDF
44	Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters	The HoTT library: a formalization of homotopy type theory in Coq.	CPP	2017	DBLP DOI BibTeX RDF
44	Érik Martin-Dorel, Pierre Roux	A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations.	CPP	2017	DBLP DOI BibTeX RDF
44	François Pottier	Verifying a hash table and its iterators in higher-order separation logic.	CPP	2017	DBLP DOI BibTeX RDF
44	Gaëtan Gilbert	Formalising real numbers in homotopy type theory.	CPP	2017	DBLP DOI BibTeX RDF
44	Jonas Kaiser, Tobias Tebbi, Gert Smolka	Equivalence of system f and ź2 in Coq based on context morphism lemmas.	CPP	2017	DBLP DOI BibTeX RDF
44	Simon Boulier, Pierre-Marie Pédrot, Nicolas Tabareau	The next 700 syntactical models of type theory.	CPP	2017	DBLP DOI BibTeX RDF
44	Jan Jakubuv, Josef Urban	BliStrTune: hierarchical invention of theorem proving strategies.	CPP	2017	DBLP DOI BibTeX RDF
44	Guillaume Allais, James Chapman 0001, Conor McBride, James McKinna	Type-and-scope safe programs and their proofs.	CPP	2017	DBLP DOI BibTeX RDF
44	Anthony C. J. Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar	Verified compilation of CakeML to multiple machine-code targets.	CPP	2017	DBLP DOI BibTeX RDF
44	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
44	Mitsuharu Yamamoto, Shogo Sekine, Saki Matsumoto	Formalization of Karp-Miller tree construction on petri nets.	CPP	2017	DBLP DOI BibTeX RDF
44	Jesper Cockx, Dominique Devriese	Lifting proof-relevant unification to higher dimensions.	CPP	2017	DBLP DOI BibTeX RDF
44	Reuben N. S. Rowe, James Brotherston	Automatic cyclic termination proofs for recursive procedures in separation logic.	CPP	2017	DBLP DOI BibTeX RDF
44	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
44	Andrea Asperti	The Speedup Theorem in a Primitive Recursive Framework.	CPP	2015	DBLP DOI BibTeX RDF
44	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
44	Steven Schäfer, Gert Smolka, Tobias Tebbi	Completeness and Decidability of de Bruijn Substitution Algebra in Coq.	CPP	2015	DBLP DOI BibTeX RDF
44	Yves Bertot	Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations.	CPP	2015	DBLP DOI BibTeX RDF
44	Ondrej Kuncar	Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading in Proof Assistants.	CPP	2015	DBLP DOI BibTeX RDF
44	Martin Bodin, Thomas P. Jensen, Alan Schmitt	Certified Abstract Interpretation with Pretty-Big-Step Semantics.	CPP	2015	DBLP DOI BibTeX RDF
44	Zhong Shao	Clean-Slate Development of Certified OS Kernels.	CPP	2015	DBLP DOI BibTeX RDF
44	Xiao Jia 0001, Wei Li, Viktor Vafeiadis	Proving Lock-Freedom Easily and Automatically.	CPP	2015	DBLP DOI BibTeX RDF
44	Manuel Eberl	A Decision Procedure for Univariate Real Polynomials in Isabelle/HOL.	CPP	2015	DBLP DOI BibTeX RDF
44	Kaustuv Chaudhuri, Matteo Cimini, Dale Miller 0001	A Lightweight Formalization of the Metatheory of Bisimulation-Up-To.	CPP	2015	DBLP DOI BibTeX RDF
44	Denis Firsov, Tarmo Uustalu	Certified Normalization of Context-Free Grammars.	CPP	2015	DBLP DOI BibTeX RDF
44	Sandrine Blazy, André Maroneze, David Pichardie	Verified Validation of Program Slicing.	CPP	2015	DBLP DOI BibTeX RDF
44	Fabian Immler	A Verified Algorithm for Geometric Zonotope/Hyperplane Intersection.	CPP	2015	DBLP DOI BibTeX RDF
44	Robbert Krebbers, Freek Wiedijk	A Typed C11 Semantics for Interactive Theorem Proving.	CPP	2015	DBLP DOI BibTeX RDF
44	Thomas Sternagel, Sarah Winkler, Harald Zankl	Recording Completion for Certificates in Equational Reasoning.	CPP	2015	DBLP DOI BibTeX RDF
44	Jingyuan Cao, Ming Fu, Xinyu Feng 0001	Practical Tactics for Verifying C Programs in Coq.	CPP	2015	DBLP DOI BibTeX RDF
44	Viktor Vafeiadis	Formal Reasoning about the C11 Weak Memory Model.	CPP	2015	DBLP DOI BibTeX RDF
44	Cezary Kaliszyk, Josef Urban, Jirí Vyskocil	Certified Connection Tableaux Proofs for HOL Light and TPTP.	CPP	2015	DBLP DOI BibTeX RDF
44	Peter Lammich, René Neumann	A Framework for Verifying Depth-First Search Algorithms.	CPP	2015	DBLP DOI BibTeX RDF
44	Thibault Gauthier, Cezary Kaliszyk	Premise Selection and External Provers for HOL4.	CPP	2015	DBLP DOI BibTeX RDF
44	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
44	Brian Huffman, Ondrej Kuncar	Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL.	CPP	2013	DBLP DOI BibTeX RDF
44	Robbert Krebbers	Aliasing Restrictions of C11 Formalized in Coq.	CPP	2013	DBLP DOI BibTeX RDF
44	Andrea Asperti	A Formal Proof of Borodin-Trakhtenbrot's Gap Theorem.	CPP	2013	DBLP DOI BibTeX RDF
44	Daniel Huang 0001, Greg Morrisett	Formalizing the SAFECode Type System.	CPP	2013	DBLP DOI BibTeX RDF
44	Denis Firsov, Tarmo Uustalu	Certified Parsing of Regular Languages.	CPP	2013	DBLP DOI BibTeX RDF
44	Olivier Savary Bélanger, Stefan Monnier, Brigitte Pientka	Programming Type-Safe Transformations Using Higher-Order Abstract Syntax.	CPP	2013	DBLP DOI BibTeX RDF
44	Cyril Cohen, Maxime Dénès, Anders Mörtberg	Refinements for Free!	CPP	2013	DBLP DOI BibTeX RDF
44	Christian Sternagel	Certified Kruskal's Tree Theorem.	CPP	2013	DBLP DOI BibTeX RDF
44	Christian Doczkal, Jan-Oliver Kaiser, Gert Smolka	A Constructive Theory of Regular Languages in Coq.	CPP	2013	DBLP DOI BibTeX RDF
44	Christian J. Bell	Certifiably Sound Parallelizing Transformations.	CPP	2013	DBLP DOI BibTeX RDF
44	Daniel R. Licata, Guillaume Brunerie	π n (S n ) in Homotopy Type Theory.	CPP	2013	DBLP DOI BibTeX RDF
44	Dale Miller 0001, Alwen Tiu	Extracting Proofs from Tabled Proof Search.	CPP	2013	DBLP DOI BibTeX RDF
44	Andrei Popescu 0001, Johannes Hölzl, Tobias Nipkow	Formalizing Probabilistic Noninterference.	CPP	2013	DBLP DOI BibTeX RDF
44	Magnus O. Myreen, Gregorio Curello	Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code.	CPP	2013	DBLP DOI BibTeX RDF
44	Gordon Stewart 0001	Computational Verification of Network Programs in Coq.	CPP	2013	DBLP DOI BibTeX RDF
44	Narges Khakpour, Oliver Schwarz, Mads Dam	Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties.	CPP	2013	DBLP DOI BibTeX RDF
44	Chunhan Wu, Xingyuan Zhang, Christian Urban	A Formal Model and Correctness Proof for an Access Control Policy Framework.	CPP	2013	DBLP DOI BibTeX RDF
44	Josiah Dodds, Andrew W. Appel	Mostly Sound Type System Improves a Foundational Program Verifier.	CPP	2013	DBLP DOI BibTeX RDF
44	Andreas Schropp, Andrei Popescu 0001	Nonfree Datatypes in Isabelle/HOL - Animating a Many-Sorted Metatheory.	CPP	2013	DBLP DOI BibTeX RDF
44	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
44	Andrei Popescu 0001, Johannes Hölzl, Tobias Nipkow	Proving Concurrent Noninterference.	CPP	2012	DBLP DOI BibTeX RDF
44	Christian Doczkal, Gert Smolka	Constructive Completeness for Modal Logic with Transitive Closure.	CPP	2012	DBLP DOI BibTeX RDF
44	Naoki Kobayashi 0001	Program Certification by Higher-Order Model Checking.	CPP	2012	DBLP DOI BibTeX RDF
44	Pierre Neron	A Formal Proof of Square Root and Division Elimination in Embedded Programs.	CPP	2012	DBLP DOI BibTeX RDF
44	Lukas Bulwahn	The New Quickcheck for Isabelle - Random, Exhaustive and Symbolic Testing under One Roof.	CPP	2012	DBLP DOI BibTeX RDF
44	Alexander Vaynberg, Zhong Shao	Compositional Verification of a Baby Virtual Memory Manager.	CPP	2012	DBLP DOI BibTeX RDF
44	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
44	Xavier Leroy	Mechanized Semantics for Compiler Verification.	CPP	2012	DBLP DOI BibTeX RDF
44	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
44	Jianzhou Zhao, Steve Zdancewic	Mechanized Verification of Computing Dominators for Formalizing Compilers.	CPP	2012	DBLP DOI BibTeX RDF
44	Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Gerwin Klein	Noninterference for Operating System Kernels.	CPP	2012	DBLP DOI BibTeX RDF
44	Greg Morrisett	Scalable Formal Machine Models.	CPP	2012	DBLP DOI BibTeX RDF
44	Thierry Coquand, Anders Mörtberg, Vincent Siles	Coherent and Strongly Discrete Rings in Type Theory.	CPP	2012	DBLP DOI BibTeX RDF
44	Kaustuv Chaudhuri	Compact Proof Certificates for Linear Logic.	CPP	2012	DBLP DOI BibTeX RDF
44	Hing-Lun Chan, Michael Norrish	A String of Pearls: Proofs of Fermat's Little Theorem.	CPP	2012	DBLP DOI BibTeX RDF
44	Keisuke Nakano 0001	Shall We Juggle, Coinductively?	CPP	2012	DBLP DOI BibTeX RDF
44	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
44	Brian Campbell 0001	An Executable Semantics for CompCert C.	CPP	2012	DBLP DOI BibTeX RDF
44	Andrea Asperti, Wilmer Ricciotti	Rating Disambiguation Errors.	CPP	2012	DBLP DOI BibTeX RDF
44	Pierre-Nicolas Tollitte, David Delahaye, Catherine Dubois	Producing Certified Functional Code from Inductive Specifications.	CPP	2012	DBLP DOI BibTeX RDF
44	Valentin Robert, Xavier Leroy	A Formally-Verified Alias Analysis.	CPP	2012	DBLP DOI BibTeX RDF
44	Beniamino Accattoli	Proof Pearl: Abella Formalization of λ-Calculus Cube Property.	CPP	2012	DBLP DOI BibTeX RDF
44	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
44	Tom Ridge	Simple, Functional, Sound and Complete Parsing for All Context-Free Grammars.	CPP	2011	DBLP DOI BibTeX RDF
44	James Cheney, Christian Urban	Mechanizing the Metatheory of mini-XQuery.	CPP	2011	DBLP DOI BibTeX RDF
44	Mathieu Boespflug, Maxime Dénès, Benjamin Grégoire	Full Reduction at Full Throttle.	CPP	2011	DBLP DOI BibTeX RDF
44	Sorin Stratulat, Vincent Demange	Automated Certification of Implicit Induction Proofs.	CPP	2011	DBLP DOI BibTeX RDF
44	Thierry Coquand, Vincent Siles	A Decision Procedure for Regular Expression Equivalence in Type Theory.	CPP	2011	DBLP DOI BibTeX RDF
44	Michael Backes 0001, Catalin Hritcu, Thorsten Tarrach	Automatically Verifying Typing Constraints for a Data Processing Language.	CPP	2011	DBLP DOI BibTeX RDF
44	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
44	Martin Henz, Aquinas Hobor	Teaching Experience: Logic and Formal Methods with Coq.	CPP	2011	DBLP DOI BibTeX RDF
44	Andrew W. Appel	VeriSmall: Verified Smallfoot Shape Analysis.	CPP	2011	DBLP DOI BibTeX RDF
44	Christian Doczkal, Gert Smolka	Constructive Formalization of Hybrid Logic with Eventualities.	CPP	2011	DBLP DOI BibTeX RDF
44	Thomas Braibant	Coquet: A Coq Library for Verifying Hardware.	CPP	2011	DBLP DOI BibTeX RDF
44	Nikolaj S. Bjørner	Engineering Theories with Z3.	CPP	2011	DBLP DOI BibTeX RDF
44	Thomas Braibant, Damien Pous	Tactics for Reasoning Modulo AC in Coq.	CPP	2011	DBLP DOI BibTeX RDF
44	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
44	Frank Pfenning, Luís Caires, Bernardo Toninho	Proof-Carrying Code in a Session-Typed Process Calculus.	CPP	2011	DBLP DOI BibTeX RDF