Borealis bounded model checker: The coming of age story

M. Akhin

doi:10.1007/978-3-319-67425-4_8

Publications

?

Borealis bounded model checker: The coming of age story

P. 119–138.

Akhin M., Беляев М. А., Ицыксон В. М.

Our research group has been developing a boundedmodel 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. © Springer International Publishing AG 2017.

Language: English

DOI

Text on another site

Keywords: software static analysis bounded model checking

In book

Present and Ulterior Software Engineering

Cham: Springer, 2017.

LLVM-based static analysis tool using type and effect systems

Beliaev Mikhail, Tsesko V., Автоматика и вычислительная техника 2012 Т. 7 № 46 С. 324–330

The intent of this paper is to describe a static analysis tool under development. The main idea behind the design of this tool is to use type and effect systems for static analysis of real programs. The tool uses LLVM bitcode files as input, thus extending the set of analyzed languages to those supported by ...

Added: July 3, 2019

Software defect detection by combining bounded model checking and approximations of functions

Akhin M., Beliaev Mikhail, Itsykson Vladimir, Automatic Control and Computer Sciences 2014 Vol. 7 No. 48 P. 389–397

Added: July 3, 2019

Using a bounded model checker for test generation: How to kill two birds with one SMT solver

Beliaev Mikhail, Petrov M., Gagarski K. et al., Automatic Control and Computer Sciences 2015 Vol. 7 No. 49 P. 466–472

Added: July 3, 2019

Distributed analysis of the BMC kind: Making it fit the tornado supercomputer

Abdullin A., Stepanov D., Akhin M., , in: Communications in Computer and Information ScienceVol. 779: Tools and Methods of Program Analysis.: Springer, 2018. P. 1–10.

Software analysis is becoming increasingly important as a way of software quality assurance. Most works in this area focus their attention on a single machine scenario, when the analysis is run and implemented on a single processing node, as it seems to be a good fit for the current software development methodologies. We argue that ...

Added: November 12, 2018

Random model sampling: Making craig interpolation work when it should not

Akhin M., Kolton S., Ицыксон В. М., Automatic Control and Computer Sciences 2015 Vol. 49 No. 7 P. 413–419

One of the most serious problems when doing program analyses is dealing with function calls. While function inlining is the traditional approach to this problem, it nonetheless suffers from the increase in analysis complexity due to the state space explosion. Craig interpolation has been successfully used in recent years in the context of bounded model ...

Added: November 12, 2018

By the power of SMT! Mining function contracts to better bounded model checking

Abdullin A., Akhin M., , in: Proceedings of the 5th International Workshop on Software Mining, co-located with ASE 2016.: Association for Computing Machinery (ACM), 2016. P. 11–17.

Program analysis is rapidly changing the way we develop software; one of the more important problems is that of function contract creation, as these contracts can greatly increase the quality and performance of the analysis. However, the predominant way of creating function contracts is their manual development by the end-user. In this paper we present ...

Added: November 12, 2018