FMBC 2020: 2ND INTERNATIONAL WORKSHOP ON FORMAL METHODS FOR BLOCKCHAINS

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

B
Bitcoin	Towards Verifying the Bitcoin-S Library Mechanized Formal Model of the Bitcoin's Blockchain Validation Procedures Summary of Bitcoin Trace-Net: Formal Contract Verification at Signing Time. (Extended Abstract)
bitcoin-s	Towards Verifying the Bitcoin-S Library
Blockchain	Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper) Inter-blockchain protocols with the Isabelle Infrastructure framework A Blockchain Model in Tamarin Formal Design, Implementation and Verification of Blockchain Languages using K
Blockchains	Mechanized Formal Model of the Bitcoin's Blockchain Validation Procedures Albert, an intermediate smart-contract language for Tezos.
C
Certified compilation	Albert, an intermediate smart-contract language for Tezos.
Certified programming	Albert, an intermediate smart-contract language for Tezos.
code extraction	Verifying, testing and running smart contracts in ConCert
Compiler Optimizations	Populating the Peephole Optimizer of a Smart Contract Compiler
Constraint Solving	Populating the Peephole Optimizer of a Smart Contract Compiler
coq	Mechanized Formal Model of the Bitcoin's Blockchain Validation Procedures Verifying, testing and running smart contracts in ConCert
D
datatypes	Authenticated Data Structures as Functors in Isabelle/HOL
distributed ledger	Authenticated Data Structures as Functors in Isabelle/HOL
E
Elliptic curves	High-assurance field inversion for pairing-friendly primes
Ethereum	Formal Specification and Verification of Solidity Contracts with Events (short paper)
Ethereum Bytecode	Populating the Peephole Optimizer of a Smart Contract Compiler
events	Formal Specification and Verification of Solidity Contracts with Events (short paper)
F
Field inversion	High-assurance field inversion for pairing-friendly primes
First-Order Logic	Formal verification of the Stellar Consensus Protocol
formal analysis	Formal Design, Implementation and Verification of Blockchain Languages using K
formal methods	Mechanized Formal Model of the Bitcoin's Blockchain Validation Procedures
Formal verification	A Blockchain Model in Tamarin WhylSon: Proving your Michelson Smart Contracts in Why3
functor	Authenticated Data Structures as Functors in Isabelle/HOL
H
hash time lock contract	A Blockchain Model in Tamarin
High-assurance crypto	High-assurance field inversion for pairing-friendly primes
higher-order logic	Authenticated Data Structures as Functors in Isabelle/HOL
I
inter-blockchain protocols	Inter-blockchain protocols with the Isabelle Infrastructure framework
interactive theorem proving	Inter-blockchain protocols with the Isabelle Infrastructure framework
Intermediate representation	Tezla, an intermediate representation for static analysis of Michelson smart contracts
Ivy	Formal verification of the Stellar Consensus Protocol
K
K framework	Formal Design, Implementation and Verification of Blockchain Languages using K
L
languages	Formal Design, Implementation and Verification of Blockchain Languages using K
Linear types	Albert, an intermediate smart-contract language for Tezos.
Liveness	Formal verification of the Stellar Consensus Protocol
M
Merkle tree	Authenticated Data Structures as Functors in Isabelle/HOL
MetaCoq	Verifying, testing and running smart contracts in ConCert
Michelson	Tezla, an intermediate representation for static analysis of Michelson smart contracts WhylSon: Proving your Michelson Smart Contracts in Why3
model checking	Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper) Summary of Bitcoin Trace-Net: Formal Contract Verification at Signing Time. (Extended Abstract)
P
petri net	Summary of Bitcoin Trace-Net: Formal Contract Verification at Signing Time. (Extended Abstract)
Programming languages	Albert, an intermediate smart-contract language for Tezos.
proof assistants	Verifying, testing and running smart contracts in ConCert
property-based testing	Verifying, testing and running smart contracts in ConCert
S
Safety	Formal verification of the Stellar Consensus Protocol
Scala	Towards Verifying the Bitcoin-S Library
Smart contract	Tezla, an intermediate representation for static analysis of Michelson smart contracts
smart contracts	Formal Specification and Verification of Solidity Contracts with Events (short paper) Inter-blockchain protocols with the Isabelle Infrastructure framework Albert, an intermediate smart-contract language for Tezos. Summary of Bitcoin Trace-Net: Formal Contract Verification at Signing Time. (Extended Abstract) Verifying, testing and running smart contracts in ConCert WhylSon: Proving your Michelson Smart Contracts in Why3
Solidity	Formal Specification and Verification of Solidity Contracts with Events (short paper)
specification	Formal Specification and Verification of Solidity Contracts with Events (short paper)
Stainless	Towards Verifying the Bitcoin-S Library
Static analysis	Tezla, an intermediate representation for static analysis of Michelson smart contracts
Stellar Consensus Protocol	Formal verification of the Stellar Consensus Protocol
symbolic execution	Summary of Bitcoin Trace-Net: Formal Contract Verification at Signing Time. (Extended Abstract)
T
Tamarin	A Blockchain Model in Tamarin
Tendermint	Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper)
Tezos	WhylSon: Proving your Michelson Smart Contracts in Why3
Tezos blockchain	Tezla, an intermediate representation for static analysis of Michelson smart contracts
TLA+	Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper)
U
utxo	Mechanized Formal Model of the Bitcoin's Blockchain Validation Procedures
V
validation	Mechanized Formal Model of the Bitcoin's Blockchain Validation Procedures
verification	Formal Specification and Verification of Solidity Contracts with Events (short paper) High-assurance field inversion for pairing-friendly primes Verifying, testing and running smart contracts in ConCert
verification tools	Formal Design, Implementation and Verification of Blockchain Languages using K
voting protocols	Verifying, testing and running smart contracts in ConCert
W
Why3	WhylSon: Proving your Michelson Smart Contracts in Why3

Disclaimer | Powered by EasyChair Smart Program