В докладе будут изложены результаты, полученные в ходе стажировки в Microsoft Research летом/осенью 2010 года под руководством Итана Джексона. Доклад посвящен применению технологий на основе SMT-солверов и машинного обучения к моделированию/автоматической разработке аппаратно-программных co-designs. В ходе стажировки моделировались планировщики ОС реального времени, протоколы передачи данных, драйверы и т.д., запускались полученные модели и собиралась статистика о том, насколько хорошо/плохо та или иная модель работает. Используя эту статистику, алгоритм машинного обучения определял, какие еще модели стоит попробовать. В результате удавалось среди огромного множества вариантов находить очень хорошие архитектуры, и, что самое интересное, автоматически определять, что именно делает их хорошими.