OberonCore

Возник вопрос по эквивалентным преобразованием программ (Alexey_Donskoy).

Пусть пока здесь будет.

По теории схем программ:

В.Е. Котов, В.К. Сабельфельд. Теория схем программ.
http://ermakov.metasystems.ru/forum/boo ... Kotov.djvu

М.А. Князева, С.К. Клещев "Концепция банка знаний в области оптимизации программ..."
http://www.iacp.dvo.ru/is/publications.php?pub_id=101

Можно поискать другие современные публикации в окрестности сайтов ИСИ СО РАН (iis.nsk.su).

Конечно же, работы А.П. Ершова "Введение в теоретическое программирование", "Теория программирования и вычислительные системы". Если не лезть дальше в область смешанных вычислений и суперкомпиляции (проекции Футамуры-Ершова...)
Эти и многие другие работы - на http://www.ershov.ras.ru

Кларк Э.М., Грамберг О., Пелед Д.
Верификация моделей программ: Model Checking. Пер. с англ. / под ред. Р. Смелянского. - М.: МЦНМО, 2002.- 416 с.

Книга по семейству языков-методов формальной спецификации LARCH:

http://www.cs.cmu.edu/afs/cs/usr/wing/w ... chBook.pdf

Внимание!
Вышла книга Карпова Ю.Г. по Model Checking.

Карпов Ю.Г. Model Checking. Верификация параллельных и распределенных программных систем. - СПб.: БХВ-Петербург, 2010. - 560 с. + CD ROM

Судя по предисловию и первым главам - самое то для систем реального времени.

Получил книгу. Интересно, написано хорошим языком. Буду постепенно знакомиться

Потом сообщите о её полезности.

Презентация Н.Н. Непейводы
"Ограничения открытого софта", с обращением к вопросам доказательства программ
http://freeschool.altlinux.ru/wp-conten ... llfree.odp

Н.Н. Непейвода "Математик и прикладник: о взаимо(не)понимании"
http://vestnik.udsu.ru/2007/2007-01/vuu_07_01_18.pdf

Тип odp - это из опен-офиса?

Так точно, презентация Open Office Impress.

Ну вот...

А в pdf распечатать?

Сделал:

Он уже наступил...

Спасибо, забавно, но...

Насчет "повышать уровень" -- очевидно.

А остальное про логику -- слегка напоминает характерный синдром (начинающих) учёных: "Я выучил алгебры Ли! Это круто! Теперь я буду их применять!!"

То есть всякие красивые теоремы нужно знать, это здорово и полезно, но полезность не прямолинейная.
------

Но логики в мире и в мире ИТ не хватает.
В этом смысле образовательное усилие у них там хорошее.
Некая концептуальность в системе.
Противовес всеобщему рукосуйству.

Мне срезонировало с собственным опытом (говорил сам практически те же слова) вот это, из "Математика и прикладника":



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

И. Б. Бурдонов, А. С. Косачев, В. В. Кулямин
Теория соответсвия для систем с блокировками и разрушением
М.: ФИЗМАТЛИТ, 2008 . 412 с.

http://panda.ispras.ru/~kuliamin/docs/C ... k-2008.pdf

А не будет небольшого резюме, почему её стоит прочитать?

Аналогичный вопрос возник и у меня.

Книгу смотреть подробно было некогда.

Про практическую деятельность авторов только знаю. С А.С. Косачевым на одном семинаре общались, он рассказывал. Центр верификации и сертификации Линуха у них там.

Разве не Явы?