Niklas Een

where:	Currently at UC Berkeley, EECS.
e-mail:	niklaseen.se
phone:	+1-510-387-9419 (cell)
address:	1354 Grizzly Peak Blvd Berkeley, CA 94708, USA

Publications:

Efficient Implementation of Property Directed Reachability, Niklas Een, Alan Mishchenko, Robert Brayton, IWLS 2011.
The Benefit of Concurrency in Model Checking, Baruch Sterin, Niklas Een, Robert Brayton, IWLS 2011.
A Single-Instance Incremental SAT Formulation of Proof- and Counterexample-Based Abstraction, Niklas Een, Alan Mishchenko, Nina Amla, FMCAD 2010.
Magic: An Industrial-Strength Logic Optimization, Technology Mapping, And Formal Verification Tool , A. Mishchenko, N. Een, R. K. Brayton, S. Jang, M. Ciesielski, T. Daniel, IWLS 2010.
SAT-Solving in Practice, K. Claessen, N. Een, M. Sheeran, N. Sorensson, WODES 2008.
Cut Sweeping, Niklas Een, Cadence Technical Report, 2007.
Applying Logic Synthesis for Speeding Up SAT, Niklas Een, Alan Mishchenko, Niklas Sorensson, SAT 2007.
Improvements to Combinational Equivalence Checking, Alan Mishchenko, Satrajit Chatterjee, Robert Brayton, Niklas Een, IWLS 2006.
Translating Pseudo-Boolean Constraints into SAT, Niklas Een, Niklas Sorensson, JSAT 2006.
Effective Preprocessing in SAT through Variable and Clause Elimination, Niklas Een, Armin Biere, SAT 2005.
SAT Based Model Checking, Ph.D. Thesis, 2005.
An Extensible SAT-solver, Niklas Een, Niklas Sorensson, SAT 2003.
Temporal Induction by Incremental SAT Solving, Niklas Een, Niklas Sorensson, BMC 2003.
Symbolic Reachability Analysis based on SAT-Solvers, Parosh A. Abdulla, Per Bjesse, Niklas Een, TACAS 2000.

Software:

MiniSat and SatELite now have their own page at minisat.se. All other software I developed during my Ph.D. can be found in the EenSoft.zip package. More information and references can be found on the (somewhat out-dated) Satzoo page, and on the Tip (temporal induction prover) page.

Personal:

During 1991-94, I created some Single Image Stereograms that are still somewhat popular, although quite low-res by today's standards. They used to take about 20 hours to generate by my 25 MHz 486sx.