| 2024 | VMCAI | 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 |
| 2022 | ICCAD | Combining BMC and Complementary Approximate Reachability to Accelerate Bug-Finding. | Xiaoyu Zhang, Shengping Xiao, Jianwen Li, Geguang Pu, Ofer Strichman |
| 2021 | FMCAD | Exploiting Isomorphic Subgraphs in SAT. | Alexander Ivrii, Ofer Strichman |
| 2019 | FMCAD | Synthesizing Reactive Systems Using Robustness and Recovery Specifications. | Roderick Bloem, Hana Chockler, Masoud Ebrahimi, Ofer Strichman |
| 2017 | ICSE | Decision-Making with Cross-Entropy for Self-Adaptation. | Gabriel A. Moreno, Ofer Strichman, Sagar Chaki, Radislav Vaisman |
| 2017 | VMCAI | Synthesizing Non-Vacuous Systems. | Roderick Bloem, Hana Chockler, Masoud Ebrahimi, Ofer Strichman |
| 2016 | CPAIOR | Cyclic Routing of Unmanned Aerial Vehicles. | Nir Drucker, Michal Penn, Ofer Strichman |
| 2016 | FM | Regression Verification for Unbalanced Recursive Functions. | Ofer Strichman, Maor Veitsman |
| 2016 | FMCAD | Minimal unsatisfiable core extraction for SMT. | Ofer Guthmann, Ofer Strichman, Anna Trostanetski |
| 2015 | ATVA | Learning the Language of Error. | Martin Chapman, Hana Chockler, Pascal Kesseli, Daniel Kroening, Ofer Strichman, Michael Tautschnig |
| 2015 | CPAIOR | Learning General Constraints in CSP. | Michael Veksler, Ofer Strichman |
| 2015 | SAT | Mining Backbone Literals in Incremental SAT - A New Kind of Incremental Data. | Alexander Ivrii, Vadim Ryvchin, Ofer Strichman |
| 2014 | SAT | Ultimately Incremental SAT. | Alexander Nadel, Vadim Ryvchin, Ofer Strichman |
| 2013 | FMCAD | Verifying periodic programs with priority inheritance locks. | Sagar Chaki, Arie Gurfinkel, Ofer Strichman |
| 2013 | FMCAD | Efficient MUS extraction with resolution. | Alexander Nadel, Vadim Ryvchin, Ofer Strichman |
| 2013 | VMCAI | Compositional Sequentialization of Periodic Programs. | Sagar Chaki, Arie Gurfinkel, Soonho Kong, Ofer Strichman |
| 2012 | SAT | Preprocessing in Incremental SAT. | Alexander Nadel, Vadim Ryvchin, Ofer Strichman |
| 2012 | VMCAI | Regression Verification for Multi-threaded Programs. | Sagar Chaki, Arie Gurfinkel, Ofer Strichman |
| 2011 | CAV | Linear Completeness Thresholds for Bounded Model Checking. | Daniel Kroening, Jol Ouaknine, Ofer Strichman, Thomas Wahl, James Worrell |
| 2011 | FMCAD | Time-bounded analysis of real-time systems. | Sagar Chaki, Arie Gurfinkel, Ofer Strichman |
| 2011 | SAT | Faster Extraction of High-Level Minimal Unsatisfiable Cores. | Vadim Ryvchin, Ofer Strichman |
| 2010 | AAAI | A Proof-Producing CSP Solver. | Michael Veksler, Ofer Strichman |
| 2009 | CAV | Translation Validation: From Simulink to C. | Michael Ryabtsev, Ofer Strichman |
| 2009 | CAV | Regression Verification: Proving the Equivalence of Similar Programs. | Ofer Strichman |
| 2009 | DAC | Regression verification. | Benny Godlin, Ofer Strichman |
| 2009 | FMCAD | Decision diagrams for linear arithmetic. | Sagar Chaki, Arie Gurfinkel, Ofer Strichman |
| 2008 | FMCAD | Beyond Vacuity: Towards the Strongest Passing Formula. | Hana Chockler, Arie Gurfinkel, Ofer Strichman |
| 2008 | FMCAD | A Theory-Based Decision Heuristic for DPLL(T). | Dan Goldwasser, Ofer Strichman, Shai Fine |
| 2008 | SAT | Local Restarts. | Vadim Ryvchin, Ofer Strichman |
| 2007 | CAV | Underapproximation for Model-Checking Based on Random Cryptographic Constructions. | Arie Matsliah, Ofer Strichman |
| 2007 | MEMOCODE | Easier and More Informative Vacuity Checks. | Hana Chockler, Ofer Strichman |
| 2007 | TACAS | Deciding Bit-Vector Arithmetic with Abstraction. | Randal E. Bryant, Daniel Kroening, Jol Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady |
| 2007 | TACAS | Optimized L*-Based Assume-Guarantee Reasoning. | Sagar Chaki, Ofer Strichman |
| 2006 | CAV | Deriving Small Unsatisfiable Cores with Dominators. | Roman Gershman, Maya Koifman, Ofer Strichman |
| 2005 | CAV | Abstraction Refinement for Bounded Model Checking. | Anubhav Gupta, Ofer Strichman |
| 2005 | CAV | Yet Another Decision Procedure for Equality Logic. | Orly Meir, Ofer Strichman |
| 2005 | POPL | Proof-guided underapproximation-widening for multi-process systems. | Orna Grumberg, Flavio Lerda, Ofer Strichman, Michael Theobald |
| 2005 | SAT | Cost-Effective Hyper-Resolution for Preprocessing CNF Formulas. | Roman Gershman, Ofer Strichman |
| 2004 | CAV | Abstraction-Based Satisfiability Solving of Presburger Arithmetic. | Daniel Kroening, Jol Ouaknine, Sanjit A. Seshia, Ofer Strichman |
| 2004 | CAV | Range Allocation for Separation Logic. | Muralidhar Talupur, Nishant Sinha, Ofer Strichman, Amir Pnueli |
| 2004 | VMCAI | Completeness and Complexity of Bounded Model Checking. | Edmund M. Clarke, Daniel Kroening, Jol Ouaknine, Ofer Strichman |
| 2003 | VMCAI | Efficient Computation of Recurrence Diameters. | Daniel Kroening, Ofer Strichman |
| 2002 | CAV | SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques. | Edmund M. Clarke, Anubhav Gupta, James H. Kukula, Ofer Strichman |
| 2002 | CAV | Deciding Separation Formulas with SAT. | Ofer Strichman, Sanjit A. Seshia, Randal E. Bryant |
| 2002 | FMCAD | On Solving Presburger and Linear Arithmetic with SAT. | Ofer Strichman |
| 2001 | CAV | Finite Instantiations in Equivalence Logic with Uninterpreted Functions. | Yoav Rodeh, Ofer Strichman |
| 2000 | CAV | Tuning SAT Checkers for Bounded Model Checking. | Ofer Strichman |
| 1999 | CAV | Deciding Equality Formulas by Small Domains Instantiations. | Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel |
| 1998 | FM | Translation Validation: From DC+ to C*. | Amir Pnueli, Ofer Strichman, Michael Siegel |
| 1998 | ICALP | Translation Validation for Synchronous Languages. | Amir Pnueli, Ofer Strichman, Michael Siegel |