| Chair of Programming Methodology | |
 |
|
|
Semester-, Master-, and Diploma-Projects
Ongoing Semester-/Diplomarbeiten || Completed Semester-/Diplomarbeiten |
|
We offer semester projects and Master's projects across a number of software engineering topics, all related to the same general goal: the construction of high-quality software through object technology and formal methods.
Our student projects are typically embedded in larger research projects. Therefore, the available topics change frequently as our research progresses. Contact one of us to learn about the student projects we currently offer. We typically have a variety of topics - both theoretical and practical - in the following areas:
|
| Name of Student | Type of Project | Title of Project | Documents |
|---|---|---|---|
| Simon Hofer | Masterarbeit 09/08 - 02/09 |
Verification of Design Patterns | Details |
| Christoph Studer | Masterarbeit 10/08 - 04/09 |
Multiple heaps for ownership based verification | Details |
| Andreas Kaegi | Masterarbeit 09/08 - 03/09 |
Embedding JML-annotated Programs in the Coq Proof System | Details |
| Phokham Nonava | Semesterarbeit SS 2008 |
A Universe Type Checker using JSR308 | Details |
|
| Name of Student | Type of Project | Title of Project | Documents |
|---|---|---|---|
| Samuele Gantner | Masterarbeit 03/08 - 09/08 |
Verifying Spec# Delegates | Details |
| Jürg Billeter | Masterarbeit 02/08 - 08/08 |
Counterexample Execution | Details |
| Benjamin Morandi | Masterarbeit 10/07 - 04/08 |
Translating invariant proofs between Spec# and JML | Details |
| Benjamin Lutz | Diplomarbeit 01/08 - 05/08 |
Error Reporting for Universe Types with Transfer | Details |
| Sebastian Groessl | Semesterarbeit HS 2007 |
Slicing Spec# Programs | Details |
| David Steiger | Semesterarbeit HS 2007 |
Extending supported language subset of Jive | Details Report |
| Manfred Stock | Masterarbeit 08/07 - 01/08 |
Implementing a Universe Type System for Scala | Details |
| Annetta Schaad | Masterarbeit 05/07 - 11/07 |
Inferring Universe annotations in the presence of ownership transfer | Details |
| Geraldine von Roten | Masterarbeit 04/07 - 10/07 |
Proving well-formedness of interface specifications | Details Report |
| Karin Freiermuth | Masterarbeit 03/07 - 09/07 |
Using program slicing to improve error reporting in Boogie | Details |
| Martin Bill | Semesterarbeit WS 2006/07 |
Usability Evaluation of Jive | Details |
| Claudia Brauchli | Masterarbeit 03/07 - 09/07 |
Integration of a new VCGen in ESC/Java2 | Details |
| Samuel Willimann | Masterarbeit 03/07 - 09/07 |
An Automated Program Verifier for Java Bytecode | Details |
| Mathias Ottiger | Masterarbeit 02/07 - 08/07 |
Runtime Support for Generics and Transfer in Universe Types | Details |
| Robin Züger | Masterarbeit 01/07 - 07/07 |
Generic Universe Types in JML | Details |
| Daniel Schregenberger | Masterarbeit 09/06 - 06/07 |
Universe Type System for Scala | Details |
| Yoshimi Takano | Masterarbeit 09/06 - 03/07 |
Implementing Uniqueness and Ownership Transfer in the Universe Type System | Details |
| Martin Klebermaß | Diplomarbeit 10/06 - 04/07 |
An Isabelle Formalization of the Universe Type System | Details |
| Andreas Fürer | Masterarbeit 09/06 - 03/07 |
Combining Runtime and Static Universe Type Inference | Details |
| Dominique Schneider | Semesterarbeit WS 2006/07 |
Testing Tool for Compilers | Details |
| Cristian Garcia | Masterarbeit 09/06 - 03/07 |
Kangoo API for Web-Based Applications | Report available on request. |
| Ovidio Mallo | Masterarbeit WS 2006/07 |
A Translator from BML annotated Java Bytecode to BoogiePL | Details |
| Alex Suzuki | Masterarbeit 04/06 - 09/06 |
Formalization and implementation of translation from Java Bytecode to Guarded Commands | Details |
| Yoshimi Takano | Semesterarbeit SS 2006 |
Integrating Simplify into Jive | Details |
| Annetta Schaad | Semesterarbeit SS 2006 |
Universe Type System for Eiffel | Details |
| Ovidio Mallo | Semesterarbeit SS 2006 |
MultiJava, JML, and Generics | Details |
| Paolo Bazzi | Semesterarbeit SS 2006 |
Integration of Universe Type System Tools into Eclipse | Details |
| Benjamin Lutz | Semesterarbeit SS 2006 |
Mono's System.Collection Classes: A Spec# Case Study | Details |
| Olivier Girard | Semesterarbeit SS 2006 |
Case Study in the Boogie Methodology | Details |
| Matthias Niklaus | Masterarbeit 12/05 - 06/06 |
Static Universe Type Inference using a SAT-Solver | Details |
| Marco Bär | Masterarbeit 11/05 - 05/06 |
Practical Runtime Universe Type Inference | Details |
| David Graf | Semesterarbeit WS 2005/06 |
Implementing Purity and Side Effect Analysis for Java Programs | Details |
| Stefan Nägeli | Masterarbeit 09/05 - 03/06 |
Ownership in Design Patterns | Details |
| Marco Meyer | Semesterarbeit WS 2005/06 |
Interaction with Ownership Graphs | Details |
| Erich Laube | Masterarbeit WS 2005/06 |
Design and Implementation of a JML Frontend for Boogie | Details Paper |
| Ronny Zakhejm | Masterarbeit WS 2005/06 |
Ownership-based Program Verification in Jive | Details Paper |
| Fabian Bannwart | Masterarbeit WS 2005/06 |
Changing Software Correctly | Details Paper |
| Adrian Moos | Semesterarbeit SS 2005 |
Welldefinedness and expressiveness of JML specifications | Details Paper |
| Dirk Wellenzohn | Semesterarbeit SS 2005 |
Implementation of a Universe type checker in ESC/Java2 | Details |
| Nathalie Kellenberger | Masterarbeit 04/05-10/05 |
Static Universe Type Inference | Details |
| Samuel Burri | Semesterarbeit SS 2005 |
Translation of object-oriented programs into guarded commands | Paper |
| Dominik Grolimund | Semesterarbeit SS 2005 |
Design Patterns in Peer-to-Peer Systems | Details Paper |
| Frank Lyner | Masterarbeit 01/05-07/05 |
Runtime Universe Type Inference | Details |
| Ghislain Fourny | Semesterarbeit WS 2004/05 |
Generating Proof Obligations from JML Specifications | Details |
| Erich Laube | Semesterarbeit WS 2004/05 |
Transformation of Java Card into Diet Java Card | Details |
| Thomas Hächler | Masterarbeit 09/04-03/05 |
Applying the Universe Type System to an Industrial Application | Details |
| Alex Suzuki | Semesterarbeit WS 2004/05 |
Bytecode support for the Universe type system and compiler | Details |
| Marcello Miragliotta | Semesterarbeit SS 2004 |
Specification Model Library for the Interactive Program Prover JIVE |
Details Paper |
| Fabian Bannwart | Semesterarbeit SS 2004 |
A Logic for Bytecode and the Translation of Proofs from Sequential Java | Details Paper |
| Thomas Hächler | Semesterarbeit SS 2004 |
Static Fields in the Universe Type System | Details |
| Daniel Schregenberger | Semesterarbeit SS 2004 |
Runtime checks for the Universe Type System | Details |
|
|
Last update: 10.20.2008 by Arsenii.Rudich@inf.ethz.ch |
