Ofer Strichman

124 papers A* 18A 11B 19C 1Journal 46Unranked 22

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