Коне́чный автома́т (КА) в теории алгоритмов — математическая абстракция, модель дискретного устройства, имеющего один вход, один выход и в каждый момент времени находящегося в одном состоянии из множества возможных. Является частным случаем абстрактного дискретного автомата, число возможных внутренних состояний которого конечно.
Тести́рование програ́ммного обеспе́че́ния — процесс исследования, испытания программного продукта, имеющий своей целью проверку соответствия между реальным поведением программы и её ожидаемым поведением на конечном наборе тестов, выбранных определённым образом.
Верифика́ция в различных сферах деятельности человека может подразумевать:
- подтверждение того, что заданные требования выполнены, через предоставление объективных свидетельств;
- оценка соответствия продукта, услуги или системы нормам, требованиям, спецификациям или установленным условиям;
- проверка, подтверждение, метод доказательств каких-либо теоретических положений, алгоритмов, программ и процедур путём их сопоставления с опытными данными, алгоритмами и программами;
- методика распознавания на соответствие правде;
- в науке, проверка теоретических положений на соответствие реальности при помощи эксперимента.
Switch-технология — технология разработки систем логического управления на базе конечных автоматов, охватывающая процесс спецификации, проектирования, реализации, отладки, верификации, документирования и сопровождения. Предложена А. А. Шалыто в 1991 году.
Язык спецификаций — формальный язык, предназначенный для декларативного описания структуры, связей, свойств данных и способов их преобразований, без явного упоминания порядка выполняемых действий и использования конкретных значений данных.
Формальная верификация или формальное доказательство — формальное доказательство соответствия или несоответствия предмета верификации его формальному описанию. Предметом выступают алгоритмы, программы и другие доказательства.
Дескрипцио́нная логика — язык представления знаний, позволяющий описывать понятия предметной области в недвусмысленном, формализованном виде, организованный по типу языков математической логики. Дескрипционные логики сочетают, с одной стороны, богатые выразительные возможности, а с другой — хорошие вычислительные свойства, такие как разрешимость и относительно невысокая вычислительная сложность основных логических проблем, что делает возможным их применение на практике, обеспечивая компромисс между выразительностью и разрешимостью. Могут быть рассмотрены как разрешимые фрагменты логики предикатов, синтаксически же они близки к модальным логикам.
Линеаризу́емость — свойство программной системы, при котором результат любого параллельного выполнения (операций) эквивалентен некоторому последовательному выполнению. Для любого другого потока выполнение линеаризуемой операции является мгновенным: операция либо не начата, либо завершена. Применяется как в многопоточном программировании, так и в распределённых системах.
UniTESK — технология тестирования программного и аппаратного обеспечения на основе формальных спецификаций, разработанная в Институте системного программирования РАН. Технология представляет собой сочетание хорошо зарекомендовавших себя техник, которые могут применяться в различных комбинациях, взаимно сочетаясь и усиливая друг друга. Это делает технологию гибкой и настраиваемой под существующие процессы разработки на всех этапах жизненного цикла разработки программного обеспечения от сбора и анализа требований до сопровождения.
Темпоральная логика — логика, в высказываниях которой учитывается временной аспект. Используется для описания последовательностей явлений и их взаимосвязи по временной шкале.
Модель Крипке — это один из вариантов недетерминированного конечного автомата, который был предложен Солом Крипке. Этот вид НКА применяется при проверке моделей для представления поведения системы.
Java PathFinder (JPF) — свободный инструмент для проверки многопоточных Java программ. По своей сути это виртуальная Java машина на основе которой реализованы методы проверки моделей. Это означает, что JPF выполняет программу не один раз, как это делает обычная виртуальная машина, а по всем возможным путям, связанным с переключением потоков планировщиком. JPF находит такие ошибки как тупики, необработанные исключения, а также нарушения условий, задаваемых пользователем в виде assert выражений. Кроме того, пользователь может писать специальные слушатели для проверки произвольных свойств. Некоторые из таких слушателей, такие как состояния гонок и ограничения на кучу поставляются вместе с JPF. При нахождении ошибки JPF выводит полную трассу, которая к ней ведет, включая все необходимые переключения планировщика.

В информатике и инженерии программного обеспечения формальными методами называется группа техник, основанных на математическом аппарате для спецификации, разработки и верификации программного и аппаратного обеспечения. Использование формальных методов для проектирования программного и аппаратного обеспечения обусловлено ожиданиями того, что, как и в других инженерных областях, использование математического анализа может существенно поднять надёжность систем. При этом формальные методы довольно сложны, требуют специальной подготовки, временных и ресурсных вложений, и при этом нередко основываются на не всегда достижимых в реальных условиях предположениях. Это приводит к тому, что формальные методы чаще всего находят применение в проектировании высокоточных систем, где важность безопасности оправдывает любые средства.

Astra Linux — операционная система на базе ядра Linux, которая внедряется в России в качестве альтернативы Microsoft Windows в государственных организациях. Обеспечивает степень защиты обрабатываемой информации до уровня государственной тайны «особой важности» включительно. Сертифицирована в системах сертификации средств защиты информации Минобороны РФ, ФСТЭК и ФСБ России. Включена в Единый реестр российских программ Минкомсвязи России.
Estelle — метод формального описания распределённых систем, коммуникационных протоколов, основанный на расширенной конечно-автоматной модели. Разработан и стандартизован ISO для описания протоколов модели OSI. Раздельно определяет как общую архитектуру распределённой системы, так и поведение отдельных компонентов. Использует синтаксис стандартного языка Паскаль.
Логика разделения, сепарационная логика — формальная система, субструктурная логика, применимая к верификации программ, содержащих изменяемые структуры данных и указатели, расширение логики Хоара. Разработана Джоном Рейнольдсом, Питером О’Хирном, Самином Иштиаком и Хонсёком Яном на основе работ Рода Бёрстола. Язык утверждений логики разделения является специальным случаем логики пучковых импликаций.
Формальная верификация криптографических протоколов — проверка криптографических протоколов на обеспечение требуемых свойств безопасности. Одной из составляющих такой проверки является определение стойкости протокола к атакам в предположении о надёжности криптографических примитивов, на которых он основывается. Для решения этой задачи разработан ряд подходов, основанных на различных формальных методах верификации. Общей чертой формальных методов является использование системного подхода к проблеме, позволяющего выполнять более обоснованную, точную и эффективную проверку свойств безопасности протокола.
Взаимодействующие последовательные процессы — формальный язык для описания моделей взаимодействия в параллельных системах. Относится к математическим теориям параллелизма, известных как исчисление процессов, основанных на передаче сообщений по каналам. Оказал влияние на разработку языков Оккам, Limbo, Go.
В информатике переписывание графов — техника по созданию нового графа из исходного графа алгоритмическим образом. Переписывание графов находит широкое применение в компьютерных науках, например, в конструировании программного обеспечения, в верификации программного обеспечения, в генерировании изображений, в компиляторах, в графовых базах данных.

SPARK — формально определённый язык программирования, являющийся подмножеством Ады, предназначен для разработки верифицированного программного обеспечения высокого уровня полноты безопасности. SPARK позволяет создавать приложения, которые обладают предсказуемым поведением и обеспечивают высокую надёжность.