I am a researcher and engineer developing high-performance constraint solving tools.
I have been at Intel, Haifa for 14 years. My professional interests include:
My email is alexander DOT nadel AT intel DOT com
 Alexander Nadel, 2017, “A
Correct-by-Decision Solution for Simultaneous Place and Route” [presentation]. CAV’17.
 Yakir Vizel, Alexander Nadel and Sharad Malik, 2017, “Solving Constraints over Bit-Vectors with SAT-based Model
Checking” [presentation]. SMT’17.
 Amit Erez and Alexander Nadel, 2015, “Finding
Bounded Path in Graph using SMT for Automatic Clock Routing” [presentation]. CAV’15.
 Nachum Dershowitz and Alexander Nadel, 2015, “Is
Bit-Vector Reasoning as Hard as NExpTime in Practice?”
 Yakir Vizel, Vadim Ryvchin and Alexander Nadel, 2015, “Efficient Generation of Small Interpolants in CNF”. Formal Methods in System Design (2015), pages 1-24.
 Alexander Nadel, Vadim Ryvchin, and Ofer Strichman, 2014, “Accelerated Deletion-based Extraction of Minimal
Unsatisfiable Cores”. Journal on Satisfiability, Boolean Modeling and
Computation (JSAT) 9 (2014), pages 27-51.
 Alexander Nadel, 2014, “Bit-Vector Rewriting
with Automatic Rule Generation” [presentation].
Nadel, 2013, “Handling Bit-Propagating Operations
in Bit-Vector Reasoning” [presentation].
 Yakir Vizel, Vadim Ryvchin and Alexander Nadel, 2015, “Efficient Generation of Small Interpolants in CNF” [CAV’13 presentation; Interpolation’13 presentation with additional details]. CAV’13.
We found two typos in the
paper: the subscript for the conjunction should be “j=1” instead of “j=i” at p.9, last paragraph and p. 10, Alg.2, line 3.
o A technical report containing a proof supplement is available.
 Zurab Khasidashvili, and
Alexander Nadel, 2011, “Implicative Simultaneous
Satisfiability and Applications” [presentation].
o An addendum to the paper is available.
o An addendum to the paper containing complementary experimental results is available.
for high-level minimal unsatisfiable core extraction, which were generated
by Intel’s abstraction refinement flow and used in my paper, are available at
the above link. Thanks to satcompetition.org
site organizers for hosting them.
 Anders Franzén, Alessandro Cimatti, Alexander Nadel,
Roberto Sebastiani and Jonathan Shalev, October 2010, “Applying
SMT in Symbolic Execution of Microcode”. FMCAD’10.
Received the FMCAD’10 best paper award.
o Detailed experimental results are available.
Minisat 2 with shrinking and advanced restart
strategies is available. Vadim Ryvchin implemented shrinking and the
restart strategies on top of Minisat 2.
UPDATE (December, 2010): Now the code matches exactly the Minisat
version we had used for the paper. Unfortunately, an incorrect version appeared
 Sabih Agbaria, Dan Carmi,
Orly Cohen, Dmitry Korchemny, Michael Lifshits, Alexander Nadel, February 2010,
Experience of Complex Design Validation: How to Make Semiformal Verification
Proceedings of the Design and Verification Conference and Exhibition (DVCon '10).
 Orly Cohen, Moran Gordon, Michael Lifshits, Alexander Nadel, Vadim Ryvchin, February 2010, “Designers Work Less with Quality Formal Equivalence Checking” [presentation]. Proceedings of the Design and Verification Conference and Exhibition (DVCon '10).
 Roberto Bruttomesso,
Alessandro Cimatti, Anders Franzén, Alberto
Griggio, Ziyad Hanna, Alexander Nadel, Amit Palti, Roberto Sebastiani, August
2007, "A Lazy and Layered SMT(BV) Solver for Hard
Industrial Verification Problems". CAV 2007: 547-560.
 Zurab Khasidashvili,
Alexander Nadel, Amit Palti, Ziyad Hanna, November 2005, "Simultaneous SAT-Based
Model Checking of Safety Properties" [presentation]. Haifa Verification Conference 2005:
 Alexander Nadel, November 2002, "Backtrack Search Algorithms for Propositional Logic Satisfiability : Review and Innovations". Master Thesis, the Hebrew University.