FMBC'19: WORKSHOP ON FORMAL METHODS FOR BLOCKCHAINS

This page contains an index consisting of author-provided keywords.

A
Ada	Call me Back, I have a Type Invariant
address type	Solidity 0.5: when typed does not mean type safe
Algorand	Towards a Verified Model of the Algorand Consensus Protocol in Coq
B
Bitcoin	A Distributed Blockchain Model of Selfish Mining
blockchain	Statistical Model Checking of RANDAO's Resilience to Pre-computed Reveal Strategies Verifying Smart Contracts with Cubicle Towards a Verified Model of the Algorand Consensus Protocol in Coq Call me Back, I have a Type Invariant
Blockchains	Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts
Byzantine consensus	Towards a Verified Model of the Algorand Consensus Protocol in Coq
C
Certified programming	Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts
Coq	Towards a Smart Contract Verification Framework in Coq Towards a Verified Model of the Algorand Consensus Protocol in Coq Smart Contract Interactions in Coq
D
DAO	Smart Contract Interactions in Coq
deductive verification	Deductive Proof of Industrial Smart Contracts Using Why3
Distributed Ledger Applications	Smart Contracts: Application Scenarios for Deductive Program Verification
E
Execution layer	Smart Contract Interactions in Coq
F
formal methods	Call me Back, I have a Type Invariant
formal specification	Formal specification of a security framework for smart contracts
formal verification	Call me Back, I have a Type Invariant
H
Hyperledger Fabric	Smart Contracts: Application Scenarios for Deductive Program Verification
I
Isabelle	Formal specification of a security framework for smart contracts
M
Maude	Statistical Model Checking of RANDAO's Resilience to Pre-computed Reveal Strategies
MCMT	Verifying Smart Contracts with Cubicle
Metaprogramming	Towards a Smart Contract Verification Framework in Coq
Model Checking	Verifying Smart Contracts with Cubicle
P
Probabilistic Model Checking	A Distributed Blockchain Model of Selfish Mining
Program Verification	Smart Contracts: Application Scenarios for Deductive Program Verification
programming languages	Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts Call me Back, I have a Type Invariant
R
RANDAO	Statistical Model Checking of RANDAO's Resilience to Pre-computed Reveal Strategies
Rewriting logic	Statistical Model Checking of RANDAO's Resilience to Pre-computed Reveal Strategies
S
security	Formal specification of a security framework for smart contracts
Selfish mining	A Distributed Blockchain Model of Selfish Mining
Smart Contract	Towards a Smart Contract Verification Framework in Coq
smart contracts	Solidity 0.5: when typed does not mean type safe Smart Contracts: Application Scenarios for Deductive Program Verification Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts Deductive Proof of Industrial Smart Contracts Using Why3 Call me Back, I have a Type Invariant Formal specification of a security framework for smart contracts Smart Contract Interactions in Coq
Smart-contracts	Verifying Smart Contracts with Cubicle
solidity	Deductive Proof of Industrial Smart Contracts Using Why3
Statistical Model Checking	Statistical Model Checking of RANDAO's Resilience to Pre-computed Reveal Strategies
T
type soundness	Solidity 0.5: when typed does not mean type safe
Type theory	Towards a Smart Contract Verification Framework in Coq Smart Contract Interactions in Coq
U
UPPAAL-SMC	A Distributed Blockchain Model of Selfish Mining
W
why3	Deductive Proof of Industrial Smart Contracts Using Why3

Disclaimer | Powered by EasyChair Smart Program