Здравствуйте, Paralax, Вы писали:

P>1) Интересует тема <тестирование циклов> — в теории сказано, что цикл разворачивают в линейный код и прогоняют столько раз сколько нужно для выбранного критерия структурного тестирования (C0, C1, C2). Однако, как это выполнить на практике ???
P>2) Необходима информация по формальной верификации. Какие существуют основные концепции кроме аксиоматического метода (пропозиционная алгебра или тройки Хоара) и индуктивных утверждения Флойда? Существуют ли другие механизмы?
P>4) Также интересна тема автоматизации процессов верификации и тестирования!

Если тема ещё актуальна после вашей обширной публикации (как понял тему вы раскопали очень серьёзно), то я бы посоветовал покопаться у нас в it4business.ru по категории "Тестирование ПО": http://it4business.ru/?cat=11

А по автоматизации тестирования лучше в форум:
— functioanl: http://it4business.ru/forum/index.php?showforum=113
— perfomance: http://it4business.ru/forum/index.php?showforum=114

По конкретным тулам также есть форумы и отдельный публикации.