Наталья Клаус

Регистрация: 11.01.2024

Специализация: Proof engineer / Ocaml / Rust / Full-stack web-developer

Портфолио

Формальная верификация исходного кода криптовалюты Tezos

Формальная верификация с помощью Coq и математических методов исходного кода криптовалюты Тезос (https://tezos.com/), а также встроенного языка Michelson, для написания смарт-контрактов

Автоматический перевод кода с Rust на Coq для формальной верификации

Являюсь одним из разработчиков автоматического переводчика с кода Rust на Coq. Код Rust после перевода на Coq верифицируется средствами Coq.

Статьи о формальной верификаци программного кода

Писала статьи о методах формальной верификации исходного кода программ: - Что такое формальная верификация. - Верификация рекурсивных функций в Coq, проблема остановки, горючее. - COQ: верификация функций, содержащих fold_left. - Формальная верификация кода на Coq: тактики.

Скиллы

Coq

Formal verification

Javascript

mySQL

OCaml

PHP

Postgresql

PostgreSQL

Python

Rust

Опыт работы

Специалист по формальной верификации / Программист

12.2021 - 07.2023 |Formal.Land

Coq, Rust, OCaml, Postgresql, Ocaml, Javascript

- Формальная верификация протокола криптовалюты Tezos. - Перевод кода с Rust на Coq для формальной верификации. - Code audit для проекта (Rust). - Писала статьи о формальной верификации исходного кода Тезоса: на русском и английском и много других статей... - Работала как OCaml разработчик. - Разработала на базе фреймворка Dream https://github.com/aantron/dream/, сайт на Postgresql + Ocaml + Javascript. - Последняя часть работы - это еще один сайт, снова на Dream http://nobias.formal.land/KG_main. (Эти оба сайта я сделала за 2 месяца. Дамп базы мне предоставили.) Причина, по которой я ушла из Formal.Land - санкции против Р.Ф.

Full-stack web-developer

03.2010 - 10.2017 |NDA

php, python, java-script, mySQL, postgreSQL

Full-stack web-developer (базы данных, php, python, java-script, mySQL, postgreSQL, интеграция платежных шлюзов, дизайн(html, css, bootstrap)... немного системное администрирование). Основное направление - crowd-funding crowd-investing сайты.

Образование

Аспирант

с 2010 - По настоящий момент

НИИ механики и прикладной математики им. Воровича И.И., ЮФУ

Системный анализ и управление (Магистр)

2001 - 2007

ЮФУ, Факультет Высоких Технологий

Дополнительное образование

Лямбда-исчисления, мат.логика, coq, haskell, idris, функциональные структуры данных, методы формальной верификации

с 10.2020 - По настоящий момент

Повышение квалификации

Языки

АнглийскийВыше среднегоРусскийРодной