В настоящее время, когда теоретические основы верификации программ хорошо изучены, исследователи концентрируют свои усилия на предметно-ориентированных методах для различных классов программ. Инструменты, которые они выбирают, варьируются от проверки моделей для сетевых протоколов до исчислений указателей для фрагментов ядра операционной системы. Однако, похоже, что области научных и инженерных программ все еще уделяется недостаточно внимания. Мы хотели бы внести свой вклад в заполнение этого пробела с помощью разработки системы CPPS. Целью этого проекта является создание системы параллельного программирования для Sisal-программ. Дедуктивная верификация Sisal-программ является одной из важных подцелей. Так как язык Cloud-Sisal построен на основе циклических выражений, их аксиоматическая семантика является базой логики Хоара для языка Sisal. Циклические выражения языка Cloud-Sisal, выражения конструирования массивов и выражения замещения элементов массивов позволяют реализовать эффективно исполняемые программы вычислительной или инженерной математики. Таким образом, мы полагаем, что наша аксиоматическая семантика для этих типов выражений может представлять интересный результат. Природа таких программ позволяет достичь не только эффективного исполнения, но и упростить верификацию. Действительно, программы вычислительной математики часто основаны на итерациях над структурами данных. Символический метод верификации финитных итераций является в этой ситуации очень полезным, так как он элиминирует те проблемные инварианты цикла, которые всегда мешают формальной верификации. Все предыдущие исследования этого метода были теоретическими, CPPS представляет собой первую попытку использования его на практике.
Nowadays, when formal fundamentals of program verification are well studied, researchers concentrate their efforts on domain-specific methods for various classes of programs. However, it seems that the field of scientific and engineering applications still lacks attention. We would like to contribute to filling this gap through the development of the Cloud Parallel Programming System (CPPS). The goal of this project is to create a parallel programming system for Sisal programs. Deductive verification of Sisal programs is one the of important subgoals. Since the Cloud Sisal language is built on the basis of loop expressions, their axiomatic semantics is the basis of Hoare’s logic for the Sisal language. The Cloud Sisal loop expressions, array construction expressions and array element replacement expressions enable efficiently executable computational or engineering mathematics programs. Thus, we believe that our axiomatic semantics for these types of expressions may present an interesting result.
Automatic C Program Verification Based on Mixed Axiomatic Semantics
