LINUX.ORG.RU
ФорумJob

математик-верификатор (Москва)

 


2

4

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

Обязанности:

  • Построение моделей программ,
  • Формальная верификация кода, протоколов, интерфейсов,
  • Доказательство корректности реализации.

Требования:

  • Владение различными методами и инструментами верификации, в частности Isabelle/HOL
  • Опыт верификации ПО, например драйверов, протоколов
  • Навыки программирования на функциональных и/или процедурных языках
  • Научные публикации в реферируемых журналах

Условия:

  • Официальная заработная плата (после вычета налогов) – от 90 000, определяется по результатам собеседования;
  • Индексация заработной платы;
  • 13-ая зарплата" по итогам работы за год;
  • Опытный коллектив, широкие возможности профессионального роста;
  • Возможность повышения квалификации на различных курсах;
  • Возможность посещения тематических конференций в России и за рубежом;
  • Добровольное медицинское страхование (санчасть в 5 мин. пешком от работы);
  • Членство в спортивном клубе в 10 мин. пешком от работы;
  • Соблюдение ТК;
  • Офис в районе м. Марьина Роща

ВНИМАНИЕ! Вместе с откликом присылайте, пожалуйста, примеры верифицированного вами кода/моделей. Для связи - sartakov@ksyslabs.org Рассматриваются кандидаты только с релевантным опытом. Студенты - можем рассмотреть, но хотелось бы профессионала. Удаленка точно нет.

Ответ на: комментарий от four_str_sam

поднимаем наши разработки на качественно новый уровень

По-моему, проекту будет лучше от повышения качества для любой предметной области. Вне зависимости от того, «что».

Infra_HDC ★★★★★
()
Ответ на: комментарий от Infra_HDC

Я тоже думаю так. Потому что верификация и преобразования схем - это чрезвычайно высокий уровень для обычных выпускников. А брать дфмн или кфмн со стажем в обычную фирму - нереентабельно. Даже если цели позволят. Методы конструктивной математики [суть инженерного подхода в программировании] - продуктивнее в целом обычно, чем аналитические.

pacify ★★★★★
()
12 марта 2015 г.

Ну я занимался верификацией на диплом (с недопаскаля в ACL2 конвертил и верифицировал там) и потом немного возился с dependent typами. Но всякие языки типа agda неудобны, idris жутко бажный, coq слишком старомоден. К Isabelle/HOL планировал приступить, но както мотивации не хватало. Жаль только времени потребуется, ну пару месяцев точно. Увлекающийся и специалист - разные люди.

Так что вопрос, есть ли еще надобность в сей специальности или всё, тут наняли, а больше подобного нету?

q0tw4 ★★★★
()
Последнее исправление: q0tw4 (всего исправлений: 1)
17 апреля 2015 г.

Поспрашивай ещё на сайтах пользователей ЧПУ станков.
cnc-club.ru ; mir-cnc.ru

Математика там скорее всего не окажется,но очень много «деклассировавшихся» квалифицированных специалистов, Правда им за сорок-пятьдесят со всеми недостатками этого возраста

torvn77 ★★★★★
()
Последнее исправление: torvn77 (всего исправлений: 1)
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.