Lars Hupel

Picture of Lars Hupel PhD student
Chair for Logic and Verification, Fakultät für Informatik
Office: MI 00.09.063
Office hours: upon request
Office phone: +49 89 289-17328
Email: lars.hupel the at sign tum.de
CV: [PDF]

Teaching

  • Einführung in die theoretische Informatik: SS11 (Tutor)
  • Einführung in die theoretische Informatik: SS12 (Tutor)
  • Einführung in die Informatik 2: WS12/13 (Tutor)
  • Einführung in die Informatik 2: WS13/14 (Übungsleitung)
  • Einführung in die theoretische Informatik: SS14 (Tutor)
  • Einführung in die Informatik 2: WS14/15 (Übungsleitung)
  • Perlen der Informatik 3: WS14/15 (Proseminar)
  • Equational Logic: SS15 (Übungsleitung)
  • Fortgeschrittene Konzepte der funktionalen Programmierung: SS15 (Seminar)
  • Spezifikation und Verifikation: WS15/16 (Praktikum)
  • Perlen der Informatik 1: WS15/16 (Übungsleitung)
  • Spezifikation und Verifikation: SS16 (Praktikum)
  • Perlen der Informatik: SS16 (Proseminar)
  • SAT-Solving: SS16 (Proseminar)
  • Perlen der Informatik 3: WS16/17 (Übungsleitung)
  • Logik: SS17 (Übungsleitung)

Service

Software

  • Isabelle: a generic proof assistant
    [code]
  • libisabelle: a Scala library which talks to Isabelle
    [code] [doi]
  • The Leon system for verification, synthesis, and more
    [code]
  • Fancy Formal Firewall Universal Understander
    [code]
  • Lem: a tool for lightweight executable mathematics
    [code]

Research & Publications

Isabelle

AFP Entries

Isabelle CakeML

CakeML

Haskell

Teaching Haskell

Isabelle

Network Security

(joint work with Cornelius Diekmann)
Isabelle Scala

Isabelle Tooling

  • A Visualization Toolkit for Simplifier Traces in Isabelle/jEdit
    Master's Thesis in Informatics, Technische Universität München, 2013
    [pdf]
  • Interactive Simplifier Tracing and Debugging in Isabelle
    Intelligent Computer Mathematics (CICM 2014)
    The final publication is available at Springer Link.
    [pdf] [bibtex] [doi] [arXiv] [slides]
  • Translating Scala Programs to Isabelle/HOL
    with Viktor Kuncak
    International Joint Conference on Automated Reasoning (IJCAR 2016)
    The final publication is available at Springer Link.
    [pdf] [bibtex] [doi] [arXiv] [slides]
  • Clone Detection in Isabelle Theories
    with Dominik Vinan
    accepted for presentation at the Isabelle Workshop 2016
    Download (preview): ConQAT+Isabelle bundle
    [pdf]
Scala

Generic Programming

  • Generating Type Class Instances Automatically
    Presentation at Scala2013, Montpellier
    [slides]