Erfahrung
3D Vision Engineer
Brütsch Technology
Beringen, Schweiz
Okt 2025 – heute
Deep Learning, Python, Computer Vision
Ich arbeite an einem Intraoral-Scanner (IOS), um Zähne zu scannen und daraus ein 3D-Modell zu erzeugen. Ich entwickle und verbessere Deep-Learning-Modelle, bewerte, welche Probleme sich sinnvoll mit Deep Learning lösen lassen, und erarbeite Strategien zur Umsetzung. Zusätzlich helfe ich dabei, Coding-Guidelines zu verbessern.
Doktorand (PhD)
Constructor Institute of Technology (Academia)
Schaffhausen, Schweiz
Dez 2023 – Sep 2025
Formal Verification, Eiffel, Automated Proofs (Isabelle HOL), LLMs, AI
- Mathematical Proof Engine: Entwicklung eines Engines zur Validierung mathematischer Beweise in einer objektorientierten Programmiersprache. Erste Machbarkeitsstudie (Proof of Concept) für einen einfachen Beweis.
- Formalisierung der Programmierung: Aufbau einer Formalisierung von Programmierung (Definitionen und Theoreme), einzeln verifiziert in Isabelle/HOL. (Link)
- AI für formale Verifikation: Planung, Durchführung und Analyse einer Studie zur Wirksamkeit von LLMs beim Bugfixing. (Link)
- Proof of Concepts: Entwicklung von CodeForge, einem Tool zum Kompilieren, Ausführen und Verifizieren von Programmen online (ohne lokale Installation). Zusätzlich Entwicklung von AI-Proof, das LLMs, Sledgehammer und Isabelle/HOL nutzt, um automatisch Beweise zu erzeugen. (Link)
- Teaching Assistant: Unterstützung in den Kursen Advances in Software Engineering und Software Construction, Architecture and Engineering (Übungslektionen, Prüfungen verfassen und korrigieren, Mentoring).
Data Scientist
ti&m (Banking, Government, FinTech)
Zürich, Schweiz
Aug 2020 – Nov 2023
Machine Learning, Python, JavaScript, Docker, Data Science, AI, Computer Vision, Blockchain, Recommender Systems
- eID: Evaluation mehrerer SSI-Technologien für die Schweizer E-ID. Deployment in einer Public Cloud mit Blockchain-Technologie. Umsetzung von Frontend, Backend und Mobile App. (Link)
- Fit&Proper: Erweiterung einer bestehenden Lösung zur automatischen Background-Check-Unterstützung für eine Finanzmarktaufsicht mittels NLP und Machine Learning. (Link)
- Sustainability Assessment: Entwicklung eines MVP, um einem Team von Nachhaltigkeitsexpert:innen zu helfen, Antworten in ihren Daten (insbesondere PDFs) zu finden. Das Tool vereinfacht das Extrahieren und Analysieren von Informationen aus grossen Dokumentensammlungen. (Link)
- Construction Standard Management: Planung, Entwicklung und Deployment einer Lösung zur Verwaltung der wichtigsten Baustandards in der Schweiz (eBKP/NPK). Das System verbesserte Effizienz und Zugänglichkeit für Fachpersonen. (Link)
- Proof of Concepts: Prototypen für ein Reise-Empfehlungssystem sowie Tools zur Erkennung und zum Parsing von IDs und Pässen.
Software Engineer (Machine Learning, Computer Vision)
Kitris GmbH (Sports)
Zürich, Schweiz
Jan 2020 – Jul 2020
Python, Docker, R&D, Computer Vision, Visual Computing
- Video Tracking: Proof of Concept für ein Video-Tracking-System zur Analyse von Bewegungen und Aktionen in Sportvideos. Einsatz von Computer-Vision-Methoden, um relevante Features zu extrahieren und verwertbare Insights für Coaches und Analyst:innen zu liefern.
Junior Security Researcher & Software Engineer
Exeon Analytics (Cybersecurity)
Zürich, Schweiz
Apr 2018 – Jun 2019
Python, Docker, Scala, React
- Exeon Trace: Verbesserung des Hauptprodukts durch eine neue Funktion zur Nachverfolgung und Visualisierung von Netzwerkverkehr, was die Sicherheitsüberwachung der Plattform stärkte.
- Tridyo: Entwicklung eines MVPs für ein neues Produkt zur Analyse der zukünftigen Rentabilität von Unternehmen mittels Sentimentanalyse und Fit-&-Proper-Ansatz.
Projekte
Parallelismus
GitHub, Web Demo
Parallelismus ist eine Webanwendung zum Studium biblischer Parallelismen in hebräischen und griechischen Texten. Sie ermöglicht es, durch biblische Bücher, Kapitel und Verse zu navigieren und dabei Wörter mit ihren Strong-Konkordanznummern, Originaltexten und Übersetzungen zu sehen. Benutzer können semantische Beziehungen zwischen Wörtern erstellen und verwalten (wie ähnliche Bedeutung, gegensätzliche Bedeutung, Unterkategorien und Zusammensetzung). Das Tool verwendet IndexedDB für lokale Speicherung und bietet Visualisierungsfunktionen zur Erkundung von Wortbeziehungen durch interaktive Graphen. Die gesamte Datenverarbeitung erfolgt clientseitig, wodurch es eine vollständig funktionale statische Webanwendung ist.
Background Generator
GitHub, Web Demo
Background Generator ist eine prozedurale Kunst-Suite, die SVG-Hintergründe mit TypeScript erstellt. Sie umfasst fünf verschiedene Generatoren: Farbverläufe mit Blobs und Bändern, Polygalaxy-Szenen mit geometrischen Fragmenten und Orbitalsystemen, Terrain-Landschaften mit Bergen und Nebel, urbane Skylines mit Parallax-Ebenen und botanische Gärten mit Blättern und Ranken. Das Tool bietet sowohl einen Web-Playground für Echtzeit-Experimente als auch CLI-Tools für Batch-Rendering. Alle Generatoren unterstützen anpassbare Themes, Seed-basierte Zufallsgenerierung für Reproduzierbarkeit und optionalen PNG-Export.
Python Blocks
GitHub, Web Demo
Python Blocks ist ein blockbasierter Python-Editor auf Basis von Vue 3 und Pinia. Man kann Python-Programme aus visuellen Blöcken zusammensetzen, den erzeugten Python-Code live inspizieren, bestehenden Python-Code zurück in die Blockansicht importieren und das Ergebnis direkt im Browser mit PyScript ausführen.
Buchfaltstudio
GitHub, Web Demo
Buchfaltstudio ist ein Generator für Buchfaltmuster, der präzise Faltanweisungen für Buchkunst (Orimoto) erstellt. Benutzer können entweder Text eingeben (der automatisch mit Google Fonts gerendert wird) oder Bilder hochladen (SVG, PNG, JPEG, GIF, WebP). Das Tool analysiert das Artwork, skaliert es auf physische Buchdimensionen, erkennt dunkle Bereiche und generiert detaillierte PDF-Anleitungen mit millimetergenauen Faltpositionen. Features umfassen automatisches Buchvorschau-Rendering, anpassbare Seitenzahl und Buchhöhe sowie vollständig clientseitige Verarbeitung für sofortige Ergebnisse.
Hoare Logic Proof Verifier
GitHub, Web Demo
Dies ist ein Hoare-Logik-Verifier, der vollständig im Browser läuft. Man kann Programme und Beweise per Drag & Drop erstellen. Die Beweise müssen bis zum Ende explizit geführt werden. Logische und arithmetische Beweispflichten werden an den SMT-Solver Z3 übergeben. Das Tool ist komplett frontend-basiert; es braucht keinen Server und funktioniert daher auch auf dieser statischen Website.
CodeForge
CodeForge on GitHub
CodeForge ist eine Plattform, um Code in mehreren Programmiersprachen zu kompilieren, auszuführen und zu verifizieren. Dafür werden Docker-Container genutzt, damit die Codeausführung sicher bleibt. Die Plattform eignet sich für Bildungsumgebungen und Coding-Demos. Die containerisierte Architektur erleichtert die Integration neuer Sprachen und Verifikationstools. Es wurde komplett „vibe coded“. Es ist teilweise unter eiffel.org online.
PDF Scannen
PDF Scan Automation auf GitHub
PDF Scan ist ein Projekt, das die Organisation von physischer Post und Dokumenten vereinfacht. Es verarbeitet Stapel gescannter Dokumente, erkennt automatisch, wo sie in einzelne Dateien getrennt werden müssen, richtet Seiten aus und führt OCR durch, um Text zu extrahieren. Das reduziert den manuellen Aufwand bei Digitalisierung und Archivierung. Es ist besonders hilfreich für den privaten und kleinen Bürogebrauch. Es wurde teilweise „vibe coded“.
AutoProof Docker
Autoproof Docker auf GitHub
Dieses Projekt bietet eine Docker Bild für den Betrieb AutoProof, einen statischen Prüfer für Eiffelprogramme. Durch die Containerisierung von AutoProof wird der Setup-Prozess unkompliziert und plattformunabhängig. Benutzer können Eiffel-Programme schnell überprüfen, ohne sich um komplexe Abhängigkeiten kümmern. Das Docker-Bild ist ideal für Forscher und Pädagogen, die mit formaler Verifikation arbeiten.
Evolution Showcase
Evolution Showcase on GitHub
Evolution Showcase ist ein kleines Python-Spiel, das visuell die Prinzipien der Evolution und der natürlichen Selektion zeigt. Im Spiel zeigen Agenten zufällige Verhaltensweisen, aber im Laufe der Zeit werden diejenigen ausgewählt, die für die Umgebung am besten geeignet sind, was zu nicht-random Strategien führt. Das Projekt dient als pädagogisches Instrument zur Veranschaulichung evolutionärer Algorithmen und auftauchendem Verhalten.
OpenSCAD Telefon Stand
OpensCAD Telefon Stand auf GitHub
Dieses Projekt verfügt über ein anpassbares 3D-Modell eines Telefonstands, das unter OpenSCAD erstellt wird. Das Design ist voll parametriert, so dass Benutzer die Abmessungen an jedes Handymodell anpassen können. Es ist ideal für 3D-Druckenthusiasten.
Diese Website
Diese Website auf GitHub Diese Website wurde mit MkDocs mit einer benutzerdefinierten Vorlage und eigenem Styling gebaut. Sie wird automatisch unter retoweber.info veröffentlicht.
Veröffentlichungen
Helfen KI-Modelle dabei, verifizierte Bugfixes zu erzeugen?
ICSE 2026. (eingereicht – in review)
Autoren: Reto Weber, Li Huang, Bertrand Meyer, Ilgiz Mustafin, Marco Piccioni, Alessandro Schena
PRISM: Programmierung ist wirklich einfache Mathematik
YuriFest 2025. (angenommen – erscheint)
Autoren: Reto Weber, Bertrand Meyer
Loop unrolling: formale Definition und Anwendung fürs Testen
ICTSS 2025. (angenommen – erscheint)
Autoren: Reto Weber, Li Huang, Bertrand Meyer
Konferenzen
Programmierung ist wirklich einfache Mathematik
YuriFest 2025, Ludwig-Maximilians-Universität München, München, Deutschland
Programmverifikation mit AutoProof
AVM 2024, Universität Freiburg, Freiburg, Deutschland
Ausbildung
Konstrukteur Institut für Technologie
Doktor der Philosophie (PhD), Informatik (2023 – heute)
Thema: Programmieren ist wirklich einfache Mathematik – und umgekehrt
Fokus: Statische Verifikation objektorientierter Programmiersprachen, z. B. Eiffel. Ich formalisiere Programmierung mathematisch und bette Mathematik in Eiffel ein, um die Lücke zwischen Programmierung und Mathematik zu verkleinern.
ETH Zürich
Master of Science (MSc), Informatik (2017 – 2020)
Master Thesis: Unaudible Audio-Adversarial-Perturbationen über Psychoakustische Clipping
Vorlesungen (Auswahl): Machine Learning, Web Engineering, Deep Learning, Probabilistic Artificial Intelligence, Advanced Topics in Machine Learning, Einführung in die Quanteninformatik, Models of Computation, Principles of Distributed Computing, Algorithms Lab, Computational Intelligence Lab, Introduction to Social Networks: Theory, Methods and Applications
Bachelor of Science (BSc), Informatik (2013 –2017)
Bachelor-Thesis: Solving Constraint-Satisfaction Problems with Spike-Based Neural Attractor Winner-Take-All under Oscillatory Inhibition
Vorlesungen (Auswahl): Analysis I, Analysis II, Einführung in die Programmierung, Datenstrukturen & Algorithmen, Parallele Programmierung, Lineare Algebra, Diskrete Mathematik, Physik, Digitaltechnik, Data Modelling and Databases, Formal Methods and Functional Programming, Operating Systems and Networks, Systems Programming and Computer Architecture, Theoretische Informatik, Wahrscheinlichkeit und Statistik, Learning and Intelligent Systems, Information Security, Visual Computing, Software Architecture and Engineering, Embedded Systems, Introduction to Neuroinformatics, Algorithmen und Kombinatorik, Einführung in die Spieltheorie, Introduction to Cognitive Neuroscience
