Beschreibung
The idea behind deductive program verification based on symbolic execution is to execute a program within a logic calculus using symbolic rather than concrete values for variables. As a consequence, all possible runs of a program are covered making it possible to show that the program satisfies its specification for any input. This thesis addresses several problems that occur in the verification of programs written in the object-oriented language JavaCard, e.g., the finiteness of primitive integer data types and the difficulty of finding suitable loop invariants. The presented approaches to overcome these problems are implemented in the KeY program verification system.