Proceedings of the 2015 Conference on Certified Programs and Proofs - CPP '15
Latest Publications

TOTAL DOCUMENTS

(FIVE YEARS 0)

H-INDEX

(FIVE YEARS 0)

Published By ACM Press

9781450332965

Latest Documents Most Cited Documents Contributed Authors Related Sources Related Keywords

Recording Completion for Certificates in Equational Reasoning

Proceedings of the 2015 Conference on Certified Programs and Proofs - CPP '15 ◽

10.1145/2676724.2693171 ◽

2015 ◽

Cited By ~ 2

Author(s):

Thomas Sternagel ◽

Sarah Winkler ◽

Harald Zankl

Keyword(s):

Equational Reasoning

Download Full-text

Correctness of Isabelle's Cyclicity Checker

Proceedings of the 2015 Conference on Certified Programs and Proofs - CPP '15 ◽

10.1145/2676724.2693175 ◽

2015 ◽

Cited By ~ 11

Author(s):

Ondřej Kunčar

Download Full-text

A Verified Algorithm for Geometric Zonotope/Hyperplane Intersection

Proceedings of the 2015 Conference on Certified Programs and Proofs - CPP '15 ◽

10.1145/2676724.2693164 ◽

2015 ◽

Cited By ~ 10

Author(s):

Fabian Immler

Download Full-text

Proving Lock-Freedom Easily and Automatically

Proceedings of the 2015 Conference on Certified Programs and Proofs - CPP '15 ◽

10.1145/2676724.2693179 ◽

2015 ◽

Cited By ~ 1

Author(s):

Xiao Jia ◽

Wei Li ◽

Viktor Vafeiadis

Download Full-text

A Typed C11 Semantics for Interactive Theorem Proving

Proceedings of the 2015 Conference on Certified Programs and Proofs - CPP '15 ◽

10.1145/2676724.2693571 ◽

2015 ◽

Cited By ~ 17

Author(s):

Robbert Krebbers ◽

Freek Wiedijk

Keyword(s):

Theorem Proving ◽

Interactive Theorem Proving

Download Full-text

Certified Normalization of Context-Free Grammars

Proceedings of the 2015 Conference on Certified Programs and Proofs - CPP '15 ◽

10.1145/2676724.2693177 ◽

2015 ◽

Cited By ~ 2

Author(s):

Denis Firsov ◽

Tarmo Uustalu

Keyword(s):

Context Free ◽

Context Free Grammars

Download Full-text

The Speedup Theorem in a Primitive Recursive Framework

Proceedings of the 2015 Conference on Certified Programs and Proofs - CPP '15 ◽

10.1145/2676724.2693178 ◽

2015 ◽

Cited By ~ 1

Author(s):

Andrea Asperti

Keyword(s):

Primitive Recursive

Download Full-text

Formal Reasoning about the C11 Weak Memory Model

Proceedings of the 2015 Conference on Certified Programs and Proofs - CPP '15 ◽

10.1145/2676724.2693181 ◽

2015 ◽

Cited By ~ 2

Author(s):

Viktor Vafeiadis

Keyword(s):

Memory Model ◽

Formal Reasoning

Download Full-text

Verified Validation of Program Slicing

Proceedings of the 2015 Conference on Certified Programs and Proofs - CPP '15 ◽

10.1145/2676724.2693169 ◽

2015 ◽

Cited By ~ 6

Author(s):

Sandrine Blazy ◽

Andre Maroneze ◽

David Pichardie

Keyword(s):

Program Slicing

Download Full-text

Practical Tactics for Verifying C Programs in Coq

Proceedings of the 2015 Conference on Certified Programs and Proofs - CPP '15 ◽

10.1145/2676724.2693162 ◽

2015 ◽

Cited By ~ 4

Author(s):

Jingyuan Cao ◽

Ming Fu ◽

Xinyu Feng

Keyword(s):

C Programs

Download Full-text

Proceedings of the 2015 Conference on Certified Programs and Proofs - CPP '15Latest Publications

TOTAL DOCUMENTS

H-INDEX

Published By ACM Press

Recording Completion for Certificates in Equational Reasoning

Correctness of Isabelle's Cyclicity Checker

A Verified Algorithm for Geometric Zonotope/Hyperplane Intersection

Proving Lock-Freedom Easily and Automatically

A Typed C11 Semantics for Interactive Theorem Proving

Certified Normalization of Context-Free Grammars

The Speedup Theorem in a Primitive Recursive Framework

Formal Reasoning about the C11 Weak Memory Model

Verified Validation of Program Slicing

Practical Tactics for Verifying C Programs in Coq

Proceedings of the 2015 Conference on Certified Programs and Proofs - CPP '15
Latest Publications