DiVinE 3.0–an explicit-state model checker for multithreaded C & C++ programs J Barnat, L Brim, V Havel, J Havlíček, J Kriho, M Lenčo, P Ročkai, V Štill, ... Computer Aided Verification: 25th International Conference, CAV 2013, Saint …, 2013 | 175 | 2013 |
Model Checking of C and C++ with DIVINE 4 Z Baranová, J Barnat, K Kejstová, T Kučera, H Lauko, J Mrázek, P Ročkai, ... Automated Technology for Verification and Analysis: 15th International …, 2017 | 92 | 2017 |
DiVM: model checking with LLVM and graph memory P Ročkai, V Štill, I Černá, J Barnat Journal of Systems and Software 143, 1-13, 2018 | 25 | 2018 |
Fast, dynamically-sized concurrent hash table J Barnat, P Ročkai, V Štill, J Weiser International SPIN Workshop on Model Checking of Software, 49-65, 2015 | 14 | 2015 |
Extending DIVINE with Symbolic Verification Using SMT: (Competition Contribution) H Lauko, V Štill, P Ročkai, J Barnat International Conference on Tools and Algorithms for the Construction and …, 2019 | 12 | 2019 |
Using off-the-shelf exception support components in C++ verification V Štill, P Ročkai, J Barnat 2017 IEEE International Conference on Software Quality, Reliability and …, 2017 | 9 | 2017 |
DIVINE: Explicit-State LTL Model Checker: (Competition Contribution) V Štill, P Ročkai, J Barnat International Conference on Tools and Algorithms for the Construction and …, 2016 | 9 | 2016 |
Weak memory models as LLVM-to-LLVM transformations V Štill, P Ročkai, J Barnat International Doctoral Workshop on Mathematical and Engineering Methods in …, 2015 | 9 | 2015 |
Optimizing and Caching SMT Queries in SymDIVINE: (Competition Contribution) J Mrázek, M Jonáš, V Štill, H Lauko, J Barnat Tools and Algorithms for the Construction and Analysis of Systems: 23rd …, 2017 | 8 | 2017 |
State space compression for the DiVinE model checker V Štill Masarykova univerzita, Fakulta informatiky, 2013 | 8 | 2013 |
LLVM transformations for model checking V Štill Masarykova univerzita, Fakulta informatiky, 2016 | 7 | 2016 |
Techniques for memory-efficient model checking of C and C++ code P Ročkai, V Štill, J Barnat SEFM 2015 Collocated Workshops, 268-282, 2015 | 7 | 2015 |
Model checking of C++ programs under the x86-tso memory model V Štill, J Barnat Formal Methods and Software Engineering: 20th International Conference on …, 2018 | 6 | 2018 |
Context-switch-directed verification in DIVINE V Štill, P Ročkai, J Barnat International Doctoral Workshop on Mathematical and Engineering Methods in …, 2014 | 5 | 2014 |
Local nontermination detection for parallel C++ programs V Štill, J Barnat Software Engineering and Formal Methods: 17th International Conference, SEFM …, 2019 | 2 | 2019 |
On verifying C++ programs with probabilities J Barnat, I Černá, P Ročkai, V Štill, K Zákopčanová Proceedings of the 31st Annual ACM Symposium on Applied Computing, 1238-1243, 2016 | 2 | 2016 |
Automatic Test Generation for Haskell Programming Assignments V Štill Proceedings of the 2020 ACM Conference on Innovation and Technology in …, 2020 | 1 | 2020 |
DiVinE 2.0 P Ročkai, J Barnat, L Brim, M Češka | | 2009 |
DIVINE: Extended Compilation-based Symbolic Verification Z Baranová, L Korencik, H Lauko, A Matoušek, P Rockai, V Štill | | |
Analysis of Parallel C++ Programs V Štill | | |