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 somewhat outdated verification and synthesis framework, zz-abc, is available at github.
MiniSat and SatELite now have their own page at minisat.se.
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.
Games:
Try my new vibe-coded 80s style game Rally Vroom.
een.se