Publications by Georg Stefan Schmid

Generalized Arrays for Stainless Frames

We present an approach for verification of programs with shared mutable references against specifications such as assertions, preconditions, postconditions, and read/write effects. We implement our tool in the Stainless verification system for Scala. A nov ...

Springer, Cham2022

Scaling Language Features for Program Verification

Georg Stefan Schmid

Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...

EPFL2022

Dynamic Balanced Graph Partitioning

Georg Stefan Schmid, Andreas Loukas

This paper initiates the study of the classic balanced graph partitioning problem from an online perspective: Given an arbitrary sequence of pairwise communication requests between n nodes, with patterns that may change over time, the objective is to servi ...

SIAM Publications2020

SMT-Based Checking of Predicate-Qualified Types for Scala

Viktor Kuncak, Georg Stefan Schmid

We present qualified types for Scala, a form of refinement types adapted to the Scala language. Qualified types allow users to refine base types and classes using predicate expressions. We implemented a type checker for qualified types that is embedded in ...

Assoc Computing Machinery2016