Detta är ett uppsatsförslag hämtat från Nationella Exjobb-poolen. Klicka här för att komma tillbaka till samtliga exjobbsförslag.
Implementation of a tool for formal verification of C programs
specification (if it is correct). The current version of KeY handles a subset of the programming language JAVA, but there is an ongoing work to prepare a version also for a subset of C. The work of this thesis would be to continue the work with a C-version of KeY.
A short description of how KeY works: Once a specification and an implementation of a program is available, the user can try to prove that the implementation satisfies the specification. The tool then translates the specification and the program to a so-called proof obligation, which is expressed in a kind of logic called Dynamic Logic. The task for the user is now to try to prove---with assistance from the tool---that the proof obligation is valid.
This is done by applying rules to the proof obligation that rewrite the proof obligation, and the ultimate goal is to reach a formula that is trivially true. An important part of this proving activity is to symbolically execute the program part of the proof obligation.
What needs to be done implementation-wise to prepare a C-version of KeY?
- Integrate a new front-end (parser+some analysis) for C
- Create new data structures for representing C programs
- Find out which rules for symbolically executing JAVA can
be re-used for C, and what new rules need to be defined
- Extend the infrastructure of KeY to handle some C-specific
issues, e.g. so-called deep-copy assignment
- Implement pretty-printing of C
KeY is implemented in JAVA.
Prerequisite: Programming skills in JAVA. Some knowledge in
logic/formal methods is recommended.
Informationen om uppsatsförslag är hämtad från Nationella Exjobb-poolen.