Comments:

1. The Bibtex entries for the items below can be found in my DBLP record 

2. Citation information can be seen in my profile at Google scholar

3. Prior to mid 2001 (when I came to the US) I spelled my name Shtrichman rather than Strichman. This is the reason for the inconsistent spelling in the articles.

4. The list below includes my articles in verification. Other publications (mostly in operations research) can be found at the bottom of this page.

 

Conference version

Journal version

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 12th 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.

 

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.

 

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 13th 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 13th 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 24th conference of the Association for the Advancement of Artificial Intelligence (AAAI'10). Together with Michael Veksler.

 

Presentation

(cspsat 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 ArithmeticSoftware 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 http://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.

 

 

 

Books

·           Decision Procedures - an algorithmic point of view Together with Daniel Kroening.

·  Efficient Decision Procedures for Validation This is just my PhD thesis + new introduction that for some reason some publisher decided to re-publish as a book. You can also see it here for free.

·         (Editor. Together with Stefan Szeider) Proceedings of SAT 2010 - Thirteenth International Conference on Theory and Applications of Satisfiability Testing.

 

Other publications

 

In Operations Research:

·           Cyclic Routing of Unmanned Aerial Vehicles. Proc. 13th International Conference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming (CPAIOR 2016). Together with Nir Drucker and Michal Penn. Presentation.

·           Using Simulation to Increase Efficiency in an Army Recruitment Office  'Interfaces' - an International Journal of INFORMS, the Institute of Operation Research and Management Science, Vol. 31(4) July-August 2001, pages 61-70. Together with R. Ben-Haim and M. Pollatschek.

·           A Two-Tier Hierarchical Scheduler for the Micro-Electronic Industry International Journal of Production Economics, Vol. 25, 1991. Together with E. Darel, P. Sofer and I. Molcho.       

 

In Testing:

·           The 'Logic Assurance (LA)' System - A Tool for Testing and Controlling Real-Time Systems Proc. of the 8th Israeli Conference on Computer Systems and Software Engineering (IEEE - ISySE97). Together with R. Goldring. Also see A Paper in Hebrew describing LA, published in the Israeli Engineers' Association Journal, Feb. 1996. Together with R. Goldring.

 

Patents

·         Device, System and Method of Underapproximated Model-Checking, 2007, together with Arie Matsliah. 

·         Clause and proof tightening, 2007, together with Oded Fuhrmann and Ohad Shacham.  

·         Sharing information between SAT instances, Dec 2000 Patent cover page. Full text can be found in the US paten's office web page here.

Technical Reports

·         Linear-time Reductions of Resolution Proofs (full version) Technical report IE/IS-2008-02. Together with Omer Bar-Ilan, Oded Fuhrmann, Shlomo Hoory and Ohad Shacham.

·         Underapproximation for Model-Checking Based on Universal Circuits (Full version) Technical report IE/IS-2007-07. Together with Arie Matsliah.

·         Easier and more informative vacuity checks (full version) Technical report TR-07-IEM/ISE-02. Together with Hana Chockler.

·         Generating minimum transitivity constraints in P-time for deciding equality logic Technical report IEM/ ISE-1-TR-07. Together with Mirron Rozanov.

·         Advances in Counterexample-Guided Abstraction/Refinement Technical report (CMU-CS-03-180), Edited together with E. Clarke.

·         Optimizations in Decision Procedures for Propositional Linear Inequalities Technical report (CMU-CS-02-133). (Please read the note about this report).