Joined the Erlang Computer Science lab in 1997 to work with the development of Erlang. In particular the verification of Erlang programs in a broad sense. Failed to build a useful type system for Erlang, but together with SICS we got a theorem prover for Erlang to work. Proved part of Mnesia to be correct. Also worked with model checking of Erlang programs and tested an optimization of the TCAP protocol. Turned out that formal methods for Erlang is great stuff, but with steep learning curve.

After moving to a position at Chalmers, worked with John Hughes to get QuickCheck into Erlang. QuickCheck generates test cases automatically. It is a useful way to get specifications drive verififcation through testing. So successful that we could start a company baded upon this idea. Quviq is now world leading in automatic test case generation tools.