Programming Methodology Group

Search

en

Completed Projects

Verification2 of the Authentic Digital EMblem
Lasse Meinen, SS 2024
DownloadDescription (PDF, 154 KB), DownloadReport (PDF, 862 KB)

Automated verification of a Rust differential privacy library
Till Arnold, AS 2023
DownloadDescription (PDF, 80 KB), DownloadReport (PDF, 448 KB)

Contract Checking at Runtime and Verification-based Optimizations for a Rust Verifier
Cedric Hegglin, AS 2023
DownloadDescription (PDF, 159 KB), DownloadReport (PDF, 695 KB)

An Automatic Program Verifier for Hyperproperties
Anqi Li, AS 2023
DownloadDescription (PDF, 135 KB), DownloadReport (PDF, 820 KB)

A Linear Typesystem for a Go Verifier
Liming Han, SS 2023
DownloadDescription (PDF, 165 KB), DownloadReport (PDF, 1.1 MB)

Secure Deletion of Sensitive Data in Protocol Implementations
Hugo Queinnec, SS 2023
DownloadDescription (PDF, 175 KB), DownloadReport (PDF, 1.1 MB)

Using Verification Techniques to Synthesise Rust Programs
Fabian Bösiger, SS 2023
DownloadDescription (PDF, 189 KB), DownloadReport (PDF, 548 KB)

Ownership Typesystem based Optimisations for Rust
Janis Peyer, SS 2023
DownloadDescription (PDF, 83 KB), DownloadReport (PDF, 781 KB)

A Formally Verified Automatic Verifier for Concurrent Programs
Ellen Arlt, SS 2023
DownloadDescription (PDF, 130 KB), DownloadReport (PDF, 1.2 MB)

Proving Refinement in a Rust Verifier
Jan Schär, SS 2023
DownloadDescription (PDF, 122 KB), DownloadReport (PDF, 577 KB)

Time Reasoning and Secure Information Flow in a Rust Verifier
Alexandre Pinazza, SS 2023
DownloadDescription (PDF, 106 KB), DownloadReport (PDF, 358 KB)

Annotating the Rust Standard Library with Specifications for
Use in a Rust Verifier
Julian Dunskus, SS 2023
DownloadDescription (PDF, 115 KB), DownloadReport (PDF, 2.4 MB)

Automatically Generating Memory Safety Certificates for Rust Programs
Pascal Huber, SS 2022
DownloadDescription (PDF, 68 KB), DownloadReport (PDF, 641 KB)

Verification of closures for Go programs
Stefano Milizia, SS 2022
DownloadDescription (PDF, 168 KB), DownloadReport (PDF, 392 KB)

Specification and Verification of Iterators in a Rust Verifier
Jonas Hansen, SS 2022
DownloadDescription (PDF, 278 KB), DownloadReport (PDF, 1.3 MB)

Adding Algebraic Data Types to a Verification Language
Allesandro Maissen, SS 2022
DownloadDescription (PDF, 113 KB), DownloadReport (PDF, 867 KB)

Specifying and Verifying the IO Behavior of the SCION Border Router   
Lino Telschow, AS 2021
DownloadDescription (PDF, 208 KB), DownloadReport (PDF, 3.7 MB)

Automatically Generating Java Benchmarks with Known Errors
Madalina Hurmuz, AS 2021
DownloadDescription (PDF, 178 KB), DownloadReport (PDF, 1.1 MB)

Reasoning about Complexities in a Rust Verifier
Lowis Engel, AS 2021
DownloadDescription (PDF, 170 KB), DownloadReport (PDF, 697 KB)

Extending the Viper Verification Language with User-Defined Permission Models
Matthias Roshardt, SS 2021
DownloadDescription (PDF, 271 KB), DownloadReport (PDF, 1.2 MB)

Specifying and Verifying Sequences and Array Algorithms in a Rust Verifier
Johannes Schilling, SS 2021
DownloadDescription (PDF, 81 KB), DownloadReport (PDF, 417 KB)

Verifying Competitive-Programming Programs in a Rust Verifier
Ahmed Rayan, AS 2020
DownloadDescription (PDF, 136 KB), DownloadReport (PDF, 598 KB)

Extended Support for Borrowing and Lifetimes in Prusti
Lorenz Gorse, SS 2020
DownloadDescription (PDF, 270 KB), DownloadReport (PDF, 1004 KB)

Assertion-based Testing of Go Programs
Eva Charlotte Mayer, SS 2020
DownloadDescription (PDF, 165 KB), DownloadReport (PDF, 789 KB)

Verification of Advanced Properties for Real World Vyper Contracts
Christian Bräm, SS 2020
DownloadDescription (PDF, 171 KB), DownloadReport (PDF, 1.1 MB)

Verifying Safe Clients of Unsafe Code and Trait Implementations in Rust
Jakob Beckmann, SS 2020
DownloadDescription (PDF, 137 KB) DownloadReport (PDF, 1.1 MB)

Verification of Closures in Rust Programs
Fabian Wolff, SS 2020
DownloadDescription (PDF, 208 KB), DownloadReport (PDF, 821 KB)

Computing Fine-grained Type Information for Rust Programs
William Seddon, SS 2020
DownloadDescription (PDF, 210 KB), DownloadReport (PDF, 1.2 MB)

Verification of Programs Written in Libra's Move Language
Constantin Müller, SS 2020
DownloadDescription (PDF, 162 KB), DownloadReport (PDF, 1.1 MB)

Inference of Progressive Loop Invariants for Array Programs
Nils Becker, SS 2020
DownloadDescription (PDF, 237 KB), DownloadReport (PDF, 802 KB)

Beyond the Frame Rule: Static Inlining in Separation Logic
Thibault Dardinier, AS 2019
DownloadDescription (PDF, 145 KB), DownloadReport (PDF, 1.3 MB)

Profiling Symbolic Execution
Linard Arquint, SS 2019
DownloadDescription (PDF, 159 KB), DownloadReport (PDF, 2.4 MB)

Verification of Ethereum Smart Contracts written in Vyper
Robin Sierra, FS 2019
DownloadDescription (PDF, 226 KB), DownloadReport (PDF, 1.1 MB)

Supporting Borrows in Specification Functions of a Rust Verifier
Nicolas Trüssel, AS 2019
DownloadDescription (PDF, 52 KB), DownloadReport (PDF, 1.4 MB)

Deductive Verification of Real-World C++ Weak-Memory Programs
Pascal Wiesmann, AS 2018
DownloadDescription (PDF, 123 KB), DownloadReport (PDF, 882 KB)

SMT models for verification debugging
Cédric Stoll, AS 2018
DownloadDescription (PDF, 94 KB), DownloadReport (PDF, 3.8 MB)

Verification of Rust Generics, Typestates, and Traits
Matthias Erdin, SS 2018
DownloadDescription (PDF, 146 KB), DownloadReport (PDF, 717 KB)

Verification of Information Flow Security for Python Programs
Severin Meier, SS 2018
DownloadDescription (PDF, 112 KB), DownloadReport (PDF, 1.1 MB)

Visual Debugging for Symbolic Execution
Alessio Aurecchia, SS 2018
DownloadDescription (PDF, 313 KB), DownloadReport (PDF, 8.7 MB)

Verifying Lock-Free Data Structures and Algorithms
Felix Wolf, SS 2018
DownloadDescription (PDF, 121 KB), DownloadReport (PDF, 1 MB)

Modular Verification of Message Passing Programs
Gaurav Parthasarathy, AS 2017
DownloadDescription (PDF, 68 KB), DownloadReport (PDF, 1.6 MB)

Automated Generation of Data Quality Checks
Madelin Schumacher, AS 2017
DownloadDescription (PDF, 165 KB), DownloadReport (PDF, 1.3 MB)

Automatic Verification of Closures and Lambda-Functions in Python
Benjamin Weber, SS 2017
DownloadDescription (PDF, 156 KB), DownloadReport (PDF, 565 KB)

Proving Temporal Properties by Abstract Interpretation
Samuel Ueltschi, SS 2017
DownloadDescription (PDF, 107 KB), DownloadReport (PDF, 901 KB)

Static Program Analysis of Data Usage Properties
Simon Wehrli, SS 2017
DownloadDescription (PDF, 218 KB), DownloadReport (PDF, 858 KB)

Interprocedural Static Analysis by Abstract Interpretation
Flurin Rindisbacher, SS 2017
DownloadDescription (PDF, 127 KB), DownloadReport (PDF, 1.5 MB)

Serializability checking for MongoDB clients
Johannes Baum, AS 2016
DownloadDescription (PDF, 125 KB), DownloadReport (PDF, 2.3 MB)

Inference of Pointwise Specifications for Heap Manipulating Programs
Severin Münger, AS 2016
DownloadDescription (PDF, 166 KB), DownloadReport (PDF, 2 MB)

A Framework for Bidirectional Program Transformations
Simon Fritsche, AS 2016
DownloadDescription (PDF, 105 KB), DownloadReport (PDF, 954 KB)

Analyzing Serializability of Cassandra Applications
Arthur Kurath, AS 2016
DownloadDescription (PDF, 144 KB), DownloadReport (PDF, 1.3 MB)

A formal Semantics for Viper
Cyrill Gössi, SS 2016
DownloadDescription (PDF, 58 KB), DownloadReport (PDF, 842 KB)

Testing program robustness against deviant behavior
Patrick Emmisberger, SS 2016
DownloadDescription (PDF, 142 KB), DownloadReport (PDF, 1.6 MB)

Advanced Features for an Integrated Verification Environment
Ruben Kälin, SS 2016
DownloadDescription (PDF, 585 KB), DownloadReport (PDF, 3.5 MB)

Termination Analysis of Heap-Manipulating Programs by Abstract Interpretation
Lukas Neukom, SS 2016
DownloadDescription (PDF, 32 KB), DownloadReport (PDF, 989 KB)

Input-Output Verification in Viper
Vytautas Astrauskas, SS 2016
DownloadDescription (PDF, 68 KB), DownloadReport (PDF, 455 KB)

Generalised Verification for Quantified Permissions
Nadja Müller, SS 2016
DownloadDescription (PDF, 64 KB), DownloadReport (PDF, 506 KB)

From Viper to Grasshopper
Andrea Helfenstein, SS 2016
DownloadDescription (PDF, 89 KB), DownloadReport (PDF, 393 KB)

Automatic Inference of Quantified Permissions by Abstract Interpretation
Seraiah Walter, SS 2016
DownloadDescription (PDF, 440 KB), DownloadReport (PDF, 1.1 MB)

Improving Code Reviews using the Envision IDE
Manuel Galbier, SS 2016
DownloadDescription (PDF, 106 KB), DownloadReport (PDF, 8.2 MB)

Rust2Viper: Building a static verifier for Rust
Florian Hahn, AS 2015
DownloadDescription (PDF, 160 KB), DownloadReport (PDF, 3.8 MB)

Integration and Analysis of Alternative SMT Solvers for Software Verification
Frederik Rothenberger, AS 2015
DownloadDescription (PDF, 94 KB), DownloadReport (PDF, 1.4 MB)

Augmenting software development with information scripting
Lukas Vogel, AS 2015
DownloadDescription (PDF, 153 KB), DownloadReport (PDF, 6.9 MB)

Self-hosting the Envision Visual Programming Environment
Patrick Lüthi, SS 2015
DownloadDescription (PDF, 95 KB), DownloadReport (PDF, 1.2 MB)

Automated Support for Mathematical Datatypes via Trigger-based Axiomatization
Prasoon Dadhich, SS 2015
DownloadDescription (PDF, 112 KB), DownloadReport (PDF, 417 KB)

Verification of Finite Blocking in Chalice
Robert Meier, SS 2015
DownloadDescription (PDF, 94 KB), DownloadReport (PDF, 481 KB)

Modular Verification of Finite Blocking
Christian Klauser, SS 2014
DownloadDescription (PDF, 57 KB), DownloadReport (PDF, 1.3 MB)

Static Checking of TouchDevelop Programs against Web Service Specifications

Pascal Zimmermann, AS 2013
DownloadDescription (PDF, 140 KB), DownloadReport (PDF, 555 KB)

Fine-grained Software Version Control Based on a Program's Abstract Syntax Tree

Martin Pascal Otth, SS 2014
DownloadDescription (PDF, 163 KB), DownloadReport (PDF, 2.7 MB)

Inferring Counter-Examples from Abstract Error States via Backward Analysis

Raphael Fuchs, AS 2013
DownloadDescription (PDF, 52 KB), DownloadReport (PDF, 1.6 MB)

Inferring SIL Specifications with the Abstract Interpreter Sample

Severin Heiniger, AS 2013
DownloadDescription (PDF, 150 KB), DownloadReport (PDF, 959 KB)

Quantified Permissions for Random Access Data Structures

Korbinian Breu, AS 2013
DownloadDescription (PDF, 171 KB), DownloadReport (PDF, 424 KB)

Delfy: Dynamic Test Generation for Dafny

Patrick Spettel, AS 2013
DownloadDescription (PDF, 71 KB), DownloadReport (PDF, 1.1 MB)

Must Analysis of Collection Elements

Yves Bonjour, SS 2013
DownloadDescription (PDF, 233 KB), DownloadReport (PDF, 887 KB)

Verification Condition Generation for the Intermediate Verification Language SIL

Stefan Heule, SS 2013
DownloadDescription (PDF, 149 KB), DownloadReport (PDF, 941 KB)

Translating Scala to SIL

Bernhard Brodowsky, SS 2013
DownloadDescription (PDF, 53 KB), DownloadReport (PDF, 463 KB)

Overapproximating the Cost of Loops

Daniel Schweizer, AS 2012
DownloadDescription (PDF, 194 KB), DownloadReport (PDF, 542 KB)

Permission-Based Verification of Subclassing and Traits

Andres Bühlmann, AS 2012
DownloadDescription (PDF, 114 KB), DownloadReport (PDF, 1.2 MB)

Debugging Symbolic Execution

Ivo Colombo, SS 2012
DownloadDescription (PDF, 168 KB), DownloadReport (PDF, 1.8 MB)

Extensible Code Contracts for Scala

Rokas Matulis, SS 2012
DownloadDescription (PDF, 105 KB), DownloadReport (PDF, 512 KB)

Translating Spec# Programs to C# with CodeContracts

Florian Egli, AS 2011
DownloadDescription (PDF, 241 KB), DownloadReport (PDF, 2.4 MB)

Disjunction on Demand

Dominik Gabi, SS 2011
DownloadDescription (PDF, 107 KB), DownloadReport (PDF, 1.5 MB)

Design and Implementation of Envision - a Visual Programming System

Dimitar Asenov, AS 2010
DownloadDescription (PDF, 137 KB), DownloadReport (PDF, 2.2 MB)

Symbolic Execution for Chalice

Malte Schwerhoff, AS 2010
DownloadDescription (PDF, 88 KB), DownloadReport (PDF, 685 KB)

Adding Closure Support to Chalice

Prateek Agarwal, SS 2010
DownloadDescription (PDF, 121 KB), DownloadReport (PDF, 824 KB)

Automatic Verification of Concurrent Programs

Filip Wieladek, SS 2010
DownloadDescription (PDF, 33 KB), DownloadReport (PDF, 732 KB)

Encoding Scala Programs for the Boogie Verifier

Valentin Wüstholz, SS 2009
DownloadDescription (PDF, 82 KB), DownloadReport (PDF, 764 KB)

Implementation of Frozen Objects into Spec#

Florian Leu, SS 2009
DownloadDescription (PDF, 33 KB), DownloadReport (PDF, 538 KB)

Software Engineering modules for Computer Science Talent Scout

Roman Fuchs, SS 2009
DownloadDescription (PDF, 63 KB), DownloadReport (PDF, 1.4 MB)

Embedding JML-annotated Programs in the Coq Proof System

Andreas Kägi, WS 2008/2009
DownloadDescription (PDF, 38 KB), DownloadReport (PDF, 593 KB)

Improving Cee and Ownership-Based Verification

Christoph Studer, 11/08 - 04/09
DownloadDescription (PDF, 57 KB), DownloadReport (PDF, 857 KB)

Verification of Design Patterns

Simon Hofer, 09/08 - 02/09
DownloadDescription (PDF, 71 KB), DownloadReport (PDF, 71 KB)

Verifying Spec# Delegates

Samuele Gantner, 03/08 - 09/08
DownloadDescription (PDF, 140 KB), DownloadReport (PDF, 2 MB)

Counterexample Execution

Jürg Billeter, 02/08 - 08/08
DownloadDescription (PDF, 45 KB), DownloadReport (PDF, 406 KB)

Translating invariant proofs between Spec# and JML

Benjamin Morandi, 10/07 - 04/08
DownloadDescription (PDF, 43 KB)

Error Reporting for Universe Types with Transfer

Benjamin Lutz, 01/08 - 05/08
DownloadDescription (PDF, 41 KB), DownloadReport (PDF, 475 KB)

Implementing a Universe Type System for Scala

Manfred Stock, 08/07 - 01/08
DownloadDescription (PDF, 47 KB), DownloadReport (PDF, 1 MB)

Inferring Universe annotations in the presence of ownership transfer

Annetta Schaad, 05/07 - 11/07
DownloadDescription (PDF, 36 KB), DownloadReport (PDF, 3 MB)

Proving well-formedness of interface specifications

Geraldine von Roten, 04/07 - 10/07
DownloadDescription (PDF, 30 KB), DownloadReport (PDF, 440 KB)

Using program slicing to improve error reporting in Boogie

Karin Freiermuth, 02/07 - 09/07
DownloadDescription (PDF, 33 KB), DownloadReport (PDF, 476 KB)

Integration of a new VCGen in ESC/Java2

Claudia Brauchli, 03/07 - 09/07
DownloadDescription (PDF, 31 KB), DownloadReport (PDF, 2.2 MB)

An Automated Program Verifier for Java Bytecode

Samuel Willimann, 03/07 - 09/07
DownloadDescription (PDF, 69 KB), DownloadReport (PDF, 1.1 MB)

Runtime Support for Generics and Transfer in Universe Types

Mathias Ottiger, 02/07 - 08/07
DownloadDescription (PDF, 39 KB), DownloadReport (PDF, 508 KB)

Generic Universe Types in JML

Robin Züger, 01/07 - 07/07
DownloadDescription (PDF, 49 KB), DownloadReport (PDF, 2.7 MB)

Universe Type System for Scala

Daniel Schregenberger, 09/06 - 06/07
DownloadDescription (PDF, 42 KB), DownloadReport (PDF, 935 KB)

Implementing Uniqueness and Ownership Transfer in the Universe Type System

Yoshimi Takano, 09/06 - 03/07
DownloadDescription (PDF, 41 KB), DownloadReport (PDF, 781 KB)

An Isabelle Formalization of the Universe Type System

Martin Klebermass, 10/06 - 04/07
DownloadDescription (PDF, 31 KB), DownloadReport (PDF, 611 KB)

Combining Runtime and Static Universe Type Inference

Andreas Fürer, 09/06 - 03/07
DownloadDescription (PDF, 35 KB), DownloadReport (PDF, 1.4 MB)

Kangoo API for Web-Based Applications

Cristian Garcia, 09/06 - 03/07
DownloadDescription (PDF, 11 KB), DownloadReport (PDF, 2.1 MB)

A Translator from BML annotated Java Bytecode to BoogiePL

Ovidio Mallo, WS 2006/07
DownloadDescription (PDF, 34 KB), DownloadReport (PDF, 601 KB)

Formalization and implementation of translation from Java Bytecode to Guarded Commands

Alex Suzuki, 04/06 - 09/06
DownloadDescription (PDF, 42 KB), DownloadReport (PDF, 924 KB)

Static Universe Type Inference using a SAT-Solver

Matthias Niklaus, 12/05 - 06/06
DownloadDescription (PDF, 26 KB), DownloadReport (PDF, 1 MB)

Practical Runtime Universe Type Inference

Marco Bär, 11/05 - 05/06
DownloadDescription (PDF, 26 KB), DownloadReport (PDF, 1.5 MB)

Ownership in Design Patterns

Stefan Nägeli, 09/05 - 03/06
DownloadDescription (PDF, 51 KB), DownloadReport (PDF, 4.4 MB)

Design and Implementation of a JML Frontend for Boogie

Erich Laube, WS 2005/06
DownloadDescription (PDF, 33 KB), DownloadReport (PDF, 487 KB)

Ownership-based Program Verification in Jive

Ronny Zakheijm, WS 2005/06
DownloadDescription (PDF, 33 KB), DownloadReport (PDF, 649 KB)

Changing Software Correctly

Fabian Bannwart, WS 2005/06
DownloadDescription (PDF, 46 KB), DownloadReport (PDF, 2.4 MB)

Static Universe Type Inference

Nathalie Kellenberger, 04/05 - 10/05
DownloadDescription (PDF, 74 KB), DownloadReport (PDF, 807 KB)

Runtime Universe Type Inference

Frank Lyner, 01/05 - 07/05
DownloadDescription (PDF, 29 KB), DownloadReport (PDF, 1.7 MB)

Applying the Universe Type System to an Industrial Application

Thomas Hächler, 09/04 - 03/05
DownloadDescription (PDF, 36 KB), DownloadReport (PDF, 1.8 MB)

Developing Tool Support for Understanding Quantifier Instantiations
Oskari Jyrkinen, AS 2023
DownloadDescription (PDF, 191 KB), DownloadReport (PDF, 3.6 MB)

Specifying and Verifying Static Initialization in Deductive Program Verifiers
Patricia Firlejczyk, AS 2023
DownloadDescription (PDF, 131 KB), DownloadReport (PDF, 838 KB)

Development of a data collection tool for the evaluation of a deductive verifier
Simon Hostettler, AS 2024
DownloadDescription (PDF, 94 KB), DownloadReport (PDF, 1 MB)

Translating Pegagogical Verification Exercises to Viper
Benjamin Frei, SS 2023
DownloadDescription (PDF, 331 KB), DownloadReport (PDF, 1.9 MB)

Advanced Counterexample Generation in Viper
Raoul van Doren, SS 2023
DownloadDescription (PDF, 164 KB), DownloadReport (PDF, 362 KB)

Method-specific encodings for Gobra structs
René Cáky, SS 2023
DownloadDescription (PDF, 106 KB), DownloadReport (PDF, 381 KB)

Optimization of Slice Encoding in Gobra
Zdenek Snajdr FS 2023
DownloadDescription (PDF, 120 KB), DownloadReport (PDF, 520 KB)

Adding Support for Generic Types in a Program Verifier for Go
Colin Pfingstl, SS 2023
DownloadDescription (PDF, 125 KB), DownloadReport (PDF, 806 KB)

Formally Validating the CFG Optimization Phase of the Boogie Program Verifier
Lukas Himmelreich, SS 2023
DownloadDescription (PDF, 215 KB), DownloadReport (PDF, 637 KB)

Information Hiding and Package Abstraction for Go
Tommy Ho, SS 2023
DownloadDescription (PDF, 128 KB), DownloadReport (PDF, 825 KB)

Verifying Vulnerability Fixes in a Rust Verifier
Olivia Furrer, SS 2023
DownloadDescription (PDF, 318 KB), DownloadReport (PDF, 1.1 MB)

Evaluating and Documenting a Rust Verifier
Patrick Muntwiler, SS 2023
DownloadDescription (PDF, 62 KB), DownloadReport (PDF, 479 KB)

Translating Pedagogical Exercises to Viper’s Go Front-end
Timon Egli, AS 2022
DownloadDescription (PDF, 77 KB), DownloadReport (PDF, 1.1 MB)

Advanced Logical Proofs in a Verifier
Dina Weiersmüller, AS 2022
DownloadDescription (PDF, 355 KB), DownloadReport (PDF, 672 KB)

Practical Inlining in Viper
Matthias Schenk, AS 2022
DownloadDescription (PDF, 293 KB), DownloadReport (PDF, 903 KB)

Towards Verifying Real-World Rust Programs
Jonas Maier, AS 2022
DownloadDescription (PDF, 63 KB), DownloadReport (PDF, 283 KB)

Formally Validating the AST-to-CFG Phase of the Boogie Program Verifier
Aleksandar Hubanov, SS 2022
DownloadDescription (PDF, 149 KB), DownloadReport (PDF, 802 KB)

Counterexamples for Complex Data Structures for a Rust Verifier
Markus Limbeck, SS 2022
DownloadDescription (PDF, 80 KB), DownloadReport (PDF, 1.1 MB)

Sound Automation of Magic Wands in a Symbolic-Execution Verifier
Nicola Widmer, SS 2022
DownloadDescription (PDF, 226 KB), DownloadReport (PDF, 880 KB)

Verifying Rust Programs Using Floating-Point Numbers and Bitwise Operations
Lukas Friedlos, SS 2021
DownloadDescription (PDF, 76 KB), DownloadReport (PDF, 255 KB)

Automatically Testing Solvers for String and Regular Expressions Constraints
Sebastian Kühne, SS 2021
DownloadDescription (PDF, 123 KB), Report

Program Verification in Continuous Integration Workflows
Johannes Gasser, AS 2021
DownloadDescription (PDF, 127 KB), DownloadReport (PDF, 1004 KB)

Parser for Go Programs and Specification
Nico Berling, AS 2021
DownloadDescription (PDF, 105 KB), DownloadReport (PDF, 814 KB)

Counterexamples for a Rust Verifier
Cedric Hegglin, AS 2021
DownloadDescription (PDF, 163 KB), DownloadReport (PDF, 640 KB)

Automatically Testing SMT Solvers
Olivier Becker, AS 2021
DownloadDescription (PDF, 132 KB), DownloadReport (PDF, 689 KB)

Verifying Termination of Go Programs
Cheng Xuan, FS 2021
DownloadDescription (PDF, 63 KB), DownloadReport (PDF, 938 KB)

Recovering From Verification Failures
Josua Stuck, FS 2021
DownloadDescription (PDF, 190 KB), DownloadReport (PDF, 836 KB)

Performance Improvements of a Program Verifier
Fabian Bösiger, FS 2021
DownloadDescription (PDF, 137 KB), DownloadReport (PDF, 570 KB)

An Abstract Representation for Wildcard Permissions in Viper
Yanick Bachmann, FS 2021
DownloadDescription (PDF, 222 KB), DownloadReport (PDF, 1016 KB)

Cloud-based Verification IDE
Dennis Buitendijk, FS 2021
DownloadDescription (PDF, 111 KB), DownloadReport (PDF, 1.6 MB)

Verification of Practical Go Programs
Luca Halm, FS 2021
DownloadDescription (PDF, 143 KB), DownloadReport (PDF, 1.8 MB)

Extending a Go Verifier with Algebraic Data Types
Paul Dahlke, FS 2021
DownloadDescription (PDF, 136 KB), DownloadReport (PDF, 2.3 MB)

Counterexample Generation in Gobra
Fabio Aliberti, FS 2021
DownloadDescription (PDF, 234 KB), DownloadReport (PDF, 1 MB)

Explaining Unsatisfiability Proofs through Examples
Pascal Strebel, SS 2021
DownloadDescription (PDF, 1.1 MB), DownloadReport (PDF, 1.8 MB)

Reasoning about Nondeterministic Collections
Bogdan Gadzhylov, FS 2020
DownloadDescription (PDF, 148 KB), DownloadReport (PDF, 382 KB)

Optimization of Viper-Based Verifier
Till Arnold, FS 2020
DownloadDescription (PDF, 80 KB), DownloadReport (PDF, 720 KB)

A Better SMT Language: Design & Tooling
Nico Daryll Hänggi, SS 2020
DownloadDescription (PDF, 228 KB), DownloadReport (PDF, 2.4 MB)

Universal Library Components for Verification IDE Components
Valentin Racine, SS 2020
DownloadDescription (PDF, 389 KB), DownloadReport (PDF, 2.5 MB)

Developing IDE Support for a Rust Verifier
Julian Dunskus, SS 2020
DownloadDescription (PDF, 91 KB), DownloadReport (PDF, 656 KB)

IDE Support for a Golang Verifier
Silas Walker, SS 2020
DownloadDescription (PDF, 136 KB), DownloadReport (PDF, 1.9 MB)

Lightweight automatic loop invariant selection
Pavol Pozdnyakov, SS 2019
DownloadDescription (PDF, 86 KB), DownloadReport (PDF, 738 KB)

Optimization of a Symbolic Execution based Program Verifier
Moritz Knüsel, SS 2019
DownloadDescription (PDF, 103 KB), DownloadReport (PDF, 976 KB)

Towards better Function Axiomatization in a Symbolic-execution-based Verifier
Mauro Bringolf, SS 2019
DownloadDescription (PDF, 156 KB), DownloadReport (PDF, 786 KB)

Static Analysis of GPU Kernel Performance Hyperproperties
Mathias Blarer, SS 2019
DownloadDescription (PDF, 151 KB), DownloadReport (PDF, 576 KB)

Simple Explanation of Complex Lifetime Errors in Rust
David Blaser, SS 2019
DownloadDescription (PDF, 378 KB), DownloadReport (PDF, 1.8 MB)

Tool Support for Termination Proofs
Fabio Streun, AS 2018
DownloadDescription (PDF, 150 KB), DownloadReport (PDF, 1.1 MB)

Optimisation of a Deductive Program Verifier
Philippe Voinov, AS 2018
DownloadDescription (PDF, 25 KB), DownloadReport (PDF, 810 KB)

Semantic Querying of Rust Code
Nicolas Winkler, AS 2018
DownloadDescription (PDF, 53 KB), DownloadReport (PDF, 754 KB)

Visualization of Reference Lifetimes in Rust
Dominic Dietler, AS 2018
DownloadDescription (PDF, 77 KB), DownloadReport (PDF, 528 KB)

Specification and Automated Reasoning for Datastructure Comprehensions
Tierry Hörmann, SS18
DownloadDescription (PDF, 98 KB), DownloadReport (PDF, 538 KB)

Adding Generalized Magic Wand Support to a Verification-Condition-Generation-Based Verifier
Ahmed Gamal Khedr, SS 2018
DownloadDescription (PDF, 83 KB), DownloadReport (PDF, 983 KB)

Advancing Non-Standard Permission Utilisation in Program Verification
Tobias Brodmann, SS 2018
DownloadDescription (PDF, 137 KB), DownloadReport (PDF, 751 KB)

Static Verification of the SCION Router Implementation
Sascha Forster, SS 2018
DownloadDescription (PDF, 173 KB), DownloadReport (PDF, 690 KB)

Deductive Verification of Imperative Graph Algorithms
Gishor Sivanrupan, SS 2018
DownloadDescription (PDF, 126 KB), DownloadReport (PDF, 3.1 MB)

Usage Analysis of Data Stored in Map Data Structures
Lowis Engel, SS 2018
DownloadDescription (PDF, 216 KB), DownloadReport (PDF, 1.1 MB)

Automatic Inference of Hyperproperties
Christian Knabenhans, SS 2018
DownloadDescription (PDF, 146 KB), DownloadReport (PDF, 780 KB)

Automated Checking of Implicit Assumptions on Textual Data
Radwa Sherif Abdelbar, SS 2018
DownloadDescription (PDF, 158 KB), DownloadReport (PDF, 1.9 MB)

Abstract Read Permission Support for an Automatic Python Verifier
Benjamin Schmid, SS 2017
DownloadDescription (PDF, 81 KB), DownloadReport (PDF, 444 KB)

Static Type Inference for Python
Mostafa Hassan, SS 2017
DownloadDescription (PDF, 140 KB), DownloadReport (PDF, 518 KB)

Generalized Verification Support for Magic Wands
Nils Becker, SS 2017
DownloadDescription (PDF, 166 KB), DownloadReport (PDF, 510 KB)

Towards Customizability of a Symbolic-Execution-Based Program Verifier
Robin Sierra, SS 2017
DownloadDescription (PDF, 164 KB), DownloadReport (PDF, 769 KB)

Checking Termination of Abstraction Functions
Patrick Gruntz, SS 2017
DownloadDescription (PDF, 88 KB), DownloadReport (PDF, 952 KB)

Supporting Sequence Axiomatization on the SMT Solver Level for the Viper Project
Lukas Schär, AS2016
DownloadDescription (PDF, 104 KB), DownloadReport (PDF, 919 KB)

A Prototype Verifier for Weak Memory Reasoning
Christiane Goltz, AS 2016 
DownloadDescription (PDF, 34 KB), DownloadReport (PDF, 769 KB)

Developing a Web-Based Hoare Logic Proof Assistant
Flavio Goldener, AS 2015
DownloadDescription (PDF, 87 KB), DownloadReport (PDF, 3.3 MB)

Recording Symbolic Executions

Andreas Buob, SS 2015
DownloadDescription (PDF, 70 KB), DownloadReport (PDF, 326 KB)

Developing an Interactive, Web-Based Tutorial for an Intermediate Verification Language

Mathias Birrer, SS 2015
DownloadDescription (PDF, 539 KB), DownloadReport (PDF, 3.6 MB)

Incremental Symbolic Execution

Roger Koradi, SS 2015
DownloadDescription (PDF, 114 KB), DownloadReport (PDF, 1.3 MB)

Adding Magic Wand Support to Carbon

Gaurav Parthasarathy, SS 2015
DownloadDescription (PDF, 70 KB), DownloadReport (PDF, 1.1 MB)

Tree-based Version Control in Envision

Balz Guenat, SS 2015
DownloadDescription (PDF, 77 KB), DownloadReport (PDF, 1.2 MB)  

Enhancing the visual documentation artifacts in Envision

Sascha Dinkel, SS 2014
DownloadDescription (PDF, 142 KB), DownloadReport (PDF, 6.6 MB)

Closure verification in an automated fractional permission setting

Fabian Meier, SS 2014
DownloadDescription (PDF, 340 KB), DownloadReport (PDF, 756 KB)

Verifying Scala's Vals and Lazy Vals

Simon Fritsche, SS 2014
DownloadDescription (PDF, 70 KB), DownloadReport (PDF, 478 KB)

Semantic Zoom Support for Envision

Patrick Lüthi, AS 2013
DownloadDescription (PDF, 205 KB), DownloadReport (PDF, 890 KB)

Supporting documentation artifacts in Envision

Jonas Trappenberg, SS 2013
DownloadDescription (PDF, 86 KB), DownloadReport (PDF, 707 KB)

C++ Support in Envision

Lukas Vogel, SS 2013
DownloadDescription (PDF, 106 KB), DownloadReport (PDF, 403 KB)

Induction and Termination of Functions for Automatic Program Verification

Benjamin Fischer, SS 2013
DownloadDescription (PDF, 57 KB), DownloadReport (PDF, 322 KB)

Dynamic test generation with static fields and initializers

Patrick Emmisberger, SS 2013
DownloadDescription (PDF, 95 KB), DownloadReport (PDF, 496 KB)

Declarative API for Defining Visualization in Envision

Andrea Helfenstein, AS 2012
DownloadDescription (PDF, 66 KB), DownloadReport (PDF, 466 KB)

Synthesizing Method Sequences to Detect Object Invariant Violations

Timon Gehr, SS 2013
DownloadDescription (PDF, 74 KB), DownloadReport (PDF, 260 KB)

Runtime Checking for Chalice

Heinz Hegi, SS 2013
DownloadDescription (PDF, 56 KB), DownloadReport (PDF, 272 KB)

Verifying Separation Logic Contracts in Chalice

Daniel Jost, SS 2013
DownloadDescription (PDF, 58 KB), DownloadReport (PDF, 378 KB)

Translating Chalice into SIL

Christian Klauser, AS 2012
DownloadDescription (PDF, 58 KB), DownloadReport (PDF, 600 KB)

Developing a common web interface to various verification tools

Roland Meyer, SS 2012
DownloadDescription (PDF, 57 KB), DownloadReport (PDF, 508 KB)

Interfacing TVLA and Sample

Raphael Fuchs, SS 2011
DownloadDescription (PDF, 30 KB), DownloadReport (PDF, 311 KB)

Improving Permission-Based Verification of Concurrent Programs with Chalice

Stefan Heule, AS 2010
DownloadDescription (PDF, 131 KB), DownloadReport (PDF, 891 KB)

A Standard Library for Gobra
Daniel Nezamabadi, SS 2024
DownloadDescription (PDF, 451 KB), DownloadReport (PDF, 612 KB)

Verifying the IO Behaviour of the SCION Router
Markus Limbeck, SS 2024
DownloadDescription (PDF, 451 KB), DownloadReport (PDF, 625 KB)

Formally Deriving an Equirecursive Viper Semantics via a Least Fixed Point Predicate Interpretation
Hongyi Ling, SS 2023
DownloadDescription (PDF, 258 KB)

Adding Debugging Functionality to Viper
Andrea Keusch, SS 2023
DownloadDescription (PDF, 141 KB)

Extending IDE Integration of a Rust Verifier
Joseph Thommes, SS 2023
DownloadDescription (PDF, 183 KB)

Extending IDE Integration of a Rust Verifier
Cedric Hegglin, SS 2023
DownloadDescription (PDF, 183 KB)

Code Reachability and Soundness Verification Using Refute in Prusti
Simon Hrabec, AS 2022
DownloadDescription (PDF, 198 KB)

Improving User-Defined Permission Models in Viper
Anqi Li, AS 2022
DownloadDescription (PDF, 119 KB), DownloadReport (PDF, 496 KB)

Verifying Go's Standard Library
Adrian Jenny, AS 2022
DownloadDescription (PDF, 82 KB), DownloadReport (PDF, 1011 KB)

Adding Algebraic Data Types to a Verification Language
Allesandro Maissen, SS 2022
DownloadDescription (PDF, 113 KB), DownloadReport (PDF, 867 KB)

Supporting Alternative SMT Solvers in Viper
Lasse F. Wolff Anthony, FS 2022
DownloadDescription (PDF, 107 KB), DownloadReport (PDF, 5.9 MB)

Adding Native Support for Havoc in Viper
Daniel Zhang, AS 2022
DownloadDescription (PDF, 101 KB), DownloadReport (PDF, 447 KB)




Place Capabilities Summaries for Rust Programs

Dylan Wolff, AS 2019
DownloadDescription (PDF, 100 KB), DownloadReport (PDF, 227 KB)

Verifying weak memory programs in the Viper ecosystem

Anouk Paradis, SS 2019
DownloadDescription (PDF, 70 KB), DownloadReport (PDF, 264 KB)

Applying and Extending the Weak-Memory Logic FSL++

Gaurav Parthasarathy, SS 2017
DownloadDescription (PDF, 78 KB), DownloadReport (PDF, 1.2 MB)

Task specific views in Envision

Cyril Steimer, SS 2015
DownloadDescription (PDF, 91 KB), DownloadReport (PDF, 1.3 MB)

Integrating dynamic test generation with sound verification

Patrick Emmisberger, AS 2014
DownloadDescription (PDF, 79 KB), DownloadReport (PDF, 917 KB)

Debugging in Envision

Lukas Vogel , AS 2014
DownloadDescription (PDF, 100 KB), DownloadReport (PDF, 1.1 MB)

Verifying Scala Traits

Malte Schwerhoff, SS 2010
DownloadDescription (PDF, 158 KB), DownloadReport (PDF, 492 KB)

Implementation of Closures in DAFNY

Alexandru Dima, SS 2010
DownloadDescription (PDF, 18 KB), DownloadReport (PDF, 272 KB)

A feasability study for a general-purpose visual programming system

Dimitar Asenov, SS 2010
DownloadDescription (PDF, 81 KB), DownloadReport (PDF, 4.5 MB)

Translating Java bytecode to Simple

Roman Scheidegger, HS 2009
DownloadReport (PDF, 200 KB)

Slicing Spec# Programs

Sebastian Groessi, HS 2007
DownloadDescription (PDF, 28 KB), DownloadReport (PDF, 236 KB)

Extending supported language subset of Jive

David Steiger, HS 2007
DownloadDescription (PDF, 253 KB), DownloadReport (PDF, 519 KB)

Usability Evaluation of Jive

Martin Bill, WS 2006/07
DownloadDescription (PDF, 35 KB)

Testing Tool for Compilers

Dominique Schneider, WS 2006/07
DownloadDescription (PDF, 21 KB), DownloadReport (PDF, 414 KB)

Integration of Universe Type System Tools into Eclipse

Paolo Bazzi, SS 2006
DownloadDescription (PDF, 18 KB), DownloadReport (PDF, 840 KB)

Case study in the Boogie Methodology

Olivier Girard, SS 2006
DownloadDescription (PDF, 53 KB), DownloadReport (PDF, 672 KB)

Mono's System.Collection Classes: A Spec# Case Study

Benjamin Lutz, SS 2006
DownloadDescription (PDF, 40 KB), DownloadReport (PDF, 860 KB)

MultiJava, JML and Generics

Ovidio Mallo, SS 2006
DownloadDescription (PDF, 29 KB), DownloadReport (PDF, 375 KB)

Universe Type System for Eiffel

Annetta Schaad, SS 2006
DownloadDescription (PDF, 24 KB), DownloadReport (PDF, 847 KB)

Integrating Simplify into Jive

Yoshimi Takano, SS 2006
DownloadDescription (PDF, 42 KB)

Implementing Purity and Side Effect Analysis for Java Programs

David Graf, WS 2005/06
DownloadDescription (PDF, 56 KB), DownloadReport (PDF, 1 MB)

Interaction with Ownership Graphs

Marco Meyer, WS 2005/06
DownloadDescription (PDF, 25 KB), DownloadReport (PDF, 325 KB)

Translation of object-oriented programs into guarded commands

Samuel Burri, SS 2005
DownloadReport (PDF, 243 KB)

Design Patterns in Peer-to-Peer Systems

Dominik Grolimund, SS 2005
DownloadDescription (PDF, 55 KB), DownloadReport (PDF, 447 KB)

Welldefinedness and expressiveness of JML specifications

Adrian Moos, SS 2005
DownloadDescription (PDF, 14 KB), DownloadReport (PDF, 288 KB)

Implementation of a Universe type checker in ESC/Java2

Dirk Wellenzohn, SS 2005
DownloadDescription (PDF, 45 KB), DownloadReport (PDF, 402 KB)

Generating Proof Obligations from JML Specifications

Ghislain Fourny, WS 2004/05
DownloadDescription (PDF, 109 KB), DownloadReport (PDF, 373 KB)

Transformation of Java Card into Diet Java Card

Erich Laube, WS 2004/05
DownloadDescription (PDF, 18 KB), DownloadReport (PDF, 381 KB)

Bytecode support for the Universe type system and compiler

Alex Suzuki, WS 2004/05
DownloadDescription (PDF, 28 KB), DownloadReport (PDF, 382 KB)

A Logic for Bytecode and the Translation of Proofs from Sequential Java

Fabian Bannwart, SS 2004
DownloadDescription (PDF, 55 KB), DownloadReport (PDF, 668 KB)

Static Fields in the Universe Type System

Marcello Miragliotta, SS 2004
DownloadDescription (PDF, 9 KB), DownloadReport (PDF, 387 KB)

Runtime checks for the Universe Type System

Daniel Schregenberger, SS 2004
DownloadDescription (PDF, 27 KB), DownloadReport (PDF, 809 KB)

JavaScript has been disabled in your browser