Abstract
We present the software verification tool BLAST 2.7, which we submitted for the Competition on Software Verification. The tool is an improvement over BLAST 2.5, and its development is mostly targeted at its performance and usability in the Linux Driver Verification project.
The paper overviews the tool and outlines our contribution to it.
Chapter PDF
Similar content being viewed by others
References
Henzinger, T.A., Jhala, R., Majumdar, R.: Lazy abstraction. In: Symposium on Principles of Programming Languages, pp. 58–70. ACM Press (2002)
Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker BLAST: Applications to software engineering. Int. J. Softw. Tools Technol. Transf. 9(5), 505–525 (2007)
Fischer, J., Jhala, R., Majumdar, R.: Joining dataflow with predicates. SIGSOFT Softw. Eng. Notes 30, 227–236 (2005)
Khoroshilov, A., Mutilin, V., Novikov, E., Shved, P., Strakh, A.: Towards an open framework for C verification tools benchmarking. In: Proceedings of PSI (2011)
Shved, P., Mutilin, V., Mandrykin, M.: Static verfication “under the hood”: Implementation details and improvements of BLAST. In: Proceedings of SYRCoSE, vol. 1, pp. 54–60 (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Shved, P., Mandrykin, M., Mutilin, V. (2012). Predicate Analysis with BLAST 2.7. In: Flanagan, C., König, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2012. Lecture Notes in Computer Science, vol 7214. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28756-5_39
Download citation
DOI: https://doi.org/10.1007/978-3-642-28756-5_39
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28755-8
Online ISBN: 978-3-642-28756-5
eBook Packages: Computer ScienceComputer Science (R0)