Translation Validation: From DC+ to C*. - Amir Pnueli; Ofer Strichman; Michael Siegel (FM-Trends, 1998)

Translation Validation for Synchronous Languages. - Amir Pnueli; Ofer Strichman; Michael Siegel (ICALP, 1998)

The Code Validation Tool CVT: Automatic Verification of a Compilation Process. - Amir Pnueli; Ofer Strichman; Michael Siegel (Int. J. Softw. Tools Technol. Transf., 1998)

Translation Validation: From SIGNAL to C. - Amir Pnueli; Ofer Strichman; Michael Siegel (Correct System Design, 1999)

Deciding Equality Formulas by Small Domains Instantiations. - Amir Pnueli; Yoav Rodeh; Ofer Strichman; Michael Siegel (CAV, 1999)

Tuning SAT Checkers for Bounded Model Checking. - Ofer Strichman (CAV, 2000)

Finite Instantiations in Equivalence Logic with Uninterpreted Functions. - Yoav Rodeh; Ofer Strichman (CAV, 2001)

Pruning Techniques for the SAT-Based Bounded Model Checking Problem. - Ofer Strichman (CHARME, 2001)

Range Allocation for Equivalence Logic. - Amir Pnueli; Yoav Rodeh; Ofer Strichman (FSTTCS, 2001)

Using Simulation to Increase Efficiency in an Army Recruitment Office. - Ofer Shtrichman; Rami Ben-Haim; Moshe Asher Pollatschek (Interfaces, 2001)

SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques. - Edmund M. Clarke; Anubhav Gupta 001; James H. Kukula; Ofer Strichman (CAV, 2002)

Deciding Separation Formulas with SAT. - Ofer Strichman; Sanjit A. Seshia; Randal E. Bryant (CAV, 2002)

On Solving Presburger and Linear Arithmetic with SAT. - Ofer Strichman (FMCAD, 2002)

The Small Model Property: How Small Can It Be? - Amir Pnueli; Yoav Rodeh; Ofer Strichman; Michael Siegel (Inf. Comput., 2002)

Predicate Abstraction with Minimum Predicates. - Sagar Chaki; Edmund M. Clarke; Alex Groce; Ofer Strichman (CHARME, 2003)

Efficient Computation of Recurrence Diameters. - Daniel Kroening; Ofer Strichman (VMCAI, 2003)

Bounded model checking. - Armin Biere; Alessandro Cimatti; Edmund M. Clarke; Ofer Strichman; Yunshan Zhu (Adv. Comput., 2003)

Erratum ("The small model property: how small can it be?" Volume 178, Number 1 [2002], pages 279-293). - Amir Pnueli; Yoav Rodeh; Ofer Strichman; Michael Siegel (Inf. Comput., 2003)

Abstraction-Based Satisfiability Solving of Presburger Arithmetic. - Daniel Kroening; Joël Ouaknine; Sanjit A. Seshia; Ofer Strichman (CAV, 2004)

Range Allocation for Separation Logic. - Muralidhar Talupur; Nishant Sinha 001; Ofer Strichman; Amir Pnueli (CAV, 2004)

Explaining abstract counterexamples. - Sagar Chaki; Alex Groce; Ofer Strichman (SIGSOFT FSE, 2004)

Completeness and Complexity of Bounded Model Checking. - Edmund M. Clarke; Daniel Kroening; Joël Ouaknine; Ofer Strichman (VMCAI, 2004)

Deciding Disjunctive Linear Arithmetic with SAT - Ofer Strichman (CoRR, 2004)

Preface. - Armin Biere; Ofer Strichman (BMC@CAV, 2004)

Efficient Verification of Sequential and Concurrent C Programs. - Sagar Chaki; Edmund M. Clarke; Alex Groce; Joël Ouaknine; Ofer Strichman; Karen Yorav (Formal Methods Syst. Des., 2004)

Accelerating Bounded Model Checking of Safety Properties. - Ofer Strichman (Formal Methods Syst. Des., 2004)

SAT-based counterexample-guided abstraction refinement. - Edmund M. Clarke; Anubhav Gupta 001; Ofer Strichman (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2004)

Abstraction Refinement for Bounded Model Checking. - Anubhav Gupta 001; Ofer Strichman (CAV, 2005)

Yet Another Decision Procedure for Equality Logic. - Orly Meir; Ofer Strichman (CAV, 2005)

HaifaSat: A New Robust SAT Solver. - Roman Gershman; Ofer Strichman (Haifa Verification Conference, 2005)

Proof-guided underapproximation-widening for multi-process systems. - Orna Grumberg; Flavio Lerda; Ofer Strichman; Michael Theobald (POPL, 2005)

Cost-Effective Hyper-Resolution for Preprocessing CNF Formulas. - Roman Gershman; Ofer Strichman (SAT, 2005)

Regression Verification - A Practical Way to Verify Programs. - Ofer Strichman; Benny Godlin (VSTTE, 2005)

Reduced Functional Consistency of Uninterpreted Functions. - Amir Pnueli; Ofer Strichman (PDPAR@CAV, 2005)

Introductory paper. - Armin Biere; Ofer Strichman (Int. J. Softw. Tools Technol. Transf., 2005)

Computational challenges in bounded model checking. - Edmund M. Clarke; Daniel Kroening; Joël Ouaknine; Ofer Strichman (Int. J. Softw. Tools Technol. Transf., 2005)

Deriving Small Unsatisfiable Cores with Dominators. - Roman Gershman; Maya Koifman; Ofer Strichman (CAV, 2006)

Building small equality graphs for deciding equality logic with uninterpreted functions. - Yoav Rodeh; Ofer Strichman (Inf. Comput., 2006)

Error explanation with distance metrics. - Alex Groce; Sagar Chaki; Daniel Kroening; Ofer Strichman (Int. J. Softw. Tools Technol. Transf., 2006)

Underapproximation for Model-Checking Based on Random Cryptographic Constructions. - Arie Matsliah; Ofer Strichman (CAV, 2007)

Easier and More Informative Vacuity Checks. - Hana Chockler; Ofer Strichman (MEMOCODE, 2007)

Deciding Bit-Vector Arithmetic with Abstraction. - Randal E. Bryant; Daniel Kroening; Joël Ouaknine; Sanjit A. Seshia; Ofer Strichman; Bryan A. Brady (TACAS, 2007)

Optimized L*-Based Assume-Guarantee Reasoning. - Sagar Chaki; Ofer Strichman (TACAS, 2007)

Generating Minimum Transitivity Constraints in P-time for Deciding Equality Logic. - Mirron Rozanov; Ofer Strichman (SMT@CAV, 2007)

A Theory-Based Decision Heuristic for DPLL(T). - Dan Goldwasser; Ofer Strichman; Shai Fine (FMCAD, 2008)

Linear-Time Reductions of Resolution Proofs. - Omer Bar-Ilan; Oded Fuhrmann; Shlomo Hoory; Ohad Shacham; Ofer Strichman (Haifa Verification Conference, 2008)

Local Restarts. - Vadim Ryvchin; Ofer Strichman (SAT, 2008)

Inference rules for proving the equivalence of recursive procedures. - Benny Godlin; Ofer Strichman (Acta Informatica, 2008)

Three optimizations for Assume-Guarantee reasoning with L*. - Sagar Chaki; Ofer Strichman (Formal Methods Syst. Des., 2008)

An approach for extracting a small unsatisfiable core. - Roman Gershman; Maya Koifman; Ofer Strichman (Formal Methods Syst. Des., 2008)

Decision Procedures - An Algorithmic Point of View - Daniel Kroening; Ofer Strichman (Springer, 2008)

Translation Validation: From Simulink to C. - Michael Ryabtsev; Ofer Strichman (CAV, 2009)

Regression Verification: Proving the Equivalence of Similar Programs. - Ofer Strichman (CAV, 2009)

Regression verification. - Benny Godlin; Ofer Strichman (DAC, 2009)

Decision diagrams for linear arithmetic. - Sagar Chaki; Arie Gurfinkel; Ofer Strichman (FMCAD, 2009)

A framework for Satisfiability Modulo Theories. - Daniel Kroening; Ofer Strichman (Formal Aspects Comput., 2009)

Before and after vacuity. - Hana Chockler; Ofer Strichman (Formal Methods Syst. Des., 2009)

HaifaSat: a SAT solver based on an Abstraction/Refinement model. - Roman Gershman; Ofer Strichman (J. Satisf. Boolean Model. Comput., 2009)

An abstraction-based decision procedure for bit-vector arithmetic. - Randal E. Bryant; Daniel Kroening; Joël Ouaknine; Sanjit A. Seshia; Ofer Strichman; Bryan A. Brady (Int. J. Softw. Tools Technol. Transf., 2009)

A Proof-Producing CSP Solver. - Michael Veksler; Ofer Strichman (AAAI, 2010)

Variants of LTL Query Checking. - Hana Chockler; Arie Gurfinkel; Ofer Strichman (Haifa Verification Conference, 2010)

Underapproximation for model-checking based on universal circuits. - Arie Matsliah; Ofer Strichman (Inf. Comput., 2010)

Linear Completeness Thresholds for Bounded Model Checking. - Daniel Kroening; Joël Ouaknine; Ofer Strichman; Thomas Wahl; James Worrell 001 (CAV, 2011)

Time-bounded analysis of real-time systems. - Sagar Chaki; Arie Gurfinkel; Ofer Strichman (FMCAD, 2011)

Faster Extraction of High-Level Minimal Unsatisfiable Cores. - Vadim Ryvchin; Ofer Strichman (SAT, 2011)

Reducing the size of resolution proofs in linear time. - Omer Bar-Ilan; Oded Fuhrmann; Shlomo Hoory; Ohad Shacham; Ofer Strichman (Int. J. Softw. Tools Technol. Transf., 2011)

A probabilistic analysis of coverage methods. - Laurent Fournier; Avi Ziv; Ekaterina Kutsy; Ofer Strichman (ACM Trans. Design Autom. Electr. Syst., 2011)

Proving Mutual Termination of Programs. - Dima Elenbogen; Shmuel Katz; Ofer Strichman (Haifa Verification Conference, 2012)

Preprocessing in Incremental SAT. - Alexander Nadel; Vadim Ryvchin; Ofer Strichman (SAT, 2012)

Regression Verification for Multi-threaded Programs. - Sagar Chaki; Arie Gurfinkel; Ofer Strichman (VMCAI, 2012)

Verifying periodic programs with priority inheritance locks. - Sagar Chaki; Arie Gurfinkel; Ofer Strichman (FMCAD, 2013)

Efficient MUS extraction with resolution. - Alexander Nadel; Vadim Ryvchin; Ofer Strichman (FMCAD, 2013)

A New Class of Lineage Expressions over Probabilistic Databases Computable in P-Time. - Batya Kenig; Avigdor Gal; Ofer Strichman (SUM, 2013)

Compositional Sequentialization of Periodic Programs. - Sagar Chaki; Arie Gurfinkel; Soonho Kong; Ofer Strichman (VMCAI, 2013)

Beyond vacuity: towards the strongest passing formula. - Hana Chockler; Arie Gurfinkel; Ofer Strichman (Formal Methods Syst. Des., 2013)

Preface to the special issue "SI: Satisfiability Modulo Theories". - Ofer Strichman; Daniel Kroening (Formal Methods Syst. Des., 2013)

Regression verification: proving the equivalence of similar programs. - Benny Godlin; Ofer Strichman (Softw. Test. Verification Reliab., 2013)

Ultimately Incremental SAT. - Alexander Nadel; Vadim Ryvchin; Ofer Strichman (SAT, 2014)

Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores. - Alexander Nadel; Vadim Ryvchin; Ofer Strichman (J. Satisf. Boolean Model. Comput., 2014)

Learning the Language of Error. - Martin Chapman; Hana Chockler; Pascal Kesseli; Daniel Kroening; Ofer Strichman; Michael Tautschnig (ATVA, 2015)

Mining Backbone Literals in Incremental SAT - A New Kind of Incremental Data. - Alexander Ivrii; Vadim Ryvchin; Ofer Strichman (SAT, 2015)

Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation). - Sagar Chaki; Arie Gurfinkel; Ofer Strichman (Formal Methods Syst. Des., 2015)

Proving mutual termination. - Dima Elenbogen; Shmuel Katz; Ofer Strichman (Formal Methods Syst. Des., 2015)

Model Counting of Monotone Conjunctive Normal Form Formulas with Spectra. - Radislav Vaisman; Ofer Strichman; Ilya B. Gertsbakh (INFORMS J. Comput., 2015)

Cyclic Routing of Unmanned Aerial Vehicles. - Nir Drucker; Michal Penn; Ofer Strichman (CPAIOR, 2016)

Regression Verification for Unbalanced Recursive Functions. - Ofer Strichman; Maor Veitsman (FM, 2016)

Minimal unsatisfiable core extraction for SMT. - Ofer Guthmann; Ofer Strichman; Anna Trostanetski (FMCAD, 2016)

Learning general constraints in CSP. - Michael Veksler; Ofer Strichman (Artif. Intell., 2016)

Decision Procedures - An Algorithmic Point of View, Second Edition - Daniel Kroening; Ofer Strichman (Springer, 2016)

Decision-Making with Cross-Entropy for Self-Adaptation. - Gabriel A. Moreno; Ofer Strichman; Sagar Chaki; Radislav Vaisman (SEAMS@ICSE, 2017)

Synthesizing Non-Vacuous Systems. - Roderick Bloem; Hana Chockler; Masoud Ebrahimi 002; Ofer Strichman (VMCAI, 2017)

Near-Optimal Course Scheduling at the Technion. - Ofer Strichman (Interfaces, 2017)

Program Equivalence (Dagstuhl Seminar 18151). - Shuvendu K. Lahiri; Andrzej S. Murawski; Ofer Strichman; Mattias Ulbrich (Dagstuhl Reports, 2018)

The Impact of Entropy and Solution Density on Selected SAT Heuristics. - Dor Cohen; Ofer Strichman (Entropy, 2018)

Special issue: program equivalence. - Ofer Strichman (Formal Methods Syst. Des., 2018)

Synthesizing Reactive Systems Using Robustness and Recovery Specifications. - Roderick Bloem; Hana Chockler; Masoud Ebrahimi 002; Ofer Strichman (FMCAD, 2019)

Cyclic-routing of Unmanned Aerial Vehicles. - Nir Drucker; Hsi-Ming Ho; Joël Ouaknine; Michal Penn; Ofer Strichman (J. Comput. Syst. Sci., 2019)

A combination of 'pooling' with a prediction model can reduce by 73% the number of COVID-19 (Corona-virus) tests. - Tomer Cohen; Lior Finkelman; Gal Grimberg; Gadi Shenhar; Ofer Strichman; Yonatan Strichman; Stav Yeger (CoRR, 2020)

Learning the Language of Software Errors. - Hana Chockler; Pascal Kesseli; Daniel Kroening; Ofer Strichman (J. Artif. Intell. Res., 2020)

Exploiting Isomorphic Subgraphs in SAT. - Alexander Ivrii; Ofer Strichman (FMCAD, 2021)

Real-time solving of computationally hard problems using optimal algorithm portfolios. - Yair Nof; Ofer Strichman (Ann. Math. Artif. Intell., 2021)

Exploiting Isomorphic Subgraphs in SAT (Long version). - Alexander Ivrii; Ofer Strichman (CoRR, 2021)

Vacuity in synthesis. - Roderick Bloem; Hana Chockler; Masoud Ebrahimi 002; Ofer Strichman (Formal Methods Syst. Des., 2021)

Combining BMC and Complementary Approximate Reachability to Accelerate Bug-Finding. - Xiaoyu Zhang; Shengping Xiao; Jianwen Li; Geguang Pu; Ofer Strichman (ICCAD, 2022)

Automated Repair of Neural Networks. - Dor Cohen; Ofer Strichman (CoRR, 2022)

Regression verification of unbalanced recursive functions with multiple calls (long version). - Chaked R. J. Sayedoff; Ofer Strichman (CoRR, 2022)

Specifiable robustness in reactive synthesis. - Roderick Bloem; Hana Chockler; Masoud Ebrahimi 002; Ofer Strichman (Formal Methods Syst. Des., 2022)

Model-Guided Synthesis for LTL over Finite Traces. - Shengping Xiao; Yongkang Li; Xinyue Huang; Yicong Xu; Jianwen Li; Geguang Pu; Ofer Strichman; Moshe Y. Vardi (VMCAI (1), 2024)

Revisiting Assumptions Ordering in CAR-Based Model Checking. - Yibo Dong 001; Yu Chen; Jianwen Li; Geguang Pu; Ofer Strichman (CoRR, 2024)