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
 Yakir Vizel,
Alexander Nadel and Sharad Malik, 2017, “Solving Linear
Arithmetic with SAT-based Model Checking” [presentation].
 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”
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.
Alessandro Cimatti, Alexander Nadel, Roberto Sebastiani and Jonathan Shalev,
October 2010, “Applying SMT in Symbolic Execution of Microcode”.
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
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,
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.
Nachum Dershowitz, Ziyad Hanna, Alexander Nadel, June 2007, "Towards a Better Understanding of the Functionality of a Conflict-Driven SAT Solver" [presentation]. SAT 2007: 287-293.
Nachum Dershowitz, Ziyad Hanna, Alexander Nadel, August 2006, "A Scalable Algorithm for Minimal Unsatisfiable Core Extraction" [presentation]. SAT 2006: 36-41
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.