Exjobbsförslag från företag
Detta är ett uppsatsförslag hämtat från Nationella Exjobb-poolen. Klicka här för att komma tillbaka till samtliga exjobbsförslag.
Förslaget inkom 2006-10-27
Implementation of a tool for formal verification of C programs
OBS! ANSÖKNINGSTIDEN FÖR DETTA EXJOBB HAR LÖPT UT.
KeY is a tool for formal verification of computer programs. Given a formal specification of the program, an implementation of the program can be proven correct with respect to the
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.
Kolla även in Boutique Hotels Singapore,
Boutique Hotels Hong Kong,
Boutique Hotels Shanghai,
Boutique Hotels Dubai,
Boutique Hotels Los Angeles,
Boutique Hotels Denver,
Boutique Hotels Dallas,
Boutique Hotels Philadelphia,
Boutique Hotels Bath,
Boutique Hotels Santorini,
Boutique Hotels Portugal.
Informationen om uppsatsförslag är hämtad från Nationella Exjobb-poolen.