Skip to content

Amrita-TIFAC-Cyber-Blockchain/Formal-Methods-Blockchain

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

13 Commits
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Formal Methods and Verification of Blockchain Consensus and Smart Contracts




PhD Thesis and Conferences

Organisations

Bibliometric Analysis and Literature Survey

Click Here to view.

Model Formalisms, Specification and Verification

Model Formalisms

Contract-Level Models - (High-level or Abstract-level)

Program-Level Models - (Source code or compiled bytecode-level)

Specification Logic

  • Temporal Logic
    • Linear Temporal Logic
    • Computation Tree Logic
  • Dynamic Logic
  • Deontic and Defeasible Logics
  • Defeasible logic
  • Hoare-Style Properties
  • Program Path-Level Patterns

Verification Technique and Tools

Model Checking Theorem Proving Program Verification Symbolic & Concolic Execution Runtime Verification & Testing
NuSMV, nuXmv
SPIN
CPN
BIP-SMC
PRISM
UPPAAL
MCK
Maude
FDR
Ambient Calculus
LDLf
Coq
Isabelle/HOL
Agda
Datalog & Soufflé
Boogie Verifier & Corral
LLVM & SMACK
SeaHorn
F*
KeY
Why3
K framework
Custom static analyses
Oyente
Maian
Mythril
teEther
Manticore
Securify
SmartCheck
ContractLarva
EVM*
ReGuard
SODA
Solythesis
ECFChecker

Languages

Bitcoin Ethereum Hyperledger Cardano Solana Libra/Calibra Tezos RChain Aeternity Stratis Aergo
BitML Solidity
Vyper
Yul
FE
Bamboo
Go
Obsidian
Marlowe
Plutus
Rust
C
Move Michelson Rholang Sophia C# Lua
SCL

Formal Verified Blockchain Ecosystem

  • KEVEM - K Semantics of the Ethereum Virtual Machine

Amrita Blockchain and Distributed - Vulnerability Tracker (ABCD - VT)

Click Here to view.

References