Поддержу.

топ 100 блогов thesz24.04.2010 http://lambda-the-ultimate.org/node/3858#comment-59775 - ссылка на комментарий одного из разработчиков seL4, формально верифицированного ядра, реализующего интерфейс L4.

Там есть ссылка на разные работы по теме и, в частности, на исходники на Isabelle/HOL формального описания семантики подмножества C.

Говоря словами одного из героев Неуловимых Мстителей, "много, много!"

И страшно, настолько многословно.

PS
До чего, всё же, разный синтаксис у разных инструментов. Один, вроде, поверхностно знаешь, но в другом ни в зуб ногой.

Оставить комментарий

Архив записей в блогах:
Хмурым весенним вечером решилась я на адское варево. Поначалу ничего дурного не предвещало. Чтоб не промахнуться в рецептуре загодя купила пакеты для начинающих глинтвейноваров. В теплое винище спустила содержимое кулька. Поварила, настояла. В бокал плеснула. Дааааа. Не только ...
В музеи, увы, ходят далеко не все туристы, приезжающие во Францию, не говоря уже о местных жителях, - как правило, "родные" достопримечательности люди посещают с меньшей охотой, чем зарубежные. А проехавшись в таком арт-поезде, осмотрев со всех сторон вагон-"Версаль", ...
Вот что странно - чисто с железячной точки зрения. Со старым УПСом, в котором вздулся аккумулятор, а сам стал трещать при включении, очинно гудел системный блок. Кулеры напрягались, разгонялись с воем, входили в резонанс... Стукнешь по верхней крышке - вроде, притихли. А потом снова... И ...
Сегта, тут на Авву постукивать начал лесной дятел. Если кто что хочет сказать, ...
Оригинал взят у rt_russian в Украинская армия призвала Виктора Януковича срочно принять меры для стабилизации ситуации в стране Офицеры армии Украины призвали президента страны Виктора Януковича как главнокомандующего «принять безотлагательные меры для стабилизации ситуации в ...