> любой другой скажет остановится ли она. Но у нас _одна_ программа
> анализ которой нужно сделать.

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

Во вторых, простая логика подсказывает мне что у мало-мальски больших программ возможно такое большое число состояний, что анализ всех возможных вариантов работы программы займет столько, что рак на горе свистеть устанет, солнце превратится в красный карлик, ну и вообще, когда оно закончится - все это будет уже накому и даром не надо, так что радости то.

> В общем, я имею в виду вот эту технологию:
> https://en.wikipedia.org/wiki/L4_microkernel_family

Ну понятно, очередной академик натирающий мозоли на микроядра.

> (Current research and development) Посмотрите, это может быть интересно.:)

Я уже забыл сколько лет я слышу эту фразу от любителей микроядер. Уже были minix и hurd, etc. У них всех было кое-что общее: они нафиг никому не уперлись на обычных серверах, десктопах и прочем. Знаете, называя вещи своими именами, я тоже могу написать простой тасквичер без багов. Ну это так, если идею микроядра довести до абсолюта. А на баги в остальных компонентах системы сделать козью морду - мол, не мои баги, "это все они".

Правда вот поскольку оборудование, протоколы и софт проще не стали - нет никакого основания ожидать что багов станет меньше. И вообще, не очень понятно как микроядро может помочь в случае лажи в криптографической либе и софте который ей пользовался. Оно конечно замечательно - сватать таблетки от кашля при головной боли. Но эффективность этого метода подвергается сомнениям.

> provides a guarantee that the kernel is free of implementation bugs such as deadlocks,
> livelocks, buffer overflows, arithmetic exceptions or use of uninitialised variables.

Да я тоже простейший тасксвичер напишу без багов. А кому он будет нужен? В общем то единственная проблема с микроядрами: там просто сложные вещи перепихнуты на чуть другие головы, поэтому те кто писал "тасксвичер" могут встать в позу Д'Артаньяна и гордо заявить что у них багов нет. Это вполне может быть правдой, в силу того что само микроядро мелкое. К сожалению это означает лишь то что сложные моменты перепихнули в иные компоненты. И, заметим, про их верификацию все технично молчат в тряпочку. Поэтому секурным оно будет в тепличных условиях, у академиков в лаборатории, где одно лысое ядро которое ничего не делает. А сделай из этого десктопник, с навороченными драйверами и софтом - и будет все как обычно.