Forums » Программное обеспечение »
Верификация аппаратного обеспечения
Added by betastat over 11 years ago
Добрый день!
На сколько я понял из этого сообщения -- http://habrahabr.ru/post/146865/-- в качестве proof-asstant вы используете Coq.
Можно ли устроиться к вам на работу или стажировку? Дело в том, что я хотел бы изучать Coq и применять эти знания на практике. Сейчас мой опыт работы с Coq не очень большой, но я увлекаюсь функциональным программированием и думаю что смогу осилить и Coq.
Replies (2)
RE: Верификация аппаратного обеспечения - Added by micron_multiclet over 11 years ago
Можно обсудить, приходите в офис, присылайте на почту резюме (контакты на сайте)
RE: Верификация аппаратного обеспечения - Added by m.bakhterev over 11 years ago
betastat. Мы пока Coq-ом не пользуемся, но так как процессор разрабатывается и для ответственных применений, то его формальная верификация была бы полезным делом. Coq - один из инструментов, который активно для этого используется (насколько мне известно), поэтому я его и упомянул. Но там, насколько я понимаю, не совсем функциональный язык, а система исчисления конструкций. Но если Вам интересно в таком разбираться и применять это на практике в деле формальной верификации, то... Вот, Вас уже пригласили :)