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.
Contact information
- Email:
nik at cs.chalmers.se - Phone: +46 31 772 1023
- Office: EDIT building, room 5461