My full publications page can be found here.
Here is my DBLP record and profile at Google scholar.
Books:
A republication of my PhD as a book:
Decision Procedures – An algorithmic point of view:
 |
 |
| First edition. This edition was #1 best seller of Springer/CS in the ‘theoretical computer science’ series in the last decade, and one of the best sellers in all of Springer/CS’s publications. | Second edition. Published in 2017. See the Publisher’s page. |
To cite this book, please use this bibTex entry.
Coming soon: a translation to Chinese.
Selected publications:
Optimal algorithm portfolios for computationally hard real-time problems. Annals of Mathematics and Artificial Intelligence (2020). Together with Yair Nof.
Vacuity in Synthesis, Formal Methods in Systems Design, 2021. Together with Roderick Bloem, Hana Chockler and Masoud Ebrahimi.
Ultimately Incremental SAT Proc. of the17th International conference on theory and applications of satisfiability testing(SAT’14). Together with Alexander Nadel and Vadim Ryvchin.
Efficient MUS extraction with Resolution Proc. of the 13thconference on Formal Methods in Computer Aided Design (FMCAD’13). Together with Vadim Ryvchin and Alexander Nadel.
Proving mutual termination of programs. Proc. of the eighth Haifa Verification Conference (HVC’12). Together with Dima Elenbogen and Shmuel Katz.
A proof producing CSP solver.Proc. of the 24thconference of the Association for the Advancement of Artificial Intelligence (AAAI’10). Together with Michael Veksler.
Regression verification: Proving the equivalence of similar programs. Software Testing, Verification and Reliability, 23(3) 241–258, 2013. Together with Benny Godlin.
Reducing the Size of Resolution Proofs in Linear Time. Journal on Software Tools and Technology Transfer (STTT),vol13, issue 3, page 263, 2011.Together with Omer Bar-Ilan, Oded Fuhrmann, Shlomo Hoory and Ohad Shacham.
Three optimizations for Assume-Guarantee reasoning with L*.Formal Methods in Systems Design, Vol. 32, number 3, pages 267–284, 2008. Together with Sagar Chaki.
SAT based abstraction-refinement using ILP and machine learning techniques. International Conference on Computer Aided Verification, 2002, pages 265-279. Together with Edmund Clarke, Anubhav Gupta and James Kukula.
Pruning techniques for the SAT-based bounded model checking problem. In Proc. of Correct Hardware Design and Verification Methods (CHARME), 2001, pages 58-70.