Verifolio is a portfolio software verification tool.

Given a verification task and a verification property, it tries to predict the best tool from a predefined set of black-box verification tools. Our portfolio is based on high-level software metrics, variable roles and loop patterns. We have evaluated Verifolio on data from the International Competition on Software Verification (SV-COMP), where our portfolio outperforms any of the participating standalone verifiers.

NEW: Students interested in formal methods and machine learning should check related master’s thesis and semester project topics.



Verifolio v0.1 – VirtualBox virtual machine (.ova) Download (5.6 GB)
SHA1: 0112030b31d8cee2e47cb35fb69b34bcc3f77db0

Username/password for the VM: vagrant / vagrant


[5] Empirical software metrics for benchmarking of verification tools
Yulia Demyanova, Thomas Pani, Helmut Veith, Florian Zuleger
Formal Methods in System Design, volume 50, number 2-3, pages 289–316, 2017.
[bibtex] [pdf] [doi]
[4] Empirical Software Metrics for Benchmarking of Verification Tools
Yulia Demyanova, Thomas Pani, Helmut Veith, Florian Zuleger
Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, pages 561–579, July 2015.
[bibtex] [pdf] [doi]
[3] Loop Patterns in C Programs
Thomas Pani, Helmut Veith, Florian Zuleger
ECEASST, volume 72, 2015.
[bibtex] [pdf] [doi]
[2]Loop Patterns in C Programs
Thomas Pani
January 2014, Master's thesis, TU Wien.
[1] On the Concept of Variable Roles and its Use in Software Analysis
Yulia Demyanova, Helmut Veith, Florian Zuleger
FMCAD, pages 226–229, 2013.
[bibtex] [pdf]

Latest News

Jens Pagel wins Bill McCune PhD Award

We congratulate Jens Pagel for receiving the 2021 Bill McCune PhD Award in Automated Reasoning! Jens graduated in 2020; his thesis on Decision procedures for separation logic: beyond symbolic heaps (supervised by Florian Zuleger) presents his substantial contributions to the theory of formal verification and automated reasoning, and to verifying heap-manipulating programs in particular.

Continue reading

Full news archive