Files in this item

FilesDescriptionFormat

application/pdf

application/pdfcasper-report.pdf (424kB)
(no description provided)PDF

Description

Title:Verification of Casper in the Coq Proof Assistant
Author(s):Palmskog, Karl; Gligoric, Milos; Pena, Lucas; Moore, Brandon; Rosu, Grigore
Subject(s):Casper, Blockchain, Formal Verification
Abstract:This report describes our effort to model and verify the Casper blockchain finality system in the Coq proof assistant. We outline the salient details on blockchain systems using Casper, describe previous verification efforts we used as a starting point, and give an overview of the formal definitions and properties proved. The Coq source files are available at: https://github.com/runtimeverification/casper-proofs
Issue Date:2018-11-19
Genre:Report (Grant or Annual)
Technical Report
Article
Type:Text
Language:English
URI:http://hdl.handle.net/2142/102075
Date Available in IDEALS:2018-11-25


This item appears in the following Collection(s)

Item Statistics