Ofer Strichman

ORCID

Publication Activity (10 Years)

Years Active: 1998-2024
Publications (10 Years): 24

Top Venues

CoRR

Formal Methods Syst. Des.

FMCAD

SAT

Publications

Shengping Xiao, Yongkang Li, Xinyue Huang, Yicong Xu, Jianwen Li, Geguang Pu, Ofer Strichman, Moshe Y. Vardi
Model-Guided Synthesis for LTL over Finite Traces. VMCAI (1) (2024)
Chaked R. J. Sayedoff, Ofer Strichman
Regression verification of unbalanced recursive functions with multiple calls (long version). CoRR (2022)
Xiaoyu Zhang, Shengping Xiao, Jianwen Li, Geguang Pu, Ofer Strichman
Combining BMC and Complementary Approximate Reachability to Accelerate Bug-Finding. ICCAD (2022)
Roderick Bloem, Hana Chockler, Masoud Ebrahimi, Ofer Strichman
Specifiable robustness in reactive synthesis. Formal Methods Syst. Des. 60 (2) (2022)
Dor Cohen, Ofer Strichman
Automated Repair of Neural Networks. CoRR (2022)
Yair Nof, Ofer Strichman
Real-time solving of computationally hard problems using optimal algorithm portfolios. Ann. Math. Artif. Intell. 89 (7) (2021)
Alexander Ivrii, Ofer Strichman
Exploiting Isomorphic Subgraphs in SAT (Long version). CoRR (2021)
Roderick Bloem, Hana Chockler, Masoud Ebrahimi, Ofer Strichman
Vacuity in synthesis. Formal Methods Syst. Des. 57 (3) (2021)
Alexander Ivrii, Ofer Strichman
Exploiting Isomorphic Subgraphs in SAT. FMCAD (2021)
Tomer Cohen, Lior Finkelman, Gal Grimberg, Gadi Shenhar, Ofer Strichman, Yonatan Strichman, Stav Yeger
A combination of 'pooling' with a prediction model can reduce by 73% the number of COVID-19 (Corona-virus) tests. CoRR (2020)
Hana Chockler, Pascal Kesseli, Daniel Kroening, Ofer Strichman
Learning the Language of Software Errors. J. Artif. Intell. Res. 67 (2020)
Roderick Bloem, Hana Chockler, Masoud Ebrahimi, Ofer Strichman
Synthesizing Reactive Systems Using Robustness and Recovery Specifications. FMCAD (2019)
Nir Drucker, Hsi-Ming Ho, Joël Ouaknine, Michal Penn, Ofer Strichman
Cyclic-routing of Unmanned Aerial Vehicles. J. Comput. Syst. Sci. 103 (2019)
Shuvendu K. Lahiri, Andrzej S. Murawski, Ofer Strichman, Mattias Ulbrich
Program Equivalence (Dagstuhl Seminar 18151). Dagstuhl Reports 8 (4) (2018)
Dor Cohen, Ofer Strichman
The Impact of Entropy and Solution Density on Selected SAT Heuristics. Entropy 20 (9) (2018)
Ofer Strichman
Special issue: program equivalence. Formal Methods Syst. Des. 52 (3) (2018)
Roderick Bloem, Hana Chockler, Masoud Ebrahimi, Ofer Strichman
Synthesizing Non-Vacuous Systems. VMCAI (2017)
Ofer Strichman
Near-Optimal Course Scheduling at the Technion. Interfaces 47 (6) (2017)
Dor Cohen, Ofer Strichman
The impact of Entropy and Solution Density on selected SAT heuristics. CoRR (2017)
Gabriel A. Moreno, Ofer Strichman, Sagar Chaki, Radislav Vaisman
Decision-Making with Cross-Entropy for Self-Adaptation. SEAMS@ICSE (2017)
Nir Drucker, Michal Penn, Ofer Strichman
Cyclic Routing of Unmanned Aerial Vehicles. CPAIOR (2016)
Ofer Guthmann, Ofer Strichman, Anna Trostanetski
Minimal unsatisfiable core extraction for SMT. FMCAD (2016)
Ofer Strichman, Maor Veitsman
Regression Verification for Unbalanced Recursive Functions. FM (2016)
Michael Veksler, Ofer Strichman
Learning general constraints in CSP. Artif. Intell. 238 (2016)
Sagar Chaki, Arie Gurfinkel, Ofer Strichman
Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation). Formal Methods Syst. Des. 47 (3) (2015)
Dima Elenbogen, Shmuel Katz, Ofer Strichman
Proving mutual termination. Formal Methods Syst. Des. 47 (2) (2015)
Radislav Vaisman, Ofer Strichman, Ilya B. Gertsbakh
Model Counting of Monotone Conjunctive Normal Form Formulas with Spectra. INFORMS J. Comput. 27 (2) (2015)
Alexander Ivrii, Vadim Ryvchin, Ofer Strichman
Mining Backbone Literals in Incremental SAT - A New Kind of Incremental Data. SAT (2015)
Martin Chapman, Hana Chockler, Pascal Kesseli, Daniel Kroening, Ofer Strichman, Michael Tautschnig
Learning the Language of Error. ATVA (2015)
Michael Veksler, Ofer Strichman
Learning General Constraints in CSP. CPAIOR (2015)
Alexander Nadel, Vadim Ryvchin, Ofer Strichman
Ultimately Incremental SAT. SAT (2014)
Alexander Nadel, Vadim Ryvchin, Ofer Strichman
Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores. J. Satisf. Boolean Model. Comput. 9 (1) (2014)
Hana Chockler, Arie Gurfinkel, Ofer Strichman
Beyond vacuity: towards the strongest passing formula. Formal Methods Syst. Des. 43 (3) (2013)
Sagar Chaki, Arie Gurfinkel, Ofer Strichman
Verifying periodic programs with priority inheritance locks. FMCAD (2013)
Ofer Strichman, Daniel Kroening
Preface to the special issue "SI: Satisfiability Modulo Theories". Formal Methods Syst. Des. 42 (1) (2013)
Alexander Nadel, Vadim Ryvchin, Ofer Strichman
Efficient MUS extraction with resolution. FMCAD (2013)
Benny Godlin, Ofer Strichman
Regression verification: proving the equivalence of similar programs. Softw. Test. Verification Reliab. 23 (3) (2013)
Batya Kenig, Avigdor Gal, Ofer Strichman
A New Class of Lineage Expressions over Probabilistic Databases Computable in P-Time. SUM (2013)
Sagar Chaki, Arie Gurfinkel, Soonho Kong, Ofer Strichman
Compositional Sequentialization of Periodic Programs. VMCAI (2013)
Sagar Chaki, Arie Gurfinkel, Ofer Strichman
Regression Verification for Multi-threaded Programs. VMCAI (2012)
Dima Elenbogen, Shmuel Katz, Ofer Strichman
Proving Mutual Termination of Programs. Haifa Verification Conference (2012)
Alexander Nadel, Vadim Ryvchin, Ofer Strichman
Preprocessing in Incremental SAT. SAT (2012)
Daniel Kroening, Joël Ouaknine, Ofer Strichman, Thomas Wahl, James Worrell
Linear Completeness Thresholds for Bounded Model Checking. CAV (2011)
Laurent Fournier, Avi Ziv, Ekaterina Kutsy, Ofer Strichman
A probabilistic analysis of coverage methods. ACM Trans. Design Autom. Electr. Syst. 16 (4) (2011)
Vadim Ryvchin, Ofer Strichman
Faster Extraction of High-Level Minimal Unsatisfiable Cores. SAT (2011)
Sagar Chaki, Arie Gurfinkel, Ofer Strichman
Time-bounded analysis of real-time systems. FMCAD (2011)
Omer Bar-Ilan, Oded Fuhrmann, Shlomo Hoory, Ohad Shacham, Ofer Strichman
Reducing the size of resolution proofs in linear time. Int. J. Softw. Tools Technol. Transf. 13 (3) (2011)
Benny Godlin, Ofer Strichman
Inference Rules for Proving the Equivalence of Recursive Procedures. Essays in Memory of Amir Pnueli (2010)
Arie Matsliah, Ofer Strichman
Underapproximation for model-checking based on universal circuits. Inf. Comput. 208 (4) (2010)
Hana Chockler, Arie Gurfinkel, Ofer Strichman
Variants of LTL Query Checking. Haifa Verification Conference (2010)
Michael Veksler, Ofer Strichman
A Proof-Producing CSP Solver. AAAI (2010)
Benny Godlin, Ofer Strichman
Regression verification. DAC (2009)
Roman Gershman, Ofer Strichman
HaifaSat: a SAT solver based on an Abstraction/Refinement model. J. Satisf. Boolean Model. Comput. 6 (1-3) (2009)
Hana Chockler, Ofer Strichman
Before and after vacuity. Formal Methods Syst. Des. 34 (1) (2009)
Ofer Strichman
Regression Verification: Proving the Equivalence of Similar Programs. CAV (2009)
Daniel Kroening, Ofer Strichman
A framework for Satisfiability Modulo Theories. Formal Aspects Comput. 21 (5) (2009)
Sagar Chaki, Arie Gurfinkel, Ofer Strichman
Decision diagrams for linear arithmetic. FMCAD (2009)
Michael Ryabtsev, Ofer Strichman
Translation Validation: From Simulink to C. CAV (2009)
Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady
An abstraction-based decision procedure for bit-vector arithmetic. Int. J. Softw. Tools Technol. Transf. 11 (2) (2009)
Benny Godlin, Ofer Strichman
Inference rules for proving the equivalence of recursive procedures. Acta Informatica 45 (6) (2008)
Sagar Chaki, Ofer Strichman
. Formal Methods Syst. Des. 32 (3) (2008)
Dan Goldwasser, Ofer Strichman, Shai Fine
A Theory-Based Decision Heuristic for DPLL(T). FMCAD (2008)
Mirron Rozanov, Ofer Strichman
Generating Minimum Transitivity Constraints in P-time for Deciding Equality Logic. Electron. Notes Theor. Comput. Sci. 198 (2) (2008)
Vadim Ryvchin, Ofer Strichman
Local Restarts. SAT (2008)
Hana Chockler, Arie Gurfinkel, Ofer Strichman
Beyond Vacuity: Towards the Strongest Passing Formula. FMCAD (2008)
Omer Bar-Ilan, Oded Fuhrmann, Shlomo Hoory, Ohad Shacham, Ofer Strichman
Linear-Time Reductions of Resolution Proofs. Haifa Verification Conference (2008)
Roman Gershman, Maya Koifman, Ofer Strichman
An approach for extracting a small unsatisfiable core. Formal Methods Syst. Des. 33 (1-3) (2008)
Hana Chockler, Ofer Strichman
Easier and More Informative Vacuity Checks. MEMOCODE (2007)
Ofer Strichman, Armin Biere
Preface. Electron. Notes Theor. Comput. Sci. 174 (3) (2007)
Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady
Deciding Bit-Vector Arithmetic with Abstraction. TACAS (2007)
Sagar Chaki, Ofer Strichman
Optimized L*-Based Assume-Guarantee Reasoning. TACAS (2007)
Arie Matsliah, Ofer Strichman
Underapproximation for Model-Checking Based on Random Cryptographic Constructions. CAV (2007)
Yoav Rodeh, Ofer Strichman
Building small equality graphs for deciding equality logic with uninterpreted functions. Inf. Comput. 204 (1) (2006)
Amir Pnueli, Ofer Strichman
Reduced Functional Consistency of Uninterpreted Functions. Electron. Notes Theor. Comput. Sci. 144 (2) (2006)
Armin Biere, Ofer Strichman
Preface. Electron. Notes Theor. Comput. Sci. 144 (1) (2006)
Roman Gershman, Maya Koifman, Ofer Strichman
Deriving Small Unsatisfiable Cores with Dominators. CAV (2006)
Alex Groce, Sagar Chaki, Daniel Kroening, Ofer Strichman
Error explanation with distance metrics. Int. J. Softw. Tools Technol. Transf. 8 (3) (2006)
Roman Gershman, Ofer Strichman
Cost-Effective Hyper-Resolution for Preprocessing CNF Formulas. SAT (2005)
Anubhav Gupta, Ofer Strichman
Abstraction Refinement for Bounded Model Checking. CAV (2005)
Orly Meir, Ofer Strichman
Yet Another Decision Procedure for Equality Logic. CAV (2005)
Roman Gershman, Ofer Strichman
HaifaSat: A New Robust SAT Solver. Haifa Verification Conference (2005)
Armin Biere, Ofer Strichman
Introductory paper. Int. J. Softw. Tools Technol. Transf. 7 (2) (2005)
Orna Grumberg, Flavio Lerda, Ofer Strichman, Michael Theobald
Proof-guided underapproximation-widening for multi-process systems. POPL (2005)
Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman
Computational challenges in bounded model checking. Int. J. Softw. Tools Technol. Transf. 7 (2) (2005)
Ofer Strichman, Benny Godlin
Regression Verification - A Practical Way to Verify Programs. VSTTE (2005)
Armin Biere, Ofer Strichman
Preface. Electron. Notes Theor. Comput. Sci. 119 (2) (2005)
Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman
Completeness and Complexity of Bounded Model Checking. VMCAI (2004)
Ofer Strichman
Deciding Disjunctive Linear Arithmetic with SAT CoRR (2004)
Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman
Abstraction-Based Satisfiability Solving of Presburger Arithmetic. CAV (2004)
Sagar Chaki, Edmund M. Clarke, Alex Groce, Joël Ouaknine, Ofer Strichman, Karen Yorav
Efficient Verification of Sequential and Concurrent C Programs. Formal Methods Syst. Des. 25 (2-3) (2004)
Muralidhar Talupur, Nishant Sinha, Ofer Strichman, Amir Pnueli
Range Allocation for Separation Logic. CAV (2004)
Edmund M. Clarke, Anubhav Gupta, Ofer Strichman
SAT-based counterexample-guided abstraction refinement. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 23 (7) (2004)
Ofer Strichman
Accelerating Bounded Model Checking of Safety Properties. Formal Methods Syst. Des. 24 (1) (2004)
Sagar Chaki, Alex Groce, Ofer Strichman
Explaining abstract counterexamples. SIGSOFT FSE (2004)
Daniel Kroening, Ofer Strichman
Efficient Computation of Recurrence Diameters. VMCAI (2003)
Sagar Chaki, Edmund M. Clarke, Alex Groce, Ofer Strichman
Predicate Abstraction with Minimum Predicates. CHARME (2003)
Ofer Strichman, Armin Biere
Preface. Electron. Notes Theor. Comput. Sci. 89 (4) (2003)
Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, Yunshan Zhu
Bounded model checking. Adv. Comput. 58 (2003)
Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel
Erratum ("The small model property: how small can it be?" Volume 178, Number 1 [2002], pages 279-293). Inf. Comput. 184 (1) (2003)
Edmund M. Clarke, Anubhav Gupta, James H. Kukula, Ofer Strichman
SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques. CAV (2002)

Ofer Strichman.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Ofer Strichman