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

Abdullin A.; M. Akhin

doi:10.1145/2975961.2975963

Publications

?

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

P. 11–17.

Abdullin A., Akhin M.

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 an approach which allows one to automatically collect function contracts for bounded model checking by software mining augmented with deep SMT solver integration. The prototype implementation in Borealis bounded model checker has been evaluated on a number of programs and proved its ability to find interesting contracts. © 2016 ACM.

Language: English

DOI

Text on another site

Keywords: bounded model checking software mining Function contracts Function summarization

In book

Proceedings of the 5th International Workshop on Software Mining, co-located with ASE 2016

Association for Computing Machinery (ACM), 2016.

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

Proceedings of the 5th International Workshop on Software Mining, co-located with ASE 2016

Association for Computing Machinery (ACM), 2016.

Added: November 12, 2018

Borealis bounded model checker: The coming of age story

Akhin M., Беляев М. А., Ицыксон В. М., , in: Present and Ulterior Software Engineering.: Cham: Springer, 2017. P. 119–138.

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 ...

Added: November 12, 2018