Немного информации в дополнение к Робу
Инструмент для нарезки программ в Висконсине превратился в инструмент под названием CodeSurfer. Хорошие новости: он коммерчески доступен и поддерживается, и он отлично работает для того, что он делает. Плохая новость (возможно): на самом деле она не создает сокращенную программу, которая вычисляет то же значение, которое вы выбрали, но это очень удобно для навигации по исходному коду, который вы не написали.
Frama-C обрабатывает только C (без C ++ в обозримом будущем). Это хорошо, но не очень хорошо для навигации по исходному коду, но может создать эквивалентную меньшую программу по заданному вами критерию, если исходная программа того типа, которую она может анализировать автоматически (без рекурсии, нет динамического распределения). Frama-C является открытым исходным кодом и имеет список рассылки, в котором будут приветствоваться ваши вопросы, если вы заинтересованы в методах, которые он использует.
Причина, по которой CodeSurfer не рискует создавать собственную эквивалентную программу, а Frama-C может делать это только для кода со встроенными подобными ограничениями, заключается в том, что для этого требуется знание значений указателей, что может быть сколь угодно сложным вычислить с точностью.