дыбр...

[alexott]

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

Comments

[eraplee]

а Haskell для дела учишь или просто интерес?

[alexott]

да я некоторые прототипы на нем стараюсь писать.
кстати, под вашу тему - посмотри на пакет language-c из hackage - может быть полезен для статического анализа кода

[eraplee]

Да не, во-первых, я с Си не работаю вообще, а во-вторых, у нас млин как в армии, чем сказали тем и пользуйся, а импровизация не приветствуется :((

[alexott]

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

[eraplee]

да, некоторые из нас верифицируют С, но я нет.

конечно, плохо, а что делать :((

а ты закончил аспирантуру?

[alexott]

закончил, но не защищался

[alexott]

кстати, а что ты верифицируешь?

[eraplee]

это такая академическая версия распределенной "вычислительной" сети, закос под Flexray (http://en.wikipedia.org/wiki/FlexRay).

Есть имплементация на ML. Имплементация синтезируема в Верилог, т.е. это не совсем сферический конь в вакууме :).

Так вот в Isabelle я должен доказать, что эта имплементация выполнят спецификацию, которая тоже в ML.

прикол всей ферификации в том, что здесь узлы этой сети имеют каждый свой клок, таким образом это уже не просто 1 дигитальная схема, которую можно просто прогнать через мощный модел чеккер, а в игру вступают всякие аналоговые факторы, как например hold & setup times регистра. Т.е. тут уже надо работать не только с дискретным временем, а с реальными числами. Эх геморр еще тот :)

[alexott]

понятно, интересная тема