Advancing the science of certainty through formal methods, program analysis, and mathematical logic.
Automatically generating programs from specifications. Our group develops synthesis techniques using type-directed search, sketching, and machine learning to produce provably correct code fragments.
A technique for program optimisation that explores the entire space of equivalent programs simultaneously. ANF researchers have contributed foundational theoretical results and practical tools for e-graph-based rewriting.
Compact data structures that efficiently represent large equivalence classes of expressions. Our work extends classical e-graph algorithms to support recursive and higher-order language constructs.
Analysing programs without executing them to find bugs, security vulnerabilities, and performance bottlenecks. We develop scalable analyses for industrial-size codebases.
A mathematical framework for approximating program semantics. Rector Zielińska's group pioneered its application to concurrent systems, enabling verification of multi-threaded programs.
Formally proving that blockchain smart contracts behave as intended. Our Solidity verification framework has been used to audit contracts holding over €2 billion in value.
Automatically finding and fixing bugs in source code. Our techniques combine symbolic execution with synthesis to generate patches that are provably correct.
The study of type systems as a foundation for both mathematics and programming. Our researchers contribute to dependent types, linear types, and their implementation in Coq and Lean.
Software tools that help construct machine-checked proofs. We develop tactics, automation strategies, and libraries for Coq and contribute to the Lean mathematical library.
Our research is organised into seven laboratories, each led by a senior faculty member. Labs operate with significant autonomy, fostering deep specialisation while collaborating across disciplinary boundaries.
Since 2004, the Wrocław Formal Methods Workshop has been ANF's flagship academic event. Each June, 80–120 researchers from across Europe gather for three days of invited talks, contributed papers, and poster sessions. WFMW has become a key venue for presenting early-stage work in program verification, type theory, and automated reasoning, with proceedings published by Springer LNCS.
WFMW 2026 — June 15–17, Wrocław
Visit Workshop Website