Search results for "CPP"

Hits ?▲	Authors	Title	Venue	Year	Link
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

Publications at "CPP"( http://dblp.L3S.de/Venues/CPP )