Project Proposal on C VerificationNeelima Premsankar, UT EID: np4438C remains a language of choice, for developing embedded software – mainly because of the programmer's control over all the resources required for program execution such as memory layout and allocation. Although this increases efficiency, it comes with the drawbacks of run-time errors due to buffer overflows and dangling pointers. Since the C type system is unsafe, such errors are difficult to detect in programs. This project seeks to analyze the different methods and tools currently adopted for the verification of software systems written in C. Some of the methods that will be discussed include static analysis, specification languages for C (similar to JML for Java) and a verification tool that uses this specification language, “separation logic” as opposed to conventional Hoare logic, etc.The first task is to arrive at a taxonomy for the different techniques, methods and tools – for instance, the tools that annotate the C language with specification constructs, those that use model checking, static analysis vs. run-time checks, etc. Also, static analysis tools are fully automated whereas tools like Caduceus use interactive proof assistants. How theoretic methods like verification using “automated reasoning” and “separation logic” are effective for C language will be tackled. “Separation logic” has been defined as an extension of Hoare logic for reasoning about programs that manipulate pointer structures. Separation logic aims at proving fine-grained properties about pointers and memory footprints, such as non overlapping (i.e. separation) between memory regions. Contrary to Hoare logic, separation logic allows local reasoning on the memory footprint of a statement. Such a local reasoning facilitates program proofs.Once the classification has been done, a comparative analysis of the methods and tools will be done. For the tools, I'd run them on different types of C constructs to check their efficacy against specific types of errors (NULL pointer dereferencing, integer/arithmetic overflow, out of bounds memory access, etc.) and analyze the results. The expected results at the end of the first task would be a broad understanding of the varying methods/tools used to verify the C language and a suitable classification for them. Also, a mapping of the tools to the techniques they adopt will be available at the end of the first phase. The results at the end of the last phase would be comparisons between different methods/tools on the basis of the accuracy of their verification, against different types of errors, scalability, computational time and memory required.A brief timeline is as follows:1. Literature Survey October 102. Taxonomy October 173. Installation of Tools & Identification of the C Constructs to be Checked forOctober 314. Running of Tests November 155. Comparative Analysis November 30References:1) Tools for Verification and Validation http://www.springerlink.com/content/rj5glgjp6lvbvt4e/2) Experiments in validating formal semantics for C (Sandrine Blazy, ENSIIE and INRIA Rocquencourt)3) Multi-Prover Verification of C Programs (Jean-Christophe Filliâtre, Claude Marché4) The software model checker B LAST - Applications to software engineering (Dirk Beyer · Thomas A. Henzinger · Ranjit Jhala · Rupak Majumdar)5) C-Language Verification Tool Using Formal Methods “VARVEL” (TOKUOKA Hiroki, MIYAZAKI Yoshiaki, HASHIMOTO
View Full Document
Unlocking...