I am a computer scientist and engineer. I completed my PhD at the Tel Aviv university under the supervision of Prof. Nachum Dershowitz at 2009.
I am currently at Intel, Haifa. My professional interests include:
My email is alexander DOT nadel AT intel DOT com
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.
 Anders Franzén, Alessandro
Cimatti, Alexander Nadel, Roberto Sebastiani and Jonathan Shalev, October 2010,
SMT in Symbolic Execution of Microcode”. FMCAD’10.
Received the FMCAD’10 best paper
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
 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.