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.
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.
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.
Web development [professional 2015-2018]
Three years of back- and frontend development building WordPress websites.