Magnus Björk

I'm a researcher within formal verification. Currently, I'm employed by Jasper Design Automation for a joint research project with Chalmers University of Technology. We're investigating formal verification of high level design models. The research is funded by the Swedish Research Council.

During 2008, I did a post doc together with RUAG Aerospace (formerly known as Saab Space), investigating how to introduce formal verification into their ASIC design flow. Simultaneously, I taught at the IT University of Gothenburg. In 2007, I did a post doc at Oxford University, doing research about symbolic trajectory evaluation, STE. The year before, I worked with scheduling and compilation in the FlexSoC project.

Some of my publications can be found at DBLP, and some more at this Chalmers page.

        Me

PhD thesis: A First Order Extension of Stålmarck's Method

For my PhD, I developed a first order extension of Stålmarck's method. The major features of this work is outlined in a poster presented at IJCAR 2004 (download as pdf, ps.gz, ps). My PhD thesis offers the most thorough description of the method, including proofs of soundness and completeness, and some benchmarks.

I also implemented the automated theorem prover Dilemma based on my proof method. A gzipped linux binary for Dilemma can be downloaded here.

Personal

Disclaimer