CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Towards a Deductive Compilation Approach

Ran Ji (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Göteborg : Chalmers University of Technology, 2012. - 110 s.

Software correctness is an important topic, however, it is difficult to achieve. This thesis is a step towards a new way to ensure the software correctness in both source code and bytecode level. KeY is a state-of-the-art verification tool for Java source code. We boost the speed of the proving process of KeY by interleaving symbolic execution and partial execution. We propose a deductive compilation approach to ensure correctness of the compiled code by generating it directly, while guaranteeing its soundness with respect to the source code. Further verification for bytecode is not needed. It is a two step approach. The first step is symbolic execution of the Java source code, interleaved with partial evaluation for optimization purpose. In the second step, the compiled code is generated by an extended sequent calculus. At the moment, we experiment with generating Java source code from Java source code, which results in a program specialized for Java programs. A prototypical implementation is available.

Nyckelord: Symbolic Execution, Partial Evaluation, Deductive Compilation, Software Verification, Software Engineering

Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2012-02-06.
CPL Pubid: 154805


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)


Informations- och kommunikationsteknik

Chalmers infrastruktur


Datum: 2012-03-07
Tid: 13:15
Lokal: room EB, Hörsalsvägen 11, Chalmers Universiry of Technology
Opponent: Marieke Huisman

Ingår i serie

Technical report L - Department of Computer Science and Engineering, Chalmers University of Technology and Göteborg University