software engineer && acrobat
- generally interested in software correctness, e.g. testing, type systems, static anaysis and verification
- specifially interested in formal logic and SMT solving
- programming languages and compiler nerd
- open source contributor
- Haskell ex-beginner
- part-time acrobat, e.g. handstands, backflips et cetera
Fuzz-testing SMT solvers [education] | Python, Z3, CVC4, SMT-LIB, formal logic, testing
My master thesis project at ETH Zürich. I am implementing a semantic method to mutate SMT-LIB formulas in a satisfiability-preserving way to help uncover bugs in widely used solvers like Z3 and CVC4.
Lambda Calculus [personal project] | Haskell, Lambda Calculus, compiler, interpreter
I am writing a compiler for a small subset of Haskell to pure lambda calculus. Useless but glorious.
Haskell bindings for Z3 [opensource] | Haskell, Z3
I help with general maintenance and am extending the bindings to cover more of the Z3 API.
- Viper Program Verification [education/professional] | Scala, SMT encoding of program heaps, symbolic execution