Найти в Дзене
Раньше ведь как было: изучаешь теорию языков программирования и формальные методы, формальные грамматики, лексический и синтаксический
анализ, работу c AST (обход дерева, трансформация), атрибутные грамматики и синтезируемые/наследуемые атрибуты, изучаешь системы типов, семантику программ, чтобы понимать, что означает программа, изучаешь межпроцедурный анализ. Изучаешь алгоритмы статического анализа: анализ потоков данных и анализ потоков управления, абстрактную интерпретацию, ML для статического анализа, изучаешь реализации SOTA статических анализаторов с открытым исходным кодом (вроде ничего не забыл). И через несколько лет вы может быть разработаете статический анализатор, который будет находить проблемы в популярных проектах с высоким уровнем качества кода...
1 неделю назад
Поиск точек разладки (changepoint) это популярная задача в разных областях
Это канал про тестирование ПО, поэтому ограничимся поиском точек разладки при анализе результатов тестирования производительности. В отличие от функционального тестирования результаты тестов производительности нужно постоянно анализировать и выявлять причины отклонений результатов, в некоторых компаниях этим занимаются отдельные команды (Андрей Акиньшин работе такой команды целую книжку посвятил, рекомендую к прочтению). Но если выделенной команды нет, а тестировать производительность всё еще хочется, то можно использоваться математические методы для анализа результатов. Не буду рассказывать, что задача поиска точек разладки непростая, Андрей Акиньшин это уже сделал...
1 месяц назад
После анонса задачи про верификацию оптимизаций в LuaJIT в лаборатории Tarantool мне написал студент Физтеха Алексей и сказал, что хочет
взять эту задачу в качестве дипломной работы и с сентября прошлого года мы продолжаем делать верификатор для LuaJIT. Много успели сделать и есть результаты, которыми можно поделиться. Напомню основную идею - научиться моделировать семантику LuaJIT IR с помощью SMT-LIB, декларативного LISP-подобного языка для SMT-солверов, и тем самым получить возможность проверять эквивалентность программы, представленной в виде LuaJIT до и после оптимизаций. В отличие от сравнительного тестирования верификация с помощью SMT-решателя позволяет проверить корректность на всех допустимых входах, а не только на конкретных тестовых данных...
1 месяц назад
Если нравится — подпишитесь
Так вы не пропустите новые публикации этого канала