Abstract
SMACK and Corral are two components of a modular toolchain for verifying C programs. Together they exploit state-of-the-art compiler technologies and theorem provers to simplify and dispatch verification conditions.
Citation
Arvind Haran,
Montgomery Carter,
Michael Emmi,
Akash Lal,
Shaz Qadeer,
Zvonimir Rakamaric
SMACK+Corral: A Modular Verifier (Competition Contribution)
Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 9035: 450--453, doi:10.1007/978-3-662-46681-0_42, 2015.
BibTeX
@inproceedings{2015_tacas_hcelqr,
title = {SMACK+Corral: A Modular Verifier (Competition Contribution)},
author = {Arvind Haran and Montgomery Carter and Michael Emmi and Akash Lal and Shaz Qadeer and Zvonimir Rakamaric},
booktitle = {Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
series = {Lecture Notes in Computer Science},
volume = {9035},
publisher = {Springer},
editor = {Christel Baier and Cesare Tinelli},
pages = {450--453},
doi = {10.1007/978-3-662-46681-0_42},
year = {2015}
}
Acknowledgements
Partially supported by NSF award CCF 1346756 and a Microsoft Research SEIF award.