Abstract
Our research group has been developing a bounded model checker called Borealis for almost 4 years now, and it has been mostly a research prototype with all that it entails. A lot of different ideas have been tested in Borealis, and this chapter draws a bottom line for most of them. We believe this chapter would be of interest to other researchers as a brief introduction to the topic of bounded model checking, and to us as a cornerstone on which to build our future work on making Borealis into a tool.
Access provided by CONRICYT-eBooks. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Akhin, M., Belyaev, M., Itsykson, V.: Improving static analysis by loop unrolling on an arbitrary iteration. Humanit. Sci. Univ. J. 8, 154–168 (2014)
Akhin, M., Belyaev, M., Itsykson, V.: Software defect detection by combining bounded model checking and approximations of functions. Autom. Control. Comput. Sci. 48(7), 389–397 (2014)
Akhin, M., Kolton, S., Itsykson, V.: Random model sampling: making Craig interpolation work when it should not. Autom. Control. Comput. Sci. 49(7), 413–419 (2015)
Armando, A., Mantovani, J., Platania, L.: Bounded model checking of software using SMT solvers instead of SAT solvers. Int. J. Softw. Tools Technol. Transfer 11(1), 69–83 (2009)
Ayewah, N., Hovemeyer, D., Morgenthaler, J.D., Penix, J., Pugh, W.: Experiences using static analysis to find bugs. IEEE Softw. 25, 22–29 (2008)
Bachmann, O., Wang, P.S., Zima, E.V.: Chains of recurrences — a method to expedite the evaluation of closed-form functions. In: ISSAC’94, pp. 242–249 (1994)
Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, vol. 185, pp. 825–885. IOS Press, Amsterdam (2009)
Baudin, P., Filliâtre, J.C., Hubert, T., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C Specification Language. Preliminary Design, version 1.4, 2008, preliminary edn. (2008)
Belyaev, M., Itsykson, V.: Fast and safe concrete code execution for reinforcing static analysis and verification. Model. Anal. Inform. Sist. 22, 763–772 (2015)
Berlin, D., Edelsohn, D., Pop, S.: High-level loop optimizations for GCC. In: Proceedings of the 2004 GCC Developers Summit, pp. 37–54 (2004)
Beyer, D.: Status report on software verification. In: TACAS’14, pp. 373–388 (2014)
Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: TACAS’99, pp. 193–207 (1999)
Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: VMCAI’06, pp. 427–442 (2006)
Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R.: The MathSAT 4 SMT solver. In: CAV’08, pp. 299–303 (2008)
Buckland, M., Gey, F.: The relationship between recall and precision. J. Am. Soc. Inf. Sci. 45(1), 12–19 (1994)
Calcagno, C., Distefano, D., Dubreil, J., et al.: Moving fast with software verification. NASA Formal Methods, pp. 3–11. Springer, Cham (2015)
Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003)
Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: TACAS’04, pp. 168–176 (2004)
Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ANSI-C software. In: ASE’09, pp. 137–148 (2009)
Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Log. 22(3), 269–285 (1957)
Dan, A.M., Meshman, Y., Vechev, M., Yahav, E.: Predicate abstraction for relaxed memory models. Static Analysis, pp. 84–104. Springer, Berlin (2013)
de Berg, M., Cheong, O., van Kreveld, M., Overmars, M.: Computational Geometry: Algorithms and Applications. Springer, Berlin (2008)
De Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: TACAS’08, pp. 337–340 (2008)
Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: POPL’02, pp. 191–202 (2002)
Fratantonio, Y., Machiry, A., Bianchi, A., Kruegel, C., Vigna, G.: CLAPP: characterizing loops in android applications. In: DeMobile 2015, pp. 33–34 (2015)
Grosser, T.C.: Enabling polyhedral optimizations in LLVM. Doctoral dissertation (2011)
McMillan, K.L.: Applications of Craig interpolants in model checking. In: TACAS’05, pp. 1–12 (2005)
Merz, F., Falke, S., Sinz, C.: LLBMC: Bounded model checking of C and C++ programs using a compiler IR. In: VSTTE’12, pp. 146–161 (2012)
Petrov, M., Gagarski, K., Belyaev, M., Itsykson, V.: Using a bounded model checker for test generation: how to kill two birds with one SMT solver. Autom. Control. Comput. Sci. 49(7), 466–472 (2015)
Regehr, J.: A guide to undefined behavior in C and C++, part 1. http://blog.regehr.org/archives/213. Accessed 24 July 2017
Sery, O., Fedyukovich, G., Sharygina, N.: Interpolation-based function summaries in bounded model checking. In: HVC’11, pp. 160–175 (2012)
van Engelen, R.: Symbolic evaluation of chains of recurrences for loop optimization. Technical Report (2000)
Wang, X., Chen, H., Cheung, A., et al.: Undefined behavior: what happened to my code? In: APSYS’12, pp. 9:1–9:7 (2012)
Acknowledgements
We would like to thank Bertrand Meyer for organizing the PAUSE conference and all who decided to spend their precious time reading this chapter.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this chapter
Cite this chapter
Akhin, M., Belyaev, M., Itsykson, V. (2017). Borealis Bounded Model Checker: The Coming of Age Story. In: Mazzara, M., Meyer, B. (eds) Present and Ulterior Software Engineering. Springer, Cham. https://doi.org/10.1007/978-3-319-67425-4_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-67425-4_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-67424-7
Online ISBN: 978-3-319-67425-4
eBook Packages: Computer ScienceComputer Science (R0)