• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • A
  • A
  • A
  • A
  • A
Обычная версия сайта
  • RU
  • EN
  • Национальный исследовательский университет «Высшая школа экономики»
  • Публикации ВШЭ
  • Статьи
  • Using a bounded model checker for test generation: How to kill two birds with one SMT solver
  • RU
  • EN
Расширенный поиск
Высшая школа экономики
Национальный исследовательский университет
Приоритетные направления
  • бизнес-информатика
  • государственное и муниципальное управление
  • гуманитарные науки
  • инженерные науки
  • компьютерно-математическое
  • математика
  • менеджмент
  • право
  • социология
  • экономика
по году
  • 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
  • еще
Тематика
Новости
18 мая 2026 г.
В Вышке прошла XXX юбилейная научно-техническая конференция имени Е.В. Арменского
Организатором научного события выступает Московский институт электроники и математики им. А.Н. Тихонова ВШЭ. В этом году главный инженерный студенческий форум проходил 30-й раз и собрал рекордное число участников. Студенты, аспиранты и молодые специалисты из 50 вузов и организаций России представили научно-исследовательские доклады в ИТ-области. Отдельная секция была посвящена научно-исследовательским работам школьников.
15 мая 2026 г.
В НИУ ВШЭ разрабатывают нейросеть для сферы науки и инноваций
Исследователи НИУ ВШЭ учат большие языковые модели понимать русскоязычную научную терминологию, увеличивая при этом их энергоэффективность. Адаптированная модель работает в 2,7 раза быстрее и требует на 73% меньше памяти, чем исходная открытая модель, что позволяет запускать ее на более доступном оборудовании. Программа прошла государственную регистрацию.
15 мая 2026 г.
Стартовал совместный спецпроект бренд-медиа Вышки IQ Media и iFORA ИСИЭЗ
В мае 2026 года стартовал научно-популярный проект «Искусственный интеллект: технологии, данные и будущее», который стал результатом работы двух команд — проекта iFORA Института статистических исследований и экономики знаний НИУ ВШЭ и редакции бренд-медиа IQMedia. Медийно-аналитический спецпроект посвящен современному развитию искусственного интеллекта и аналитике больших данных.

 

Нашли опечатку?
Выделите её, нажмите Ctrl+Enter и отправьте нам уведомление. Спасибо за участие!

Публикации
  • Книги
  • Статьи
  • Главы в книгах
  • Препринты
  • Верификация публикаций
  • Расширенный поиск
  • Правила использования материалов
  • Наука в ВШЭ

?

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

Automatic Control and Computer Sciences. 2015. Vol. 7. No. 49. P. 466–472.
Beliaev Mikhail, Petrov M., Gagarski K., Itsykson V.M.
Приоритетные направления: компьютерно-математическое
Язык: английский
DOI
Ключевые слова: проверка моделейdynamic symbolic executionbounded model checkingproperty testing
Похожие публикации
Natural hazard database from Internet publications: text mining with a large language model
Деркачева А. А., Сакиркина М. А., Краев Г. Н. и др., /. 2026.
Добавлено: 28 апреля 2026 г.
Ising models on the hydrogen peroxide and other lattices
Qin X., Deng Y., Щур Л. Н. и др., / Series arXiv "math". 2026. No. 2603.02962.
Добавлено: 20 апреля 2026 г.
Algorithmic overlaps as thermodynamic variables: from local to cluster Monte Carlo dynamics in critical phenomena
Пиле Я. Э., Deng Y., Щур Л. Н., / Series arXiv "math". 2026. No. 2604.10254.
Добавлено: 20 апреля 2026 г.
Using predefined vector systems to speed up neural network multimillion class classification
Gabdullin N., Андросов И. А., / Series Computer Science "arxiv.org". 2026.
Добавлено: 2 апреля 2026 г.
Iterative Ricci-Foster Curvature Flow with GMM-Based Edge Pruning: A Novel Approach to Community Detection
Сорокин К. С., Бекетов М. Е., Онучин А. и др., / arxiv.org. Серия cs.SI "Social and Information Networks ". 2025.
Обнаружение сообществ в сложных сетях — фундаментальная проблема, открытая для новых подходов в различных научных областях. Мы представляем новый метод обнаружения сообществ, основанный на потоке Риччи на графах. Наша техника итеративно обновляет веса ребер (их метрические длины) в соответствии с их (комбинаторной) версией кривизны Риччи Фостера, вычисленной на основе эффективного расстояния сопротивления между узлами. Известно, ...
Добавлено: 15 января 2026 г.
Implementing Transport Coding in OMNeT++ for Message Delay Reduction
Петрованов И. С., Сергеев А. В., / Series Computer Science "arxiv.org". 2025. No. 2512.18332.
Добавлено: 24 декабря 2025 г.
Hessian-based lightweight neural network for brain vessel segmentation on a minimal training dataset
Меньшиков И. А., Бернадотт А. К., Елфимов Н. С., / Series arXie "Statistical mechanics". 2025.
Добавлено: 1 декабря 2025 г.
Determining the boundary of dynamical chaos in the generalized Chirikov map via machine learning
Чернышов Д. П., Сатанин А. М., Щур Л. Н., / Series arXiv "math". 2025.
Добавлено: 21 ноября 2025 г.
Эффективный алгоритм торговли на фондовом рынке: ретроспективный анализ, основанный на данных по S&P-500.
Рубчинский А. А., Чубарова Д. А., / Series WP7 "Математические методы анализа решений в экономике, бизнесе и политике". 2025. No. WP7/2025/01.
Добавлено: 9 ноября 2025 г.
Diffusion on language model embeddings for protein sequence generation
Мещанинов В. П., Strashnov, P., Shevtsov A. и др., / Cornell University. Серия CoRR, arXiv:2403.03726 "Computing Research Repository,". 2025.
Дизайн белков требует глубокого понимания присущей сложности «белкового вселенной». Хотя многие работы ориентируются на условную генерацию или сосредоточены на отдельных семействах белков, базовая задача безусловной генерации остаётся недостаточно изученной и недооценённой. В этой работе мы исследуем именно этот ключевой аспект и представляем DiMA — модель, которая использует непрерывную диффузию по эмбеддингам, полученным из языковой модели для белков ESM-2, ...
Добавлено: 5 октября 2025 г.
Smoothie: Smoothing Diffusion on Token Embeddings for Text Generation
Шабалин А. М., Мещанинов В. П., Vetrov D., / Series cs.CL, arXiv:2505.18853 "Computation and Language". 2025.
Диффузионные модели достигли передовых результатов в генерации изображений, аудио и видео, однако их адаптация к тексту остаётся сложной из-за его дискретной природы. Ранее подходы либо применяют гауссовскую диффузию в непрерывных латентных пространствах, что наследует семантическую структуру, но затрудняет декодирование токенов, либо работают в пространстве категориального симплекса, что учитывает дискретность, но игнорирует семантические связи между токенами. ...
Добавлено: 5 октября 2025 г.
A Feature Engineering Framework for Computer Vision Based on Topological Data Analysis
Абрамов А. С., Чернышев В. Л., Михайлец Е. В. и др., / Series Social Science Research Network "Social Science Research Network". 2025.
Добавлено: 23 сентября 2025 г.
On the construction of frieze patterns from partitions of convex polygons by nonintersecting diagonals
Кочетков Ю. Ю., / Series arXiv.org e-print archive "arXiv.math". 2025. No. 07600.
Добавлено: 17 сентября 2025 г.
On one property of Catalan numbers
Кочетков Ю. Ю., / Series arXiv.org e-print archive "arXiv.math". 2025. No. 20584.
Добавлено: 9 сентября 2025 г.
InnoChain: распределенный реестр для индустриального применения с формальной верификацией на всех уровнях реализации
Кухаренко В. А., Зиборов К. В., Садыков Р. Ф. и др., Моделирование и анализ информационных систем 2020 Т. 27 № 4 С. 454–471
Степень применения методов формальной верификации в индустриальных проектах всегда была ограничена. Распространение систем распределенного реестра (СРР), известных также как блокчейн, быстро меняет ситуацию. Поскольку основной областью применения СРР является автоматизация финансовых транзакций, свойства предсказуемости и надежности являются критическими при реализации таких систем. Реальное поведение СРР определяется выбранным протоколом консенсуса, свойства которого нуждаются в строгой спецификации ...
Добавлено: 31 мая 2021 г.
Software defect detection by combining bounded model checking and approximations of functions
Ахин М. Х., Beliaev Mikhail, Itsykson Vladimir, Automatic Control and Computer Sciences 2014 Vol. 7 No. 48 P. 389–397
Добавлено: 3 июля 2019 г.
Distributed analysis of the BMC kind: Making it fit the tornado supercomputer
Abdullin A., Stepanov D., Ахин М. Х., , in: Communications in Computer and Information ScienceVol. 779: Tools and Methods of Program Analysis.: Springer, 2018. P. 1–10.
Добавлено: 12 ноября 2018 г.
Random model sampling: Making craig interpolation work when it should not
Ахин М. Х., Kolton S., Ицыксон В. М., Automatic Control and Computer Sciences 2015 Vol. 49 No. 7 P. 413–419
Добавлено: 12 ноября 2018 г.
By the power of SMT! Mining function contracts to better bounded model checking
Abdullin A., Ахин М. Х., , in: Proceedings of the 5th International Workshop on Software Mining, co-located with ASE 2016.: Association for Computing Machinery (ACM), 2016. P. 11–17.
Добавлено: 12 ноября 2018 г.
Borealis bounded model checker: The coming of age story
Ахин М. Х., Беляев М. А., Ицыксон В. М., , in: Present and Ulterior Software Engineering.: Cham: Springer, 2017. P. 119–138.
Добавлено: 12 ноября 2018 г.
Введение в формальные методы верификации программ: учебное пособие
Камкин А. С., М.: МАКС Пресс, 2018.
Книга является учебным пособием по формальным методам верификации программ и основана на курсах лекций, читаемых автором на факультете ВМК МГУ имени М.В. Ломоносова, ФУПМ МФТИ и ФКН ВШЭ. В ней изложены основы таких подходов, как дедуктивный анализ и проверка моделей. Список тем включает: методы формализации семантики языков программирования (операционная и аксиоматическая семантика), методы формальной спецификации ...
Добавлено: 2 ноября 2018 г.
Dynamic detection of use after free bugs
Asryan S. A., Гайсарян С. С., Kurmangaleev S. F. и др., Proceedings of the Institute for System Programming of the RAS 2018 Vol. 30 No. 3 P. 7–20
The article describes new method of use after free bug detection using program dynamic analysis. In memory-unsafe programming languages such as C/C++ this class of bugs mainly accurse when program tries to access specific area of dynamically allocated memory that has been already freed. This method is based on combination of two basic components. The ...
Добавлено: 10 августа 2018 г.
Об интеграции формальных методов в задачах верификации операционных систем
Петренко А. К., Кулямин В. В., Хорошилов А. В., Труды Института системного программирования РАН 2015 Т. 27 № 5 С. 175–190
В данной работе ставится задача разработки методов качественной верификации операционных систем, перспективным подходом к решению которой является интеграция различных техник верификации. Результатом успешного решения этой задачи может считаться комбинация методов верификации, которая позволяет проверить всю систему в целом и при этом более тщательно верифицировать наиболее важные ее компоненты и функции, используя для этого более строгие ...
Добавлено: 28 августа 2017 г.
Верификация и анализ вариабельных операционных систем
Кулямин В. В., Лаврищева Е. М., Мутилин В. С. и др., Труды Института системного программирования РАН 2016 Т. 28 № 3 С. 189–208
В данной работе рассматриваются проблемы верификации и анализа сложных операционных систем с учетом их вариабельности, или наличия большого количества разнообразных конфигураций. Исследуются методы, позволяющие преодолеть эти проблемы, проводится их обзор и классификация. Выделены классы методов, использующих для анализа инструменты, не учитывающие вариабельность, и выборки вариантов системы и методов, использующих специализированные инструменты, учитывающие вариабельность. Как наиболее ...
Добавлено: 28 августа 2017 г.
  • О ВЫШКЕ
  • Цифры и факты
  • Руководство и структура
  • Устойчивое развитие в НИУ ВШЭ
  • Преподаватели и сотрудники
  • Корпуса и общежития
  • Закупки
  • Обращения граждан в НИУ ВШЭ
  • Фонд целевого капитала
  • Противодействие коррупции
  • Сведения о доходах, расходах, об имуществе и обязательствах имущественного характера
  • Сведения об образовательной организации
  • Людям с ограниченными возможностями здоровья
  • Единая платежная страница
  • Работа в Вышке
  • ОБРАЗОВАНИЕ
  • Лицей
  • Довузовская подготовка
  • Олимпиады
  • Прием в бакалавриат
  • Вышка+
  • Прием в магистратуру
  • Аспирантура
  • Дополнительное образование
  • Центр развития карьеры
  • Бизнес-инкубатор ВШЭ
  • Образовательные партнерства
  • Обратная связь и взаимодействие с получателями услуг
  • НАУКА
  • Научные подразделения
  • Исследовательские проекты
  • Мониторинги
  • Диссертационные советы
  • Защиты диссертаций
  • Академическое развитие
  • Конкурсы и гранты
  • Внешние научно-информационные ресурсы
  • РЕСУРСЫ
  • Библиотека
  • Издательский дом ВШЭ
  • Книжный магазин «БукВышка»
  • Типография
  • Медиацентр
  • Журналы ВШЭ
  • Публикации
  • http://www.minobrnauki.gov.ru/
    Министерство науки и высшего образования РФ
  • https://edu.gov.ru/
    Министерство просвещения РФ
  • http://www.edu.ru
    Федеральный портал «Российское образование»
  • https://elearning.hse.ru/mooc
    Массовые открытые онлайн-курсы
  • НИУ ВШЭ1993–2026
  • Адреса и контакты
  • Условия использования материалов
  • Политика конфиденциальности
  • Правила применения рекомендательных технологий в НИУ ВШЭ
  • Карта сайта
Редактору