We develop program analysis techniques and formal verification methods for improving software reliability and security. Our current focus is on static analysis of smart contracts, automated vulnerability detection in DeFi protocols, and scalable formal reasoning for EVM-compatible blockchains.
Static and dynamic analysis of Solidity and Vyper smart contracts. We develop tools that detect reentrancy, access control, and arithmetic vulnerabilities before deployment, combining abstract interpretation with symbolic execution.
Formal verification of decentralised finance protocol invariants. Our work ensures that economic properties — such as liquidity conservation and fair pricing — hold under all possible execution paths.
Theoretical foundations of static analysis, including abstract interpretation, dataflow analysis, and type-based reasoning. We design novel abstract domains tailored to the semantics of blockchain execution environments.
Formalisation of the Ethereum Virtual Machine in proof assistants. Our mechanised EVM specification serves as a trusted foundation for reasoning about bytecode-level properties of deployed contracts.
Scalable automated auditing pipelines that combine multiple analysis passes — pattern matching, taint analysis, SMT-based verification — to produce comprehensive security reports with minimal false positives.
Analysis of bridge protocols and cross-chain messaging systems. We study the formal security guarantees of inter-chain communication and develop tools for verifying bridge contract correctness.
We are actively recruiting PhD students and postdoctoral researchers. If you are interested in program analysis or smart contract security, please contact us at atlas@anf.edu.pl.
ATLAS Lab
Blockchain Security Building
ul. Wróblewskiego 9, Room 204
50-376 Wrocław, Poland