Niklas Een

email:

niklas

een.se

Publications:

DeepMath - Deep Sequence Models for Premise Selection, Alex A. Alemi, Francois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, Josef Urban, 2017
A Circuit Approach to LTL Model Checking, Koen Claessen, Niklas Een, Baruch Sterin, FMCAD 2013.
A Fast Reparameterization Procedure, Niklas Een, Alan Mishchenko, DIFTS 2013.
A Toolbox for Counterexample Analysis and Optimization, Alan Mishchenko, Niklas Een, Robert Brayton, IWLS 2013.
GLA: Gate-level Abstraction Revisited, A. Mishchenko, N. Een, R. Brayton, J. Baumgartner, H. Mony, and P. Nalla, DATE 2013.
A Semi-canonical Form for Sequential AIGs, A. Mishchenko, N. Een, R. Brayton, M. Case, P. Chauhan, and N. Sharma, DATE 2013.
Variable Time-frame Abstraction A. Mishchenko, N. Een, R. Brayton, J. Baumgartner, H. Mony, and P. Nalla, IWLS 2012.
Logic Synthesis for Disjunctions of Boolean Functions B. Sterin, A. Mishchenko, N. Een and R. K. Brayton, IWLS 2012.
Using Speculation for Sequential Equivalence Checking, R. Brayton, N. Een, and A. Mishchenko, "Using speculation for sequential equivalence checking", IWLS 2012.
Mapping into LUT structures S. Ray, A. Mishchenko, N. Een, R. Brayton, S. Jang, and C. Chen, DATE 2012.
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:

My current verification and synthesis framework, ZZ, is available at Bitbucket. MiniSat and SatELite now have their own page at minisat.se. All other software developed during my Ph.D. can be found in the EenSoft.zip package. More information and references can be found on the (now very 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.