Completed Projects

Enhancing Deductive Verification of Unbounded Heap Data Structures
Markus Limbeck SS 2025
Download Description (PDF, 186 KB), Download Report (PDF, 987 KB)

Cross-Language Verification of Python Modules Written in C
Etienne Birling, SS 2025
Download Description (PDF, 199 KB), Download Report (PDF, 743 KB)

Hyper Separation Logic (external)
Trayan Gospodinov, SS 2024
Download Description (PDF, 236 KB)

A Semantics for Predicates in Automated Separation Logic Verifiers
Yushuo Xiao, SS 2024
Download Description (PDF, 466 KB), Download Report (PDF, 174 KB)

A General Approach to Verify Viper Front-ends
Hongyi Ling, SS 2024
Download Description (PDF, 44 KB), Download Report (PDF, 942 KB)

Verification² of the Authentic Digital EMblem
Lasse Meinen, SS 2024
Download Description (PDF, 154 KB), Download Report (PDF, 617 KB)

Large Language Models for Verified Programs
Omkar Zade, SS 2024
Download Description (PDF, 150 KB), Download Report (PDF, 786 KB)

Verification of Python Code with a Dynamic Object Model
Edgars Vitolins, AS 2023
Download Description (PDF, 126 KB), Download Report (PDF, 549 KB)

Verification of Object Invariants in the Presence of Unverified Code
Frédéric Necker, AS 2023
Download Description (PDF, 135 KB), Download Report (PDF, 683 KB)

Automated verification of a Rust differential privacy library
Till Arnold, AS 2023
Download Description (PDF, 80 KB), Download Report (PDF, 448 KB)

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

An Automatic Program Verifier for Hyperproperties
Anqi Li, AS 2023
Download Description (PDF, 135 KB), Download Report (PDF, 820 KB)

A Linear Typesystem for a Go Verifier
Liming Han, SS 2023
Download Description (PDF, 165 KB), Download Report (PDF, 1.1 MB)

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

Using Verification Techniques to Synthesise Rust Programs
Fabian Bösiger, SS 2023
Download Description (PDF, 189 KB), Download Report (PDF, 548 KB)

Ownership Typesystem based Optimisations for Rust
Janis Peyer, SS 2023
Download Description (PDF, 83 KB), Download Report (PDF, 781 KB)

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

Proving Refinement in a Rust Verifier
Jan Schär, SS 2023
Download Description (PDF, 122 KB), Download Report (PDF, 577 KB)

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

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

Automatically Generating Memory Safety Certiﬁcates for Rust Programs
Pascal Huber, SS 2022
Download Description (PDF, 68 KB), Download Report (PDF, 641 KB)

Verification of closures for Go programs
Stefano Milizia, SS 2022
Download Description (PDF, 168 KB), Download Report (PDF, 392 KB)

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

Adding Algebraic Data Types to a Verification Language
Allesandro Maissen, SS 2022
Download Description (PDF, 113 KB), Download Report (PDF, 867 KB)

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

Automatically Generating Java Benchmarks with Known Errors
Madalina Hurmuz, AS 2021
Download Description (PDF, 178 KB), Download Report (PDF, 1.1 MB)

Reasoning about Complexities in a Rust Verifier
Lowis Engel, AS 2021
Download Description (PDF, 170 KB), Download Report (PDF, 697 KB)

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

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

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

Extended Support for Borrowing and Lifetimes in Prusti
Lorenz Gorse, SS 2020
Download Description (PDF, 270 KB), Download Report (PDF, 1004 KB)

Assertion-based Testing of Go Programs
Eva Charlotte Mayer, SS 2020
Download Description (PDF, 165 KB), Download Report (PDF, 789 KB)

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

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

Verification of Closures in Rust Programs
Fabian Wolff, SS 2020
Download Description (PDF, 208 KB), Download Report (PDF, 821 KB)

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

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

Inference of Progressive Loop Invariants for Array Programs
Nils Becker, SS 2020
Download Description (PDF, 237 KB), Download Report (PDF, 802 KB)

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

Profiling Symbolic Execution
Linard Arquint, SS 2019
Download Description (PDF, 159 KB), Download Report (PDF, 2.4 MB)

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

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

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

SMT models for verification debugging
Cédric Stoll, AS 2018
Download Description (PDF, 94 KB), Download Report (PDF, 3.8 MB)

Verification of Rust Generics, Typestates, and Traits
Matthias Erdin, SS 2018
Download Description (PDF, 146 KB), Download Report (PDF, 717 KB)

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

Visual Debugging for Symbolic Execution
Alessio Aurecchia, SS 2018
Download Description (PDF, 313 KB), Download Report (PDF, 8.7 MB)

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

Modular Verification of Message Passing Programs
Gaurav Parthasarathy, AS 2017
Download Description (PDF, 68 KB), Download Report (PDF, 1.6 MB)

Automated Generation of Data Quality Checks
Madelin Schumacher, AS 2017
Download Description (PDF, 165 KB), Download Report (PDF, 1.3 MB)

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

Proving Temporal Properties by Abstract Interpretation
Samuel Ueltschi, SS 2017
Download Description (PDF, 107 KB), Download Report (PDF, 901 KB)

Static Program Analysis of Data Usage Properties
Simon Wehrli, SS 2017
Download Description (PDF, 218 KB), Download Report (PDF, 858 KB)

Interprocedural Static Analysis by Abstract Interpretation
Flurin Rindisbacher, SS 2017
Download Description (PDF, 127 KB), Download Report (PDF, 1.5 MB)

Serializability checking for MongoDB clients
Johannes Baum, AS 2016
Download Description (PDF, 125 KB), Download Report (PDF, 2.3 MB)

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

A Framework for Bidirectional Program Transformations
Simon Fritsche, AS 2016
Download Description (PDF, 105 KB), Download Report (PDF, 954 KB)

Analyzing Serializability of Cassandra Applications
Arthur Kurath, AS 2016
Download Description (PDF, 144 KB), Download Report (PDF, 1.3 MB)

A formal Semantics for Viper
Cyrill Gössi, SS 2016
Download Description (PDF, 58 KB), Download Report (PDF, 842 KB)

Testing program robustness against deviant behavior
Patrick Emmisberger, SS 2016
Download Description (PDF, 142 KB), Download Report (PDF, 1.6 MB)

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

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

Input-Output Verification in Viper
Vytautas Astrauskas, SS 2016
Download Description (PDF, 68 KB), Download Report (PDF, 455 KB)

Generalised Verification for Quantified Permissions
Nadja Müller, SS 2016
Download Description (PDF, 64 KB), Download Report (PDF, 506 KB)

From Viper to Grasshopper
Andrea Helfenstein, SS 2016
Download Description (PDF, 89 KB), Download Report (PDF, 393 KB)

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

Improving Code Reviews using the Envision IDE
Manuel Galbier, SS 2016
Download Description (PDF, 106 KB), Download Report (PDF, 8.2 MB)

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

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

Augmenting software development with information scripting
Lukas Vogel, AS 2015
Download Description (PDF, 153 KB), Download Report (PDF, 6.9 MB)

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

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

Verification of Finite Blocking in Chalice
Robert Meier, SS 2015
Download Description (PDF, 94 KB), Download Report (PDF, 481 KB)

Modular Verification of Finite Blocking
Christian Klauser, SS 2014
Download Description (PDF, 57 KB), Download Report (PDF, 1.3 MB)

Verification Condition Generation for the Intermediate Verification Language SIL

Stefan Heule, SS 2013
Download Description (PDF, 149 KB), Download Report (PDF, 941 KB)

Translating Scala to SIL

Bernhard Brodowsky, SS 2013
Download Description (PDF, 53 KB), Download Report (PDF, 463 KB)

Overapproximating the Cost of Loops

Daniel Schweizer, AS 2012
Download Description (PDF, 194 KB), Download Report (PDF, 542 KB)

Permission-Based Verification of Subclassing and Traits

Andres Bühlmann, AS 2012
Download Description (PDF, 114 KB), Download Report (PDF, 1.2 MB)

Debugging Symbolic Execution

Ivo Colombo, SS 2012
Download Description (PDF, 168 KB), Download Report (PDF, 1.8 MB)

Extensible Code Contracts for Scala

Rokas Matulis, SS 2012
Download Description (PDF, 105 KB), Download Report (PDF, 512 KB)

Translating Spec# Programs to C# with CodeContracts

Florian Egli, AS 2011
Download Description (PDF, 241 KB), Download Report (PDF, 2.4 MB)

Disjunction on Demand

Dominik Gabi, SS 2011
Download Description (PDF, 107 KB), Download Report (PDF, 1.5 MB)

Design and Implementation of Envision - a Visual Programming System

Dimitar Asenov, AS 2010
Download Description (PDF, 137 KB), Download Report (PDF, 2.2 MB)

Symbolic Execution for Chalice

Malte Schwerhoff, AS 2010
Download Description (PDF, 88 KB), Download Report (PDF, 685 KB)

Adding Closure Support to Chalice

Prateek Agarwal, SS 2010
Download Description (PDF, 121 KB), Download Report (PDF, 824 KB)

Automatic Verification of Concurrent Programs

Filip Wieladek, SS 2010
Download Description (PDF, 33 KB), Download Report (PDF, 732 KB)

Encoding Scala Programs for the Boogie Verifier

Valentin Wüstholz, SS 2009
Download Description (PDF, 82 KB), Download Report (PDF, 764 KB)

Implementation of Frozen Objects into Spec#

Florian Leu, SS 2009
Download Description (PDF, 33 KB), Download Report (PDF, 538 KB)

Software Engineering modules for Computer Science Talent Scout

Roman Fuchs, SS 2009
Download Description (PDF, 63 KB), Download Report (PDF, 1.4 MB)

Embedding JML-annotated Programs in the Coq Proof System

Andreas Kägi, WS 2008/2009
Download Description (PDF, 38 KB), Download Report (PDF, 593 KB)

Improving Cee and Ownership-Based Verification

Christoph Studer, 11/08 - 04/09
Download Description (PDF, 57 KB), Download Report (PDF, 857 KB)

Verification of Design Patterns

Simon Hofer, 09/08 - 02/09
Download Description (PDF, 71 KB), Download Report (PDF, 71 KB)

Verifying Spec# Delegates

Samuele Gantner, 03/08 - 09/08
Download Description (PDF, 140 KB), Download Report (PDF, 2 MB)

Counterexample Execution

Jürg Billeter, 02/08 - 08/08
Download Description (PDF, 45 KB), Download Report (PDF, 406 KB)

Translating invariant proofs between Spec# and JML

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

Error Reporting for Universe Types with Transfer

Benjamin Lutz, 01/08 - 05/08
Download Description (PDF, 41 KB), Download Report (PDF, 475 KB)

Implementing a Universe Type System for Scala

Manfred Stock, 08/07 - 01/08
Download Description (PDF, 47 KB), Download Report (PDF, 1 MB)

Inferring Universe annotations in the presence of ownership transfer

Annetta Schaad, 05/07 - 11/07
Download Description (PDF, 36 KB), Download Report (PDF, 3 MB)

Proving well-formedness of interface specifications

Geraldine von Roten, 04/07 - 10/07
Download Description (PDF, 30 KB), Download Report (PDF, 440 KB)

Using program slicing to improve error reporting in Boogie

Karin Freiermuth, 02/07 - 09/07
Download Description (PDF, 33 KB), Download Report (PDF, 476 KB)

Integration of a new VCGen in ESC/Java2

Claudia Brauchli, 03/07 - 09/07
Download Description (PDF, 31 KB), Download Report (PDF, 2.2 MB)

An Automated Program Verifier for Java Bytecode

Samuel Willimann, 03/07 - 09/07
Download Description (PDF, 69 KB), Download Report (PDF, 1.1 MB)

Runtime Support for Generics and Transfer in Universe Types

Mathias Ottiger, 02/07 - 08/07
Download Description (PDF, 39 KB), Download Report (PDF, 508 KB)

Generic Universe Types in JML

Robin Züger, 01/07 - 07/07
Download Description (PDF, 49 KB), Download Report (PDF, 2.7 MB)

Universe Type System for Scala

Daniel Schregenberger, 09/06 - 06/07
Download Description (PDF, 42 KB), Download Report (PDF, 935 KB)

Implementing Uniqueness and Ownership Transfer in the Universe Type System

Yoshimi Takano, 09/06 - 03/07
Download Description (PDF, 41 KB), Download Report (PDF, 781 KB)

An Isabelle Formalization of the Universe Type System

Martin Klebermass, 10/06 - 04/07
Download Description (PDF, 31 KB), Download Report (PDF, 611 KB)

Combining Runtime and Static Universe Type Inference

Andreas Fürer, 09/06 - 03/07
Download Description (PDF, 35 KB), Download Report (PDF, 1.4 MB)

Kangoo API for Web-Based Applications

Cristian Garcia, 09/06 - 03/07
Download Description (PDF, 11 KB), Download Report (PDF, 2.1 MB)

A Translator from BML annotated Java Bytecode to BoogiePL

Ovidio Mallo, WS 2006/07
Download Description (PDF, 34 KB), Download Report (PDF, 601 KB)

Formalization and implementation of translation from Java Bytecode to Guarded Commands

Alex Suzuki, 04/06 - 09/06
Download Description (PDF, 42 KB), Download Report (PDF, 924 KB)

Static Universe Type Inference using a SAT-Solver

Matthias Niklaus, 12/05 - 06/06
Download Description (PDF, 26 KB), Download Report (PDF, 1 MB)

Practical Runtime Universe Type Inference

Marco Bär, 11/05 - 05/06
Download Description (PDF, 26 KB), Download Report (PDF, 1.5 MB)

Ownership in Design Patterns

Stefan Nägeli, 09/05 - 03/06
Download Description (PDF, 51 KB), Download Report (PDF, 4.4 MB)

Design and Implementation of a JML Frontend for Boogie

Erich Laube, WS 2005/06
Download Description (PDF, 33 KB), Download Report (PDF, 487 KB)

Ownership-based Program Verification in Jive

Ronny Zakheijm, WS 2005/06
Download Description (PDF, 33 KB), Download Report (PDF, 649 KB)

Changing Software Correctly

Fabian Bannwart, WS 2005/06
Download Description (PDF, 46 KB), Download Report (PDF, 2.4 MB)

Static Universe Type Inference

Nathalie Kellenberger, 04/05 - 10/05
Download Description (PDF, 74 KB), Download Report (PDF, 807 KB)

Runtime Universe Type Inference

Frank Lyner, 01/05 - 07/05
Download Description (PDF, 29 KB), Download Report (PDF, 1.7 MB)

Applying the Universe Type System to an Industrial Application

Thomas Hächler, 09/04 - 03/05
Download Description (PDF, 36 KB), Download Report (PDF, 1.8 MB)

Developing a Best-Practice Student Project Template for a Software Engineering Course
João Patrick Lopes Müller, AS 2024
Download Description (PDF, 103 KB), Download Report (PDF, 385 KB)

Specifying and Verifying Static Initialization in Deductive Program Verifiers
Patricia Firlejczyk, SS 2024
Download Description (PDF, 131 KB), Download Report (PDF, 838 KB)

Verifying Parts of the Go Standard Library
Conradin Laux, AS 2024
Download Description (PDF, 261 KB), Download Report (PDF, 1.9 MB)

Separating Magic Wands and Functional Properties
Manuel Dublanc, SS 2024
Download Description (PDF, 135 KB), Download Report (PDF, 857 KB)

Enhancing Proof Search Algorithms for Synthesising Rust Programs
Eric Gademann, SS 2024
Download Description (PDF, 209 KB), Download Report (PDF, 559 KB)

Formal Verification of Dynamic Programming Algorithms
Athena Wang, SS 2024
Download Description (PDF, 151 KB), Download Report (PDF, 504 KB)

Specification of Python Math and Data Science Libraries
Pascal Devenoge, SS 2024
Download Description (PDF, 173 KB), Download Report (PDF, 3.6 MB)

Developing Tool Support for Understanding Quantifier Instantiations
Oskari Jyrkinen, AS 2023
Download Description (PDF, 191 KB), Download Report (PDF, 3.6 MB)

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

Translating Pedagogical Verification Exercises to Viper
Elias Ruff, AS 2023
Download Description (PDF, 210 KB), Download Report (PDF, 687 KB)

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

Translating Pegagogical Verification Exercises to Viper
Benjamin Frei, SS 2023
Download Description (PDF, 331 KB), Download Report (PDF, 1.9 MB)

Advanced Counterexample Generation in Viper
Raoul van Doren, SS 2023
Download Description (PDF, 164 KB), Download Report (PDF, 362 KB)

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

Optimization of Slice Encoding in Gobra
Zdenek Snajdr FS 2023
Download Description (PDF, 120 KB), Download Report (PDF, 520 KB)

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

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

Information Hiding and Package Abstraction for Go
Tommy Ho, SS 2023
Download Description (PDF, 128 KB), Download Report (PDF, 825 KB)

Verifying Vulnerability Fixes in a Rust Verifier
Olivia Furrer, SS 2023
Download Description (PDF, 318 KB), Download Report (PDF, 1.1 MB)

Evaluating and Documenting a Rust Verifier
Patrick Muntwiler, SS 2023
Download Description (PDF, 62 KB), Download Report (PDF, 479 KB)

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

Advanced Logical Proofs in a Verifier
Dina Weiersmüller, AS 2022
Download Description (PDF, 355 KB), Download Report (PDF, 672 KB)

Practical Inlining in Viper
Matthias Schenk, AS 2022
Download Description (PDF, 293 KB), Download Report (PDF, 903 KB)

Towards Verifying Real-World Rust Programs
Jonas Maier, AS 2022
Download Description (PDF, 63 KB), Download Report (PDF, 283 KB)

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

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

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

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

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

Program Verification in Continuous Integration Workflows
Johannes Gasser, AS 2021
Download Description (PDF, 127 KB), Download Report (PDF, 1004 KB)

Parser for Go Programs and Specification
Nico Berling, AS 2021
Download Description (PDF, 105 KB), Download Report (PDF, 814 KB)

Counterexamples for a Rust Verifier
Cedric Hegglin, AS 2021
Download Description (PDF, 163 KB), Download Report (PDF, 640 KB)

Automatically Testing SMT Solvers
Olivier Becker, AS 2021
Download Description (PDF, 132 KB), Download Report (PDF, 689 KB)

Verifying Termination of Go Programs
Cheng Xuan, FS 2021
Download Description (PDF, 63 KB), Download Report (PDF, 938 KB)

Recovering From Verification Failures
Josua Stuck, FS 2021
Download Description (PDF, 190 KB), Download Report (PDF, 836 KB)

Performance Improvements of a Program Verifier
Fabian Bösiger, FS 2021
Download Description (PDF, 137 KB), Download Report (PDF, 570 KB)

An Abstract Representation for Wildcard Permissions in Viper
Yanick Bachmann, FS 2021
Download Description (PDF, 222 KB), Download Report (PDF, 1016 KB)

Cloud-based Verification IDE
Dennis Buitendijk, FS 2021
Download Description (PDF, 111 KB), Download Report (PDF, 1.6 MB)

Verification of Practical Go Programs
Luca Halm, FS 2021
Download Description (PDF, 143 KB), Download Report (PDF, 1.8 MB)

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

Counterexample Generation in Gobra
Fabio Aliberti, FS 2021
Download Description (PDF, 234 KB), Download Report (PDF, 1 MB)

Explaining Unsatisfiability Proofs through Examples
Pascal Strebel, SS 2021
Download Description (PDF, 1.1 MB), Download Report (PDF, 1.8 MB)

Reasoning about Nondeterministic Collections
Bogdan Gadzhylov, FS 2020
Download Description (PDF, 148 KB), Download Report (PDF, 382 KB)

Optimization of Viper-Based Verifier
Till Arnold, FS 2020
Download Description (PDF, 80 KB), Download Report (PDF, 720 KB)

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

Universal Library Components for Verification IDE Components
Valentin Racine, SS 2020
Download Description (PDF, 389 KB), Download Report (PDF, 2.5 MB)

Developing IDE Support for a Rust Verifier
Julian Dunskus, SS 2020
Download Description (PDF, 91 KB), Download Report (PDF, 656 KB)

IDE Support for a Golang Verifier
Silas Walker, SS 2020
Download Description (PDF, 136 KB), Download Report (PDF, 1.9 MB)

Lightweight automatic loop invariant selection
Pavol Pozdnyakov, SS 2019
Download Description (PDF, 86 KB), Download Report (PDF, 738 KB)

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

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

Static Analysis of GPU Kernel Performance Hyperproperties
Mathias Blarer, SS 2019
Download Description (PDF, 151 KB), Download Report (PDF, 576 KB)

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

Tool Support for Termination Proofs
Fabio Streun, AS 2018
Download Description (PDF, 150 KB), Download Report (PDF, 1.1 MB)

Optimisation of a Deductive Program Verifier
Philippe Voinov, AS 2018
Download Description (PDF, 25 KB), Download Report (PDF, 810 KB)

Semantic Querying of Rust Code
Nicolas Winkler, AS 2018
Download Description (PDF, 53 KB), Download Report (PDF, 754 KB)

Visualization of Reference Lifetimes in Rust
Dominic Dietler, AS 2018
Download Description (PDF, 77 KB), Download Report (PDF, 528 KB)

Specification and Automated Reasoning for Datastructure Comprehensions
Tierry Hörmann, SS18
Download Description (PDF, 98 KB), Download Report (PDF, 538 KB)

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

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

Static Verification of the SCION Router Implementation
Sascha Forster, SS 2018
Download Description (PDF, 173 KB), Download Report (PDF, 690 KB)

Deductive Verification of Imperative Graph Algorithms
Gishor Sivanrupan, SS 2018
Download Description (PDF, 126 KB), Download Report (PDF, 3.1 MB)

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

Automatic Inference of Hyperproperties
Christian Knabenhans, SS 2018
Download Description (PDF, 146 KB), Download Report (PDF, 780 KB)

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

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

Static Type Inference for Python
Mostafa Hassan, SS 2017
Download Description (PDF, 140 KB), Download Report (PDF, 518 KB)

Generalized Verification Support for Magic Wands
Nils Becker, SS 2017
Download Description (PDF, 166 KB), Download Report (PDF, 510 KB)

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

Checking Termination of Abstraction Functions
Patrick Gruntz, SS 2017
Download Description (PDF, 88 KB), Download Report (PDF, 952 KB)

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

A Prototype Verifier for Weak Memory Reasoning
Christiane Goltz, AS 2016
Download Description (PDF, 34 KB), Download Report (PDF, 769 KB)

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

Recording Symbolic Executions

Andreas Buob, SS 2015
Download Description (PDF, 70 KB), Download Report (PDF, 326 KB)

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

Mathias Birrer, SS 2015
Download Description (PDF, 539 KB), Download Report (PDF, 3.6 MB)

Incremental Symbolic Execution

Roger Koradi, SS 2015
Download Description (PDF, 114 KB), Download Report (PDF, 1.3 MB)

Adding Magic Wand Support to Carbon

Gaurav Parthasarathy, SS 2015
Download Description (PDF, 70 KB), Download Report (PDF, 1.1 MB)

Tree-based Version Control in Envision

Balz Guenat, SS 2015
Download Description (PDF, 77 KB), Download Report (PDF, 1.2 MB)

Enhancing the visual documentation artifacts in Envision

Sascha Dinkel, SS 2014
Download Description (PDF, 142 KB), Download Report (PDF, 6.6 MB)

Closure verification in an automated fractional permission setting

Fabian Meier, SS 2014
Download Description (PDF, 340 KB), Download Report (PDF, 756 KB)

Verifying Scala's Vals and Lazy Vals

Simon Fritsche, SS 2014
Download Description (PDF, 70 KB), Download Report (PDF, 478 KB)

Semantic Zoom Support for Envision

Patrick Lüthi, AS 2013
Download Description (PDF, 205 KB), Download Report (PDF, 890 KB)

Supporting documentation artifacts in Envision

Jonas Trappenberg, SS 2013
Download Description (PDF, 86 KB), Download Report (PDF, 707 KB)

C++ Support in Envision

Lukas Vogel, SS 2013
Download Description (PDF, 106 KB), Download Report (PDF, 403 KB)

Induction and Termination of Functions for Automatic Program Verification

Benjamin Fischer, SS 2013
Download Description (PDF, 57 KB), Download Report (PDF, 322 KB)

Dynamic test generation with static fields and initializers

Patrick Emmisberger, SS 2013
Download Description (PDF, 95 KB), Download Report (PDF, 496 KB)

Declarative API for Defining Visualization in Envision

Andrea Helfenstein, AS 2012
Download Description (PDF, 66 KB), Download Report (PDF, 466 KB)

Synthesizing Method Sequences to Detect Object Invariant Violations

Timon Gehr, SS 2013
Download Description (PDF, 74 KB), Download Report (PDF, 260 KB)

Runtime Checking for Chalice

Heinz Hegi, SS 2013
Download Description (PDF, 56 KB), Download Report (PDF, 272 KB)

Verifying Separation Logic Contracts in Chalice

Daniel Jost, SS 2013
Download Description (PDF, 58 KB), Download Report (PDF, 378 KB)

Translating Chalice into SIL

Christian Klauser, AS 2012
Download Description (PDF, 58 KB), Download Report (PDF, 600 KB)

Developing a common web interface to various verification tools

Roland Meyer, SS 2012
Download Description (PDF, 57 KB), Download Report (PDF, 508 KB)

Interfacing TVLA and Sample

Raphael Fuchs, SS 2011
Download Description (PDF, 30 KB), Download Report (PDF, 311 KB)

Improving Permission-Based Verification of Concurrent Programs with Chalice

Stefan Heule, AS 2010
Download Description (PDF, 131 KB), Download Report (PDF, 891 KB)

Automating Magic Wands with Advanced Features
Yiqun Liu, SS 2024
Download Description (PDF, 212 KB)

Hyperwands
Yushuo Xiao, SS 2024
Download Description (PDF, 87 KB), Download Report (PDF, 619 KB)

Optimizing and Evaluating Universal Introduction in a Program Verifier
Johannes Gasser, SS 2024
Download Description (PDF, 151 KB), Download Report (PDF, 414 KB)

Alternative SMT Encodings for Congestion Control Algorithms
Raoul van Doren, SS 2024
Download Description (PDF, 168 KB)

A Standard Library for Gobra
Daniel Nezamabadi, SS 2024
Download Description (PDF, 153 KB), Download Report (PDF, 612 KB)

Verifying the IO Behaviour of the SCION Router
Markus Limbeck, SS 2024
Download Description (PDF, 451 KB), Download Report (PDF, 625 KB)

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

Adding Debugging Functionality to Viper
Andrea Keusch, SS 2023
Download Description (PDF, 141 KB), Download Report (PDF, 555 KB)

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

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

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

Improving User-Defined Permission Models in Viper
Anqi Li, AS 2022
Download Description (PDF, 119 KB), Download Report (PDF, 496 KB)

Verifying Go's Standard Library
Adrian Jenny, AS 2022
Download Description (PDF, 82 KB), Download Report (PDF, 1011 KB)

Adding Algebraic Data Types to a Verification Language
Allesandro Maissen, SS 2022
Download Description (PDF, 113 KB), Download Report (PDF, 867 KB)

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

Adding Native Support for Havoc in Viper
Daniel Zhang, AS 2022
Download Description (PDF, 101 KB), Download Report (PDF, 447 KB)