More about HKUST
Advances in Static Analysis and Formal Verification of Smart Contracts
PhD Thesis Proposal Defence
Title: "Advances in Static Analysis and Formal Verification of Smart Contracts"
by
Mr. Soroush FAROKHNIA
Abstract:
Blockchains are a family of distributed consensus protocols that maintain a
shared, append-only ledger without relying on a trusted central authority.
Smart contracts are self-enforcing programs executed on blockchains. They
support arbitrary complex logic. Their applications span multiple domains,
including finance, healthcare, and supply chain management, in both the
public and private sectors. They are currently in charge of billions of
dollars' worth of digital assets. Given their role, any flaw can have
significant financial consequences. Thus, many optimization and verification
problems arise in this domain, yet existing approaches often produce
suboptimal results, lack strong assurances, or do not scale. These
limitations frequently compel developers to rely on manual audits, which are
costly, error-prone, and can leave vulnerabilities undiscovered.
This thesis develops algorithmic foundations that bridge the gap between
scalability and reliable guarantees for smart contracts. We achieve this by
capturing structural properties of contracts using techniques from
parameterized complexity theory, polyhedral geometry, and real algebraic
geometry. We demonstrate how these techniques can significantly advance the
state-of-the-art solutions across various domains, including gas estimation,
compiler optimization, miner revenue maximization, and decentralized
exchange routing. The thesis goes beyond core technical results, arguing
that blockchain benefits from interdisciplinary perspectives that can
uncover costly vulnerabilities otherwise overlooked.
Date: Friday, 16 January 2026
Time: 3:00pm - 5:00pm
Venue: Room 5506
Lifts 25/26
Committee Members: Dr. Jiasi Shen (Supervisor)
Dr. Amir Goharshady (Co-supervisor, Oxford)
Dr. Dimitris Papadopoulos (Chairperson)
Dr. Junxian He