Software Engineering | Formal Methods | Acrobatics

I’m Mauro, software engineer with an interest in formal methods. The other half of my life is taken up by handbalancing, bouldering and calisthenics.

A one arm handstand

current work

Incompleteness testing of SMT solvers [research 2021-now]

Based on my master thesis project at ETH Zürich, Dominik Winterer and me are testing widely used solvers Z3 and CVC5 for incompletenesses by mutating SMT-LIB formulas in a satisfiability-preserving way.

Haskell bindings for Z3 [opensource 2021-now]

I help with general maintenance of haskell-z3 and am extending the bindings to cover more of the Z3 API.

Full-stack development [professional 2021-now]

I am designing and building an OCaml web application in the area of knowledge representation and semantic web.

past work

Viper Program Verification [education/research 2019-2020]

18 months of implementation work on a program verifier for heap-manipulating programs. I designed and implemented an alternative SMT encoding of program heaps.

Babel JavaScript transpiler [opensource 2017]

A few small contributions to the Babel JavaScript transpiler, my first endeavour in open source.

Web development [professional 2015-2018]

Three years of back- and frontend development building WordPress websites.