Towards Automatic Deductive Verification of C Programs with Sisal Loops Using the C-lightVer System

The C-lightVer system is developed in IIS SB RAS for C-program deductive verification. C-kernel is an intermediate verification language in this system. Cloud parallel programming system (CPPS) is also developed in IIS SB RAS. Cloud Sisal is an input language of CPPS. The main feature of CPPS is implicit parallel execution based on automatic parallelization of Cloud Sisal loops. Cloud-Sisal-kernel is an intermediate verification language in the CPPS system. Our goal is automatic parallelization of such a superset of C that allows implementing automatic verification. Our solution is such a superset of C-kernel as C-Sisal-kernel. The first result presented in this paper is an extension of C-kernel by Cloud-Sisal-kernel loops. We have obtained the C-Sisal-kernel language. The second result is an extension of C-kernel axiomatic semantics by inference rule for Cloud-Sisal-kernel loops. The paper also presents our approach to the problem of deductive verification automation in the case of finite iterations over data structures. This kind of loops is referred to as definite iterations. Our solution is a composition of symbolic method of verification of definite iterations, verification condition metageneration and mixed axiomatic semantics method. Symbolic method of verification of definite iterations allows defining inference rules for these loops without invariants. Symbolic replacement of definite iterations by recursive functions is the base of this method. Obtained verification conditions with applications of recursive functions correspond to logical base of ACL2 prover. We use ACL2 system based on computable recursive functions. Verification condition metageneration allows simplifying implementation of new inference rules in a verification system. The use of mixed axiomatic semantics results to simpler verification conditions in some cases.

Towards verification of scientific and engineering programs. The CPPS project

В настоящее время, когда теоретические основы верификации программ хорошо изучены, исследователи концентрируют свои усилия на предметно-ориентированных методах для различных классов программ. Инструменты, которые они выбирают, варьируются от проверки моделей для сетевых протоколов до исчислений указателей для фрагментов ядра операционной системы. Однако, похоже, что области научных и инженерных программ все еще уделяется недостаточно внимания. Мы хотели бы внести свой вклад в заполнение этого пробела с помощью разработки системы 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.

The Automation of C Program Verification by Symbolic Method of Loop Invariants Elimination

During deductive verification of programs written in imperative languages, the generation and proof of verification conditions corresponding to loops can cause difficulties, because each one must be provided with an invariant whose construction is often a challenge. As a rule, the methods of invariant synthesis are heuristic ones. This impedes its application. An alternative is the symbolic method of loop invariant elimination suggested by V.A. Nepomniaschy in 2005. Its idea is to represent a loop body in a form of special replacement operation under certain constraints. This operation expresses loop effect in a symbolic form and allows to introduce an inference rule which uses no invariants in axiomatic semantics. This work represents the further development of this method. It extends the mixed axiomatic semantics method suggested for C-light program verification. This extension includes the verification method of iterations over changeable arrays possibly with loop exit in C-light programs. The method contains the inference rule for iterations without loop invariants. This rule was implemented in verification conditions generator which is a part of the automated system of C-light program verification. To prove verification conditions automatically in ACL2, two algorithms were developed and implemented. The first one automatically generates the replacement operation in ACL2 language, the second one automatically generates auxiliary lemmas which allow to prove the obtained verification conditions in ACL2 successfully in automatic mode. An example which illustrates the application of the mentioned methods is described.