Conference version

Journal version

Presentation

Accelerating CAR-based Model-Checking with

Multiple Unsatisfiable Cores. Proc of the Symposium on Model Checking of Software (SPIN’25). Together with Yibo Dong, Xiwei Wu, Jianwen Li and Geguang Pu.

Presentation

Revisiting Assumptions Ordering in CAR-Based

Model Checking. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (2025), Vol 44, Issue 10, pages 4032-4037. Together with Yibo Dong, Yu Chen, Jianwen Li and Geguang Pu.

Model-Guided Synthesis for LTL over Finite

Traces. Proc. Of the 25th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’24). Together with Shengping Xiao, Yongkang Li, Xinyue Huang, Yicong Xu, Jianwen Li, Geguang Pu and Moshe Y. Vardi.

Presentation

Combining BMC and Complementary Approximate Reachability to Accelerate Bug-Finding. Proc. of the 41 international conference on computer-aided design (ICCAD’22). Together with Xiaoyu Zhang, Shengping Xiao, Jianwen Li and Geguang Pu.

Presentation

Exploiting Isomorphic Subgraphs in SAT. Proc. of the 21^th conference on Formal Methods in Computer-Aided Design (FMCAD'21). Together with Alexander Ivrii.

Presentation

Synthesizing Reactive Systems Using Robustness and Recovery Specifications. Proc. of the 19^th conference on Formal Methods in Computer-Aided Design (FMCAD'19). Together with Roderick Bloem, Hana Chockler and Masoud Ebrahimi.

Specifiable robustness in reactive synthesis. Formal Methods in systems Design (2023, online version). Together with Roderick Bloem, Hana Chockler and Masoud Ebrahimi.

Presentation

Optimal algorithm portfolios for computationally hard real-time problems. Proc. of Data-Science meets Optimization (DSO'19), an IJCAI'19 workshop. Together with Yair Nof.

Optimal algorithm portfolios for computationally

hard real-time problems.  Annals of Mathematics and Artificial Intelligence (2020). Together with Yair Nof.

Presentation

Forward to the special issue on program equivalence, Formal Methods in Systems Design.

Near-Optimal Course Scheduling at the Technion. Interfaces, Volume 47 Issue 6, November-December 2017, pp. 537-554. Available online also from https://pubsonline.informs.org/doi/full/10.1287/inte.2017.0920

The impact of Entropy and Solution Density on selected SAT heuristics. In CoRR arXiv:1706.05637. Together with Dor Cohen.

The Impact of Entropy and Solution Density on

Selected SAT Heuristics, Entropy 2018, 20, 713; Together with Dor Cohen.

presentation

Decision-Making with Cross-Entropy for Self-Adaptation. Proc. of 12^th international symposium on software engineering for adaptive and self-managing systems (SEAMS'17). Together with Gabriel A. Moreno, Sagar Chaki and Radislav Vaisman.

Presentation

Synthesizing Non-Vacuous Systems Proc. of 18th Conference on Verification, Model Checking, and Abstract Interpretation - VMCAI 2017. Together with Roderick Bloem, Hana Chockler and Masoud Ebrahimi.

Vacuity in Synthesis, Formal Methods in Systems Design, 2021. Together with Roderick Bloem, Hana Chockler and Masoud Ebrahimi.

Presentation

Regression Verification for unbalanced recursive functions  Proc. of 21st International Symposium on Formal Methods (FM’16). Together with Maor Veitsman.

Presentation

Minimal unsatisfiable core extraction for SMT. Proc. of the 16th conference on Formal Methods in Computer Aided Design (FMCAD'16). Together with Ofer Guthman and Anna Trostanetski.

Presentation

Mining Backbone Literals in Incremental SAT -a new kind of incremental data. Proc. of the 18th International conference on theory and applications of satisfiability testing (SAT'15), pages 88-103. Together with Alexander Ivrii and Vadim Ryvchin.

Presentation

(presentation in pdf)

Learning the Language of Error Proc. of the 13th International Symposium on Automated Technology for Verification and Analysis (ATVA'15). Together with Martin Chapman, Hana Chockler, Pascal Kesseli, Daniel Kroening and Michael Tautschnig. Please read this note.

Learning the language of software errors Journal of Artificial Intelligence Research (JAIR) 67 (pp 881 – 903), 2020. Together with Hana Chockler, Pascal Kesseli, and Daniel Kroening.

(This article contains the novel technique of ‘Lazy learning’).

Presentation

Learning general constraints in CSP Proc. of The 12th International Conference on Integration of Artificial Intelligence (AI) and Operations Research (OR) techniques in Constraint Programming (CPAIOR 2015). Together with Michael Veksler.

Learning general constraints in CSP Journal of Artificial Intelligence 238 (2016) 135-153. Together with Michael Veksler.

Model Counting of Monotone CNF Formulas with

Spectra   INFORMS Journal on Computing 27(2). Together with Radislav Vaisman and Ilya Gertsbakh, 2015.

Ultimately Incremental SAT Proc. of the 17th International conference on theory and applications of satisfiability testing (SAT'14). Together with Alexander Nadel and Vadim Ryvchin.

Presentation

Verifying Periodic Programs with Priority Inheritance Locks  Proc. of the 13^th conference on Formal Methods in Computer Aided Design (FMCAD'13). Together with Sagar Chaki and Arie Gurfinkel.

Presentation

Efficient MUS extraction with Resolution  Proc. of the 13^th conference on Formal Methods in Computer Aided Design (FMCAD'13). Together with Vadim Ryvchin and Alexander Nadel. Please read the note.

Accelerated Deletion-based Extraction of Minimal

Unsatisfiable Cores Journal on Satisfiability, Boolean Modeling and Computation (JSAT) 9 (2014), pages 27-51.  Together with Alex Nadel and Vadim Ryvchin.

Presentation

A New Class of Lineage Expressions over Probabilistic Databases computable in P-time.  Proc. Of the7th International conference on Scalable Uncertainty Management (SUM 2013). Together with Batya Kenig and Avigdor Gal.

Presentation

Compositional Sequentialization of Periodic Programs. Proc. of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'13). Together with Sagar Chaki, Arie Gurfinkel and Soonho Kong.

Presentation

Proving mutual termination of programs.  Proc. of the eighth Haifa Verification Conference (HVC'12). Together with Dima Elenbogen and Shmuel Katz.

Proving Mutual Termination.  Formal Methods in Systems Design, Vol 47 issue 2 (2015), pages 204-229. Together with Dima Elenbogen and Shmuel Katz. You can also get it here via Springerג€™s online-first.

Presentation

Preprocessing in Incremental SAT. Proc. of the 15th International conference on theory and applications of satisfiability testing (SAT'12). Together with Alexander Nadel and Vadim Ryvchin.

Presentation

Regression Verification for Multi-Threaded Programs. Proc. of 13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'12). Together with Sagar Chaki and Arie Gurfinkel. See also the full version.

Regression Verification for Multi-Threaded Programs (with extensions to locks and dynamic thread creation)

Formal Methods in Systems Design vol 47, no 3, pages 287-301. Available also through here via online-first. Together with Sagar Chaki and Arie Gurfinkel.

Presentation

(vsse talk)

Time-bounded analysis of real-time systems. Proc. of 11th Formal Methods in Computer Aided Design (FMCAD'11). Together with Sagar Chaki and Arie Gurfinkel.

Presentation

A probabilistic analysis of coverage methods. in ACM Transactions on Design Automation of Electronic Systems (ACM TDAES), Vol 16, No 4, article 38. Together with Laurent Fourier, Avi Ziv, and Ekaterina Kutsy.

Linear Completeness Thresholds for Bounded Model Checking. Proc. of Computer-Aided Verification (CAV'11). Together with Daniel Kroening, Joel Ouaknine, Thomas Wahl, and James Worrell.

Presentation

Faster Extraction of High-Level Minimal Unsatisfiable Cores. Proc. of Theory and applications of satisfiability testing (SAT'11). Pages 174 - 187. Together with Vadim Ryvchin. See the HHLMUC page.

(see above: Accelerated deletion-based extraction of minimal unsatisfiable cores / JSAT /2014)

Presentation

Variants of LTL query checking. Proc. of Haifa Verification Conference (HVC'10). Pages 76 - 92. Together with Hana Chockler and Arie Gurfinkel.

Presentation

A proof producing CSP solver. Proc. of the 24^th conference of the Association for the Advancement of Artificial Intelligence (AAAI'10). Together with Michael Veksler.

Presentation

(cspsat talk)

(PTHG-20 talk)

Decision Diagrams for Linear Arithmetic. Proc. of 9th Formal Methods in Computer Aided Design (FMCAD'09). Pages 53 - 60. Together with Sagar Chaki and Arie Gurfinkel.

Presentation

Regression Verification. Proc. of 46th Design Automation Conference (DAC'09). Pages 466 - 471. Together with Benny Godlin.

Regression verification: Proving the equivalence of similar programs. Software Testing, Verification and Reliability, 23(3) 241 -258, 2013. Together with Benny Godliln.

Presentation

Translation Validation: From Simulink to C. Proc. of Computer Aided Verification (CAV'09). Together with Michael Ryabtsev.

Presentation

A framework for satisfiability modulo theories-

Formal Aspects of Computing Journal. Vol. 21 (5) 2009, pages 485 - 494. Together with Daniel Kroening.

Easier and more informative vacuity checks Proc. of the Fifth ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'2007). Together with Hana Chockler.

Before and after vacuity.

Formal Methods in Systems Design. Vol. 34 (1) 2009, pages 37 - 58. Together with Hana Chockler.

Presentation

HaifaSat: a new robust SAT solver  Proc. of Haifa Verification Conference (HVC'05). LNCS vol. 3875, pages 76 - 89 . Together with Roman Gershman.

HaifaSat: a SAT solver based on an abstrction/refinement model. In JSAT - Journal on Satisfiability, Boolean Modeling and Computation. Vol. 6 (2008), pages 33 - 51. Together with Roman Gerhman.

Presentation

Beyond Vacuity: Towards the Strongest Passing Formula.

Proc. of the 8th conference on Formal Methods in Computer Aided Design (FMCAD'08). Pages 188 - 195. Together with Hana Chockler and Arie Gurfinkel.

Beyond Vacuity: Towards the strongest passing formula.

In Formal Methods in systems Design. Volume 43, Issue 3 (2013), Page 552-571.

Together with Hana Chockler and Arie Gurfinkel.

Presentation

Linear-time Reductions of Resolution Proofs. Proc. of Haifa Verification Conference (HVC 2008). LNCS 5394, pages 114 - 128. Together with Omer Bar-Ilan, Oded Fuhrmann, Shlomo Hoory and Ohad Shacham.

Reducing the Size of Resolution Proofs in Linear

Time. Journal on Software Tools and Technology Transfer (STTT), vol 13, issue 3, page 263, 2011. Together with Omer Bar-Ilan, Oded Fuhrmann, Shlomo Hoory and Ohad Shacham.

Presentation

A Theory-Based Decision Heuristic for DPLL(T). Proc. of the 8th conference on Formal Methods in Computer Aided Design (FMCAD'08). Pages 93 - 100. Together with Dan Goldwasser and Shai Fine.

Presentation

Optimized L*-based Assume-Guarantee Reasoning   Proc. of the Thirteenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07). Together with Sagar Chaki.

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.

Presentation

Deciding Bit-Vector Arithmetic with Abstraction   Proc. of the Thirteenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07). Together with Randal E. Bryant, Daniel Kroening, Joel Ouaknine, Sanjit Seshia and Bryan Brady.

An Abstraction-Based Decision Procedure for Bit-Vector Arithmetic. Software Tools and Technology Transfer (STTT) Vol. 11, pages 95 - 104 (2009). Together with Randal E. Bryant, Daniel Kroening, Joel Ouaknine, Sanjit Seshia and Bryan Brady.

Presentation

Inference Rules for Proving the Equivalence of

Recursive Procedures. (not peer-reviewed) Published in LNCS 6200: Time for verification - essays in memory of Amir Pnueli. Together with Benny Godlin.

Inference rules for proving the equivalence of recursive procedures. ACTA Informatica 45(6) pages 403 - 439, 2008. Together with Benny Godlin.

Presentation

Local restarts. Proc. of the eleventh International Conference on Theory and Applications of Satisfiability Testing (SAT'08),  LNCS 4996, pages 271 - 276. Together with Vadim Ryvchin.

Local restarts in SAT. In Constraint Programming Letters (CPL), Vol. 4, pages 3 - 13, 2008. Together with Vadim Ryvchin.

Presentation

Deriving small unsatisfiable cores with dominators  Proc. of the 18th International Conference on Computer Aided Verification (CAV'06). Together with Roman Gershman and Maya Koifman.

An approach for extracting an unsatisfiable core. Formal Methods in Systems Design, Vol. 33, pages 1 - 27, 2008. First published online in SpringerLink on March 2007. Together with Roman Gershman and Maya Koifman.

Presentation

Generating minimum transitivity constraints in P-time for deciding equality logic. Proc. of Satisfiability Modulo Theoies (SMT'07). Together with Mirron Rozanov. (Vol. 198, issue 2, pages 3 - 17 of Electronic Notes in Theoretical Computer Science (ENTCS)).

Presentation

Underapproximation for Model-Checking Based on Random Cryptographic Constructions Proc. of the 19th International Conference on Computer Aided Verification (CAV'07). LNCS 4590 pages 339 - 351. Together with Arie Matsliah. 

Underapproximation for Model-Checking Based on Universal Circuits. Information and Computation 208(4), April 2010, pages 315 - 326. Together with Arie Matsliah. (Also available from ScienceDirect) .

Presentation

Finite Instantiations in Equivalence Logic with Uninterpreted Functions Proc. of the 13th International Conference on Computer Aided Verification (CAV'01), vol. 2102 of Lecture Notes in Computer Science, pages 144 - 154, Paris, France, July 2001. Together with Yoav Rodeh.

Building small equality graphs for deciding Equality Logic with Uninterpreted Functions  Information and Computation 204 (2006), pages 26 - 59. Together with Yoav Rodeh.

Explaining Abstract Counterexamples  Foundations of Software Engineering (SIGSOFT - FSE12), pages 73 - 82, Newport Beach, California, Oct-Nov 2004. Together with S. Chaki and A. Groce.

Error Explanation with Distance Metrics  Intl. Journal on Software Tools for Technology Transfer (STTT), Vol. 8(3), pages 229 - 247, June 2006. (also available online from https://dx.doi.org/10.1007/s10009-005-0202-0) Together with A. Groce, S. Chaki and D. Kroening.

Regression Verification - a practical way to verify programs  VSTTE: Verified Software: theories, tools, experiments. LNCS 4171. Together with Benny Godlin.

Reduced Functional Consistency of Uninterpreted Functions. Pragmatics of Decision Procedures for Automated Reasoning (PDPAR'05), July 2005. ENTCS 898 (Vol.144, issue 2). (also available from Science-Direct, see here). Together with Amir Pnueli. 

Presentation

Cost-Effective Hyper-Resolution for Preprocessing CNF Formulas  (full version) Eighth International Conference on Theory and Applications of Satisfiability Testing (SAT'05). LNCS vol. 3569, pages 423 - 429. Together with Roman Gershman.

Yet another Decision Procedure for Equality Logic  Proc. of the 17th International Conference on Computer Aided Verification (CAV'05), LNCS vol. 3576, pages 307-320. Together with Orly Meir. You might-as-well read the full version or even Orly's thesis. See the technical report  for a solution to the problem posed in this publication. Also, please read this note.

Presentation

Abstraction Refinement for Bounded Model Checking Proc. of the 17th International Conference on Computer Aided Verification (CAV'05), LNCS vol. 3576, pages 112 - 124. Together with Anubhav Gupta. 

Presentation

Proof-guided underapproximation-widening for multi-process systems  Proc. of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL'05) pages 122 - 131, 2005. Together with Orna Grumberg, Flavio Lerda and Michael Theobald.

Completeness and Complexity of Bounded Model-Checking Proc. of the Fifth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2004). Together with E. Clarke, D. Kroening and J. Ouaknine.

Computational Challenges in Bounded Model Checking  Intl. Journal on Software Tools for Technology Transfer (STTT) Vol.7(2), pages 174-183, Apr 2005. Together with E. Clarke, D. Kroening and J. Ouaknine.

Presentation

Range Allocation for Separation Logic  Proc. of the 16th International Conference on Computer Aided Verification (CAV 2004). Together with M. Talupur, N. Sinha and A. Pnueli.

SAT based Abstraction-Refinement using ILP and Machine Learning Techniques Proc. of the 14th International Conference on Computer Aided Verification, 2002 (CAV'02), Copenhagen, Denmark, July 2002. Together with E. Clarke, A. Gupta and J. Kukula.

SAT based counterexample-guided abstraction-refinement  Transactions on Computer Aided Design (TCAD), Vol.23(7), July 2004, pages 1113 - 1123. Together with A. Gupta and E. Clarke.

Predicate Abstraction with Minimum Predicates Proc. of the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME'03), Oct 2003. Together with S. Chaki, E. Clarke and A. Groce.

Efficient Verification of Sequential and Concurrent C programs Journal on Formal Methods in Systems Design (FMSD). Vol. 25 (2-3), Sep - Nov 2004, pages 129-166. Together with S. Chaki, E. Clarke, A. Groce, J. Ouaknine and K. Yorav.

Presentation

Abstraction-Based Satisfiability Solving of Presburger Arithmetic  Proc. of the 16th International Conference on Computer Aided Verification (CAV 2004). Together with D. Kroening, J. Ouaknine and S. Seshia.

Pruning techniques for the SAT-based Bounded Model Checking Problem Proc. of the 11th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME'01), vol. 2144 of Lecture Notes in Computer Science, pages 58 - 70, Livingston, Scotland, Sep. 2001. 

Accelerating Bounded Model Checking of Safety Formulas. Formal Methods in System Design, Vol. 24(1), Jan 2004, pages 5-24. (This article combines and extends the articles that appeared in CAV'00 and CHARME'01. See below).

Presentation

Tuning SAT checkers for Bounded Model-Checking Proc. of the 12th International Conference on Computer Aided Verification, 2000 (CAV'00). The associated technical report can be downloaded from here (word file) or viewed from here (html). The Benchmark files can be downloaded from SATLIB. 

(see above: FMSD 24 (1), 2004).

Presentation

Efficient Computation of Recurrence Diameter Proc. of the Fourth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2003), Jan 2003. Together with D. Kroening.

Bounded Model Checking (Book chapter) Advances in Computers #58. Published in 2003. Together with A. Biere, A. Cimatti, E. Clarke and Y. Zhu. Please read this note.

Deciding Equality Formulas by Small Domains Instantiations Proc. of the 11th International Conference Computer Aided Verification, 1999 (CAV'99). Together with A. Pnueli, Y. Rodeh and M. Siegel.

The Small Model Property: How small can it be? Information and Computation, Vol. 178(1), Oct 2002, pages 279-293. Together with A. Pnueli, Y. Rodeh and M. Siegel.

Presentation

On Solving Presburger and Linear Arithmetic with SAT Proc. of Formal Methods in Computer-Aided Design (FMCAD'02). (Please read the note). 

Presentation

A Failed Attempt to Optimize Variable Ordering with Tools for Constraint Solving Proc. of the First International Workshop on Constraints in Formal Verification (CFV'02), Ithaca, New-York, Sep 2002. Together with E. Clarke.

Deciding separation formulas with SAT Proc. of the 14th International Conference on Computer Aided Verification, 2002 (CAV'02). Together with S. Seshia and R. Bryant.

Presentation

SAFEAIR: Advanced Design Tools for Aircraft Systems and Airborne Software Intl. conference on Dependable systems and networks (DSN'01). June 2001, Goteborg, Sweden. Together with P.Baufreton, F.Dupont, T.Lesergent, M.Segelken, H.Brinkmann and K.Winkelmann.

Range Allocation for Equivalence Logic Proc. of the 21st conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'01), Bangalore, India, December 2001. Together with Yoav Rodeh and Amir Pnueli.

Translation Validation: from SIGNAL to C (A Book chapter) In Correct System Design: Recent Insights and Advances, an LNCS State-of-the-Art Survey, Vol. 1710, pages 231-255, 1999. Together with A. Pnueli and M. Siegel.

The Code Validation Tool (CVT) - Automatic verification of code generated from synchronous languages Proc. of the intl. workshop of Software Tools for Technology Transfer (STTT'98). Together with A. Pnueli and M. Siegel.

The Code Validation Tool (CVT) - Automatic verification of a compilation process  Intl. Journal on Software Tools for Technology Transfer (STTT), Vol. 2(2), pages 192 - 201, 1998. Together with A. Pnueli and M. Siegel.

Translation Validation: From DC+ to C Proc. of the International Workshop on Current Trends in Applied Formal Method: Applied Formal Methods, Lecture Notes in Computer Science Vol. 1641, pages 137 - 150, 1998. Together with A. Pnueli and M. Siegel.

Translation Validation for Synchronous Languages Proc. of the 25th International Colloquium on Automata, Languages, and Programming (ICALP'98). Together with A. Pnueli and M. Siegel.