Содержание
Оригинальные статьи
| От редакторов специального выпуска | |
| В. А. Непомнящий, В. А. Соколов | 5-6 |
| Типовые примеры использования языка Atoment | PDF (Rus) |
| Игорь Сергеевич Ануреев | 7-20 |
| Атрибутные аннотации и их применение в дедуктивной верификации C-программ | PDF (Rus) |
| Михаил Михайлович Атучин, Игорь Сергеевич Ануреев | 21-33 |
| Построение приближений бисимуляции в односчетчиковых сетях | PDF (Rus) |
| Владимир Анатольевич Башкин | 33-44 |
| Статический анализ с использованием систем типов и эффектов на основе LLVM | PDF (Rus) |
| Михаил Анатольевич Беляев, Вадим Александрович Цесько | 45-55 |
| Оптимизационные процедуры в аффинной проверке моделей | PDF (Rus) |
| Наталья Олеговна Гаранина | 56-67 |
| Использование зависимостей для повышения точности статического анализа программ | PDF (Rus) |
| Михаил Игоревич Глухих, Владимир Михайлович Ицыксон, Вадим Александрович Цесько | 68-79 |
| Ингибиторная сеть Петри, выполняющая произвольный заданный нормальный алгорифм Маркова | PDF (Rus) |
| Дмитрий Анатольевич Зайцев | 80-93 |
| Автоматическое обнаружение ошибок конкурентной модификации данных в моделях на языке SystemC | PDF (Rus) |
| Алексей Владимирович Захаров, Михаил Юрьевич Моисеев | 94-105 |
| Простой алгоритм решения задачи покрытия для монотонных счетчиковых систем | PDF (Rus) |
| Андрей Валентинович Климов | 106-117 |
| Формальная модель требований, используемая в процессе генерации кода приложения и кода тестов | PDF (Rus) |
| Сергей Николаевич Баранов, Всеволод Павлович Котляров | 118-130 |
| Верификация Си-программ: объяснение условий корректности и стандартная библиотека | PDF (Rus) |
| Алексей Владимирович Промский | 157-167 |
| Верификация шаблонов алгоритмов для метода отката и метода ветвей и границ | PDF (Rus) |
| Николай Вячеславович Шилов | 168-180 |
