Project funded by the Vienna Science and Technology Fund

Duration: 2023-09-01 ‒ 2027-08-31 (ongoing)

Funding: € 799.850

Members

• Dr.in. sc. Maria Christakis (PI), Professor, TU Wien

  • Christoph Hochrainer, Dipl. Ing., Pre-doc, TU Wien

• Dr. Matteo Maffei (co-PI), Professor, TU Wien

  • Markus Scherer, Dipl. Ing. / BSc., Pre-doc, TU Wien
  • Andreas Lackner, Dipl. Ing. / BSc., Pre-doc, TU Wien

• Dr.in. techn. Laura Kovács (co-PI), Professor, TU Wien

  • Johannes Schoisswohl, Dipl.-Ing. / BSc, Pre-doc, TU Wien
  • Sophie Rain, Dipl.-Ing.in / BSc, Pre-doc, TU Wien
  • Clemens Eisenhofer, Dipl.-Ing. / BSc, Pre-doc, TU Wien
  • Robin Coutelier, MSc, Pre-doc, TU Wien
  • Eva-Marie Wagner, Dipl.-Ing.in / BSc, Pre-doc, TU Wien

Project

Correctness and security of smart contracts is critical as digital assets may be at stake. To detect or evenis critical as digital assets may be at stake. To detect or even avoid such vulnerabilities in smart contracts, there have emerged bug-finding techniques, which lackin smart contracts, there have emerged bug-finding techniques, which lack soundness, and verification techniques, which lack precision.

In ForSmart, we aim to develop a hybrid, automated certification framework for smart contracts thatIn ForSmart, we aim to develop a hybrid, automated certification framework for smart contracts that symbiotically combines bug-finding in the form of test generation and verification in the form of sound staticin the form of test generation and verification in the form of sound static analysis, thereby achieving soundness and precision. Advanced automated-reasoning mechanisms, which we plan to develop and tailor to this domain, will support both testing and static analysis.to this domain, will support both testing and static analysis.

We will maximize the impact of ForSmart by applying our framework to concrete applications of academic,of academic, industrial, and public relevance, such as DeFi apps, with a focus on certifying functional and securitya focus on certifying functional and security properties, as well as by making our infrastructure available to contract developers, auditors, and users. Weas by making our infrastructure available to contract developers, auditors, and users. We additionally plan to leverage our ongoing collaborations with Certora, the Ethereum Foundation, ConsenSys, and Microsoft Research.

We request funding for 3 PhD students. The duration of each PhD will be 4 years – the funding will cover3 PhD students. The duration of each PhD will be 4 years the funding will cover 3.5 years, and the remaining time will be spent on internships at the aforementioned companies tothe aforementioned companies to encourage industrial adoption of our framework.our framework.

The core team of ForSmart (PIs) has a 2/3 female participation. We aim to maintain such a balance when(Pls) has a 2/3 female participation. We aim to maintain such a balance when expanding

Keywords: test generation, static analysis, automated reasoning, hybrid, certification, smart contracts

Results

• Christoph Hochrainer, Anastasia Isychev, Valentin Wüstholz and Maria Christakis. Fuzzing Processing Pipelines for Zero-Knowledge Circuits. In Proceedings of the 31st International Conference on Computer and Communications Security (CCS'25), 2025. ACM. To appear.
• Márton Hajdú, Laura Kovács, and Andrei Voronkov. Partial Redundancy in Saturation. In 30th International Conference on Automated Deduction (CADE), pages 532-551, 2025
• Márton Hajdú, Robin Coutelier, Laura Kovács, and Andrei Voronkov. Term Ordering Diagrams. In 30th International Conference on Automated Deduction (CADE), pages 552-569, 2025
• Filip Bártek, Ahmed Bhayat, Robin Coutelier, Márton Hajdú, Matthias Hetzenberger, Petra Hozzová, Laura Kovács, Jakob Rath, Michael Rawson, Giles Reger, Martin Suda, Johannes Schoisswohl, and Andrei Voronkov. “The Vampire Diary”. In 37th International Conference on Computer Aided Verification (CAV), pages 57-71, 2025
• Lorenzo Benetollo, Andreas Lackner, Matteo Maffei, Markus Scherer. Let’s Move2EVM. Usenix Security 2025, 1339-1355. https://www.usenix.org/conference/usenixsecurity25/presentation/benetollo
• Jakob Rath, Clemens Eisenhofer, Daniela Kaufmann, Nikolaj Bjørner and Laura Kovács. PolySat: Word-level Bit-vector Reasoning in Z3. In Proceedings of the 16th International Conference on Verified Software: Theories, Tools and Experiments (VSTTE), pages 47–69, 2024
• Robin Coutelier, Laura Kovács, Michael Rawson, Jakob Rath, Armin Biere. “SAT Solving for Variants of First-order Subsumption”. Formal Methods in System Design, 2024.
• Markus Scherer, Jeppe Fredsgaard Blaabjerg, Alexander Sjösten, Magdalena Solitro and Matteo Maffei, “Wappler: Sound Reachability Analysis for WebAssembly,” in 2024 IEEE 37th Computer Security Foundations Symposium (CSF), Enschede, Netherlands, 2024 pp. 249-264. https://www.computer.org/csdl/proceedings-article/csf/2024/620300a377/1W0eVUjUN2g
• Robin Coutelier, Mathias Fleury, Laura Kovács: “Lazy Reimplication in Chronological Backtracking”. SAT 2024: 9:1-9:19. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.9
• Scott Wesley, Maria Christakis, Jorge A. Navas, Richard Trefler, Valentin Wüstholz and Arie Gurfinkel. Inductive Predicate Synthesis Modulo Programs (Extended). CoRR abs/2407.08455, 2024. https://arxiv.org/abs/2407.084 55
• Jana Chadt, Christoph Hochrainer, Valentin Wüstholz and Maria Christakis. Olympia: Fuzzer Benchmarking for Solidity. In Proceedings of the 39th International Conference on Automated Software Engineering (ASE'24), 2024. ACM. https://mariachris.github.io/publications.html
• Scott Wesley, Maria Christakis, Jorge A. Navas, Richard Trefler, Valentin Wüstholz and Arie Gurfinkel. Inductive Predicate Synthesis Modulo Programs. In Proceedings of the 38th European Conference on Object-Oriented Programming (ECOOP'24), 2024. Schloss Dagstuhl. https://mariachris.github.io/Pubs/ECOOP-2024.pdf
• Johannes Schoisswohl, Laura Kovács, Konstantin Korovin. VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic. LPAR 2024: 147-164
• Pamina Georgiou, Márton Hajdú, Laura Kovács. Saturating Sorting without Sorts. LPAR 2024: 88-105. https://easychair.org/publications/paper/qbDc
• Sophie Rain, Lea Salome Brugger, Anja Petkovic Komel, Laura Kovács, Michael Rawson. Scaling CheckMate for Game-Theoretic Security. LPAR 2024: 222-231. https://easychair.org/publications/paper/6ZDH
• Márton Hajdú, Laura Kovács, Michael Rawson. Rewriting and Inductive Reasoning. LPAR 2024: 278-294. https://easychair.org/publications/paper/T1mjX
• Simon Jeanteur, Laura Kovacs, Matteo Maffei and Michael Rawson, “CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model,” in 2024 IEEE Symposium on Security and Privacy (SP), San Francisco, CA, USA, 2024 pp. 3165-3183. https://doi.org/10.1109/SP54263.2024.00246
• Clemens Eisenhofer, Laura Kovács, Michael Rawson. Embedding the Connection Calculus in Satisfiability Modulo Theories. AReCCa@TABLEAUX 2023: 54-63. https://ceur-ws.org/Vol-3613/AReCCa2023_paper4.pdf
• Laura Kovács, Petra Hozzová, Marton Hajdu, Andrei Voronkov. Induction in Saturation. IJCAR 2024: 21-29. https://doi.org/10.1007/978-3-031-63498-7_2
• Márton Hajdu, Laura Kovács, Michael Rawson, Andrei Voronkov. Reducibility Constraints in Superposition. IJCAR 2024: 115-132. https://doi.org/10.1007/978-3-031-63498-7_8
• Petra Hozzová, Daneshvar Amrollahi, Márton Hajdu, Laura Kovács, Andrei Voronkov, Eva Maria Wagner. Synthesis of Recursive Programs in Saturation. IJCAR 2024: 154-171. https://doi.org/10.1007/978-3-031-63498-7_10
• Thomas Hader, Daniela Kaufmann, Ahmed Irfan, Stéphane Graham-Lengrand, Laura Kovács. MCSat-Based Finite Field Reasoning in the Yices2 SMT Solver (Short Paper). IJCAR 2024: 386–395. https://doi.org/10.1007/978-3-031-63498-7_23