Verifolio
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.
Download
Verifolio v0.1 – VirtualBox virtual machine (.ova) Download (5.6 GB)
SHA1: 0112030b31d8cee2e47cb35fb69b34bcc3f77db0
Username/password for the VM: vagrant
/ vagrant
Publications
2017 | |
[5] | Empirical software metrics for benchmarking of verification tools Formal Methods in System Design, volume 50, number 2-3, pages 289–316, 2017. |
2015 | |
[4] | Empirical Software Metrics for Benchmarking of Verification Tools Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, pages 561–579, July 2015. |
[3] | Loop Patterns in C Programs ECEASST, volume 72, 2015. |
2014 | |
[2] | Loop Patterns in C Programs January 2014, Master's thesis, TU Wien. |
2013 | |
[1] | On the Concept of Variable Roles and its Use in Software Analysis FMCAD, pages 226–229, 2013. |