 |
|
||||||||||
Completed Master's Theses
| Name of Student | Timeframe | Title of Project |
Documents |
|
Daniel Schweizer |
AS 2012 |
Overapproximating the Cost of Loops |
[Description] [Report] |
|
Andres Bühlmann |
AS 2012 |
Permission-Based Verification of Subclassing and Traits |
[Description] [Report] |
|
Ivo Colombo |
SS 2012 |
Debugging Symbolic Execution |
[Description] [Report] |
|
Rokas Matulis |
SS 2012 |
Extensible Code Contracts for Scala |
[Description] [Report] |
|
Florian Egli |
AS 2011 |
Translating Spec# Programs to C# with CodeContracts |
[Description] [Report] |
|
Dominik Gabi |
SS 2011 |
Disjunction on Demand |
[Description] [Report] |
|
Dimitar Asenov |
AS 2010 |
Design and Implementation of Envision - a Visual Programming System |
[Description] [Report] |
| Malte Schwerhoff | AS 2010 | Symbolic Execution for Chalice |
[Description] [Report] |
|
Prateek Agarwal |
SS 2010 |
Adding Closure Support to Chalice |
[Description] [Report] |
|
Filip Wieladek |
SS 2010 |
Automatic Verification of Concurrent Programs |
[Description] [Report] |
|
Valentin Wüstholz |
SS 2009 |
Encoding Scala Programs for the Boogie Verifier |
[Description] [Report] |
|
Florian Leu |
SS 2009 |
Implementation of Frozen Objects into Spec# |
[Description] [Report] |
|
Roman Fuchs |
SS 2009 |
Software Engineering modules for Computer Science Talent Scout |
[Description] [Report] |
| Andreas Kägi | WS 2008/2009 |
Embedding JML-annotated Programs in the Coq Proof System |
[Description] [Report] |
| Christoph Studer | 11/08/- 04/09 | Improving Cee and Ownership-Based Verification |
[Description] [Report] |
|
Simon Hofer |
09/08 - 02/09 | Verification of Design Patterns |
[Description] [Report] |
| Samuele Gantner | 03/08 - 09/08 | Verifying Spec# Delegates |
[Description] [Report] |
| Jürg Billeter | 02/08 - 08/08 | Counterexample Execution |
[Description] [Report] |
| Benjamin Morandi | 10/07 - 04/08 | Translating invariant proofs between Spec# and JML |
[Description] [Report] |
| Benjamin Lutz | 01/08 - 05/08 | Error Reporting for Universe Types with Transfer |
[Description] [Report] |
| Manfred Stock | 08/07 - 01/08 | Implementing a Universe Type System for Scala |
[Description] [Report] |
| Annetta Schaad | 05/07 - 11/07 | Inferring Universe annotations in the presence of ownership transfer |
[Description] [Report] |
| Geraldine von Roten | 04/07 - 10/07 | Proving well-formedness of interface specifications |
[Description] [Report] |
| Karin Freiermuth | 03/07 - 09/07 | Using program slicing to improve error reporting in Boogie |
[Description] [Report] |
| Claudia Brauchli | 03/07 - 09/07 | Integration of a new VCGen in ESC/Java2 |
[Description] [Report] |
| Samuel Willimann | 03/07 - 09/07 | An Automated Program Verifier for Java Bytecode |
[Description] [Report] |
| Mathias Ottiger | 02/07 - 08/07 | Runtime Support for Generics and Transfer in Universe Types |
[Description] [Report] |
| Robin Züger | 01/07 - 07/07 | Generic Universe Types in JML |
[Description] [Report] |
| Daniel Schregenberger | 09/06 - 06/07 | Universe Type System for Scala |
[Description] [Report] |
| Yoshimi Takano | 09/06 - 03/07 | Implementing Uniqueness and Ownership Transfer in the Universe Type System |
[Description] [Report] |
| Martin Klebermaß | 10/06 - 04/07 | An Isabelle Formalization of the Universe Type System |
[Description] [Report] |
| Andreas Fürer | 09/06 - 03/07 | Combining Runtime and Static Universe Type Inference |
[Description] [Report] |
| Cristian Garcia | 09/06 - 03/07 | Kangoo API for Web-Based Applications |
[Description] [Report] |
| Ovidio Mallo | WS 2006/07 | A Translator from BML annotated Java Bytecode to BoogiePL |
[Description] [Report] |
| Alex Suzuki | 04/06 - 09/06 | Formalization and implementation of translation from Java Bytecode to Guarded Commands |
[Description] [Report] |
| Matthias Niklaus | 12/05 - 06/06 | Static Universe Type Inference using a SAT-Solver |
[Description] [Report] |
| Marco Bär | 11/05 - 05/06 | Practical Runtime Universe Type Inference |
[Description] [Report] |
| Stefan Nägeli | 09/05 - 03/06 | Ownership in Design Patterns |
[Description] [Report] |
| Erich Laube | WS 2005/06 | Design and Implementation of a JML Frontend for Boogie |
[Description] [Report] |
| Ronny Zakhejm | WS 2005/06 | Ownership-based Program Verification in Jive |
[Description] [Report] |
| Fabian Bannwart | WS 2005/06 | Changing Software Correctly |
[Description] [Report] |
| Nathalie Kellenberger | 04/05-10/05 | Static Universe Type Inference |
[Description] [Report] |
| Frank Lyner | 01/05-07/05 | Runtime Universe Type Inference |
[Description] [Report] |
| Thomas Hächler | 09/04-03/05 | Applying the Universe Type System to an Industrial Application |
[Description] [Report] |
Wichtiger Hinweis:
Diese Website wird in älteren Versionen von Netscape ohne
graphische Elemente dargestellt. Die Funktionalität der
Website ist aber trotzdem gewährleistet. Wenn Sie diese
Website regelmässig benutzen, empfehlen wir Ihnen, auf
Ihrem Computer einen aktuellen Browser zu installieren. Weitere
Informationen finden Sie auf
folgender
Seite.
Important Note:
The content in this site is accessible to any browser or
Internet device, however, some graphics will display correctly
only in the newer versions of Netscape. To get the most out of
our site we suggest you upgrade to a newer browser.
More
information
