← В ленту
Middle
Регистрация: 11.01.2024

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

Специализация: Proof engineer / Ocaml / Rust / Full-stack web-developer
Специалист по формальной верификации, формальным методам. Coq, математические методы формальной верификации. Формальная верификация Ocaml кода (работаю с автоматическим переводчиком кода Ocaml на Coq, затем провожу формальную верификацию) Программист, разработчик (Ocaml, Rust, full-stack web-developer, базы данных)
Специалист по формальной верификации, формальным методам. Coq, математические методы формальной верификации. Формальная верификация Ocaml кода (работаю с автоматическим переводчиком кода Ocaml на Coq, затем провожу формальную верификацию) Программист, разработчик (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
OCaml
Python
PHP
Javascript
Rust
Formal verification
Postgresql
mySQL
PostgreSQL

Опыт работы

Специалист по формальной верификации / Программист
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
ЮФУ, Факультет Высоких Технологий

Языки

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