Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Niklas Sörensson

Niklas Sörensson

I am a Ph.D. student at the Computing Science Department at Chalmers University of Technology and Göteborg University.
I am a member of the Formal Methods Research Group. My supervisor is Reiner Hähnle.

Research Interests

Applications and extensions of algorithms for SAT solving
First order theorem proving and finite model finding
SAT based model checking

Publications

Applications of SAT solving
Ph. Licenciate Thesis, 2003
An extensible SAT solver
Niklas Eén and Niklas Sörensson
Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing, 2003
Temporal Induction by incremental SAT solving
Niklas Eén and Niklas Sörensson
Proceedings of the First International Workshop on Bounded Model Checking, 2003
New techniques that improve MACE-style finite model finding
Koen Claessen and Niklas Sörensson
CADE-19, Workshop W4, Model Computation -- Principles, Algorithms, Applications, 2003
Fair constraint merging tableaux in lazy functional programming style
Reiner Hähnle and Niklas Sörensson
Published in a shorter form in Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, 2003
Symbolic Model Checking based on Induction
Master's Thesis, 2000

Software

Paradox This is a finite model finder for first order logic developed together with Koen Claessen. It won the Model class of the SAT division in CASC-19 competition for first order tools.

Tip (Temporal Induction Prover) I developed prototypes for this SAT based model checker in Haskell and C++. Niklas Eén later developed a full version in C++, keeping the core ideas from my prototypes.

Propositional SAT solvers I have implemented a Chaff-style SAT solver called Satnik which is used in Paradox and my prototypes for Tip. It performed fairly well in the SAT Competition 2003. Later I co-developed MiniSat together with Niklas Eén, which is a reimplementation of the core ideas from Satnik and his SAT solver Satzoo.

LTab A toy theorem prover for first order logic. It is an implementation of Constraint Merging Tableaux in the lazy functional programming language Haskell.

My CV

Contact information

Email: nik at cs.chalmers.se
Phone: +46 31 772 1023
Office: EDIT building, room 5461