Alexander Nadel's
Page
General
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:
- Formal Verification of Hardware and Software
- Propositional Satisfiability (SAT)
- Model Checking
- Satisfiability Modulo Theories (SMT)
Contact Information
My email is alexander DOT nadel AT intel DOT com
Publications
2013
[1] Alexander Nadel, Vadim Ryvchin, and Ofer Strichman, 2013, “Efficient MUS Extraction with Resolution”. FMCAD’13.
[2] Alexander
Nadel, 2013, “Handling Bit-Propagating Operations
in Bit-Vector Reasoning” [presentation].
SMT’13.
[3] Yakir
Vizel, Vadim Ryvchin and Alexander Nadel, 2013, “Efficient Generation of Small
Interpolants in CNF” [CAV’13
presentation; Interpolation’13
presentation with additional details]. CAV’13.
2012
[4] Alexander Nadel, and Vadim Ryvchin, 2012, “Efficient SAT Solving under Assumptions” [presentation]. SAT’12.
o
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.
[5] Alexander Nadel, Vadim Ryvchin, and Ofer Strichman, 2012, “Preprocessing in Incremental SAT” [presentation]. SAT’12.
o A technical report containing a proof supplement is available.
2011
[6] Zurab Khasidashvili, and Alexander Nadel, 2011, “Implicative Simultaneous Satisfiability and Applications”
[presentation].
HVC’11.
[7] Alexander Nadel, June 2011, “Generating Diverse Solutions in SAT” [presentation]. SAT’11 The original publication is available at www.springerlink.com.
o An addendum to the paper is available.
2010
[8] Alexander Nadel, October 2010, “Boosting Minimal Unsatisfiable Core Extraction” [presentation]. FMCAD’10.
o An addendum to the paper containing complementary experimental results is available.
o
Benchmarks
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.
[9] Sabih Agbaria, Dan Carmi, Orly Cohen, Dmitry Korchemny, Michael
Lifshits and Alexander Nadel, October 2010, “SAT-Based
Semiformal Verification of Hardware”. FMCAD’10.
[10] 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.
[11] Alexander Nadel, Vadim Ryvchin, July 2010, “Assignment Stack Shrinking” [presentation]. SAT 2010: 375-381.
o Detailed experimental results are available.
o
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
before.
[12] Sabih Agbaria, Dan Carmi,
Orly Cohen, Dmitry Korchemny, Michael Lifshits, Alexander Nadel, February 2010,
“An
Experience of Complex Design Validation: How to Make Semiformal Verification
Work” [presentation]. Proceedings
of the Design and Verification Conference and Exhibition (DVCon '10).
[13] 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).
2009
[14] Alexander Nadel, August 2009, “Understanding and Improving a Modern SAT Solver”. PhD thesis, Tel Aviv University.
2007
[15] 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.
[16] 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.
2006
[17] Nachum Dershowitz, Ziyad Hanna, Alexander Nadel, August 2006, "A Scalable Algorithm for Minimal Unsatisfiable Core Extraction" [presentation]. SAT 2006: 36-41
2005
[18] Zurab Khasidashvili,
Alexander Nadel, Amit Palti, Ziyad Hanna, November 2005, "Simultaneous SAT-Based Model Checking of
Safety Properties" [presentation]. Haifa Verification Conference 2005:
56-75
[19] Nachum Dershowitz, Ziyad Hanna, Alexander Nadel, June 2005, "A Clause-Based Heuristic for SAT Solvers" [presentation]. SAT 2005: 46-60
2002
[20] Alexander Nadel, November 2002, "Backtrack Search Algorithms for Propositional Logic Satisfiability : Review and Innovations". Master Thesis, the Hebrew University.