Программный синтез на Rust и Z3: как заставить компьютер писать код за вас

Synthesizing Loop-Free Programs with Rust and Z3 (2020)

Автор объясняет синтез программ без циклов на основе компонентов с использованием Rust и SMT-солвера Z3. Он разбирает формализацию задачи, метод CEGIS с контрпримерами и реализацию, но признаёт, что для сложных бенчмарков синтезатор не находит решение за разумное время. Статья будет полезна как новичкам, так и специалистам, которые могут помочь с производительностью.