• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • A
  • A
  • A
  • A
  • A
Обычная версия сайта
  • RU
  • EN
  • HSE University
  • Publications
  • Book chapter
  • By the power of SMT! Mining function contracts to better bounded model checking
  • RU
  • EN
Расширенный поиск
Высшая школа экономики
Национальный исследовательский университет
Priority areas
  • business informatics
  • economics
  • engineering science
  • humanitarian
  • IT and mathematics
  • law
  • management
  • mathematics
  • sociology
  • state and public administration
by year
  • 2028
  • 2027
  • 2026
  • 2025
  • 2024
  • 2023
  • 2022
  • 2021
  • 2020
  • 2019
  • 2018
  • 2017
  • 2016
  • 2015
  • 2014
  • 2013
  • 2012
  • 2011
  • 2010
  • 2009
  • 2008
  • 2007
  • 2006
  • 2005
  • 2004
  • 2003
  • 2002
  • 2001
  • 2000
  • 1999
  • 1998
  • 1997
  • 1996
  • 1995
  • 1994
  • 1993
  • 1992
  • 1991
  • 1990
  • 1989
  • 1988
  • 1987
  • 1986
  • 1985
  • 1984
  • 1983
  • 1982
  • 1981
  • 1980
  • 1979
  • 1978
  • 1977
  • 1976
  • 1975
  • 1974
  • 1973
  • 1972
  • 1971
  • 1970
  • 1969
  • 1968
  • 1967
  • 1966
  • 1965
  • 1964
  • 1963
  • 1958
  • More
Subject
News
September 11, 2026
How to Assess Students Knowledge in the Age of AI
A researcher at HSE University has proposed a flowchart to help lecturers decide how to assess students who use artificial intelligence. It shows where the use of AI should be restricted and where it can be incorporated into the learning process. The article has been published in IT Professional.
September 9, 2026
‘Balkan Hospitality Opens Doors: Studying Dialects on the Verge of Extinction
You cannot study spoken dialects from books. Instead, you need to go to a village, seek out its elders, and earn the trust of local residents before you can record hours of spontaneous stories. This is how Natalia Muravleva, Associate Professor at the Faculty of Humanities, conducts her research. Her internship in Serbia continued her long-standing study of dialects spoken by Macedonian settlers. In this interview, she discusses how diaspora cultural centres help researchers reach informants, why native speakers need to be interviewed only in their own language (otherwise, as she puts it, they may 'break'), and how a single field season helped her finalise her monograph. She also shares warm memories of autumn in Belgrade and of colleagues with whom grammar can be discussed in three languages at once.
September 9, 2026
Scientists Train Neural Network to Generate Process Plans from 3D Models
Researchers at the HSE FCS AI and Digital Science Institute have developed CAD2TechSpec, a framework that converts 3D models of mechanical parts into machining process plans—step-by-step instructions for machine tools. The solution aims to reduce the time required for the design and preparation of technical process documentation in mechanical engineering, aircraft manufacturing, and other high-tech industries. The study findings have been published in PeerJ Computer Science.

 

Have you spotted a typo?
Highlight it, click Ctrl+Enter and send us a message. Thank you for your help!

Publications
  • Books
  • Articles
  • Chapters of books
  • Working papers
  • Report a publication
  • Research at HSE

?

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 checkingsoftware miningFunction contractsFunction summarization

In book

Proceedings of the 5th International Workshop on Software Mining, co-located with ASE 2016
Association for Computing Machinery (ACM), 2016.
Similar publications
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
  • About
  • About
  • Key Figures & Facts
  • Sustainability at HSE University
  • Faculties & Departments
  • International Partnerships
  • Faculty & Staff
  • HSE Buildings
  • HSE University for Persons with Disabilities
  • Public Enquiries
  • Studies
  • Admissions
  • Programme Catalogue
  • Undergraduate
  • Graduate
  • Exchange Programmes
  • Summer University
  • Summer Schools
  • Semester in Moscow
  • Business Internship
  • Research
  • International Laboratories
  • Research Centres
  • Research Projects
  • Monitoring Studies
  • Conferences & Seminars
  • Academic Jobs
  • Yasin (April) International Academic Conference on Economic and Social Development
  • Media & Resources
  • Publications by staff
  • HSE Journals
  • Publishing House
  • iq.hse.ru: commentary by HSE experts
  • Library
  • Economic & Social Data Archive
  • Video
  • HSE Repository of Socio-Economic Information
  • HSE1993–2026
  • Contacts
  • Copyright
  • Privacy Policy
  • Site Map
Edit