Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs - CPP 2016
Latest Publications

TOTAL DOCUMENTS

(FIVE YEARS 0)

H-INDEX

(FIVE YEARS 0)

Published By ACM Press

9781450341271

Latest Documents Most Cited Documents Contributed Authors Related Sources Related Keywords

Formal verification of control-flow graph flattening

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs - CPP 2016 ◽

10.1145/2854065.2854082 ◽

2016 ◽

Cited By ~ 5

Author(s):

Sandrine Blazy ◽

Alix Trieu

Keyword(s):

Formal Verification ◽

Control Flow ◽

Control Flow Graph ◽

Flow Graph

Download Full-text

Towards a Mizar environment for Isabelle: foundations and language

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs - CPP 2016 ◽

10.1145/2854065.2854070 ◽

2016 ◽

Cited By ~ 10

Author(s):

Cezary Kaliszyk ◽

Karol Pąk ◽

Josef Urban

Download Full-text

A logic of proofs for differential dynamic logic: toward independently checkable proof certificates for dynamic logics

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs - CPP 2016 ◽

10.1145/2854065.2854078 ◽

2016 ◽

Cited By ~ 2

Author(s):

Nathan Fulton ◽

André Platzer

Keyword(s):

Dynamic Logic ◽

Logic Of Proofs ◽

Checkable Proof ◽

Dynamic Logics

Download Full-text

Bisimulation up-to techniques for psi-calculi

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs - CPP 2016 ◽

10.1145/2854065.2854080 ◽

2016 ◽

Cited By ~ 2

Author(s):

Johannes Åman Pohjola ◽

Joachim Parrow

Download Full-text

Perspectives on formal verification (invited talk)

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs - CPP 2016 ◽

10.1145/2854065.2858808 ◽

2016 ◽

Author(s):

Harvey M. Friedman

Keyword(s):

Formal Verification

Download Full-text

Refinement based verification of imperative data structures

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs - CPP 2016 ◽

10.1145/2854065.2854067 ◽

2016 ◽

Cited By ~ 18

Author(s):

Peter Lammich

Keyword(s):

Data Structures

Download Full-text

Formalizing Jordan normal forms in Isabelle/HOL

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs - CPP 2016 ◽

10.1145/2854065.2854073 ◽

2016 ◽

Cited By ~ 12

Author(s):

René Thiemann ◽

Akihisa Yamada

Keyword(s):

Normal Forms

Download Full-text

Planning for change in a formal verification of the raft consensus protocol

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs - CPP 2016 ◽

10.1145/2854065.2854081 ◽

2016 ◽

Cited By ~ 43

Author(s):

Doug Woos ◽

James R. Wilcox ◽

Steve Anton ◽

Zachary Tatlock ◽

Michael D. Ernst ◽

...

Keyword(s):

Formal Verification ◽

Consensus Protocol

Download Full-text

A modular, efficient formalisation of real algebraic numbers

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs - CPP 2016 ◽

10.1145/2854065.2854074 ◽

2016 ◽

Cited By ~ 5

Author(s):

Wenda Li ◽

Lawrence C. Paulson

Keyword(s):

Algebraic Numbers

Download Full-text

Axiomatic semantics for compiler verification

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs - CPP 2016 ◽

10.1145/2854065.2854083 ◽

2016 ◽

Author(s):

Steven Schäfer ◽

Sigurd Schneider ◽

Gert Smolka

Keyword(s):

Compiler Verification ◽

Axiomatic Semantics

Download Full-text

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs - CPP 2016Latest Publications

TOTAL DOCUMENTS

H-INDEX

Published By ACM Press

Formal verification of control-flow graph flattening

Towards a Mizar environment for Isabelle: foundations and language

A logic of proofs for differential dynamic logic: toward independently checkable proof certificates for dynamic logics

Bisimulation up-to techniques for psi-calculi

Perspectives on formal verification (invited talk)

Refinement based verification of imperative data structures

Formalizing Jordan normal forms in Isabelle/HOL

Planning for change in a formal verification of the raft consensus protocol

A modular, efficient formalisation of real algebraic numbers

Axiomatic semantics for compiler verification

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs - CPP 2016
Latest Publications