| 2008 |
| 45 | EE | Vadim Ryvchin,
Ofer Strichman:
Local Restarts.
SAT 2008: 271-276 |
| 44 | EE | Sagar Chaki,
Ofer Strichman:
Three optimizations for Assume-Guarantee reasoning with L*.
Formal Methods in System Design 32(3): 267-284 (2008) |
| 2007 |
| 43 | EE | Arie Matsliah,
Ofer Strichman:
Underapproximation for Model-Checking Based on Random Cryptographic Constructions.
CAV 2007: 339-351 |
| 42 | EE | Hana Chockler,
Ofer Strichman:
Easier and More Informative Vacuity Checks.
MEMOCODE 2007: 189-198 |
| 41 | EE | Sagar Chaki,
Ofer Strichman:
Optimized L*-Based Assume-Guarantee Reasoning.
TACAS 2007: 276-291 |
| 40 | EE | Randal E. Bryant,
Daniel Kroening,
Joël Ouaknine,
Sanjit A. Seshia,
Ofer Strichman,
Bryan A. Brady:
Deciding Bit-Vector Arithmetic with Abstraction.
TACAS 2007: 358-372 |
| 39 | EE | Ofer Strichman,
Armin Biere:
Preface.
Electr. Notes Theor. Comput. Sci. 174(3): 1-2 (2007) |
| 2006 |
| 38 | EE | Roman Gershman,
Maya Koifman,
Ofer Strichman:
Deriving Small Unsatisfiable Cores with Dominators.
CAV 2006: 109-122 |
| 37 | EE | Armin Biere,
Ofer Strichman:
Preface.
Electr. Notes Theor. Comput. Sci. 144(1): 1- (2006) |
| 36 | EE | Amir Pnueli,
Ofer Strichman:
Reduced Functional Consistency of Uninterpreted Functions.
Electr. Notes Theor. Comput. Sci. 144(2): 53-65 (2006) |
| 35 | EE | Yoav Rodeh,
Ofer Strichman:
Building small equality graphs for deciding equality logic with uninterpreted functions.
Inf. Comput. 204(1): 26-59 (2006) |
| 34 | EE | Alex Groce,
Sagar Chaki,
Daniel Kroening,
Ofer Strichman:
Error explanation with distance metrics.
STTT 8(3): 229-247 (2006) |
| 2005 |
| 33 | EE | Anubhav Gupta,
Ofer Strichman:
Abstraction Refinement for Bounded Model Checking.
CAV 2005: 112-124 |
| 32 | EE | Orly Meir,
Ofer Strichman:
Yet Another Decision Procedure for Equality Logic.
CAV 2005: 307-320 |
| 31 | EE | Roman Gershman,
Ofer Strichman:
HaifaSat: A New Robust SAT Solver.
Haifa Verification Conference 2005: 76-89 |
| 30 | EE | Orna Grumberg,
Flavio Lerda,
Ofer Strichman,
Michael Theobald:
Proof-guided underapproximation-widening for multi-process systems.
POPL 2005: 122-131 |
| 29 | EE | Roman Gershman,
Ofer Strichman:
Cost-Effective Hyper-Resolution for Preprocessing CNF Formulas.
SAT 2005: 423-429 |
| 28 | EE | Armin Biere,
Ofer Strichman:
Preface.
Electr. Notes Theor. Comput. Sci. 119(2): 1- (2005) |
| 27 | EE | Edmund M. Clarke,
Daniel Kroening,
Joël Ouaknine,
Ofer Strichman:
Computational challenges in bounded model checking.
STTT 7(2): 174-183 (2005) |
| 26 | EE | Armin Biere,
Ofer Strichman:
Introductory paper.
STTT 7(2): 87-88 (2005) |
| 2004 |
| 25 | EE | Muralidhar Talupur,
Nishant Sinha,
Ofer Strichman,
Amir Pnueli:
Range Allocation for Separation Logic.
CAV 2004: 148-161 |
| 24 | EE | Daniel Kroening,
Joël Ouaknine,
Sanjit A. Seshia,
Ofer Strichman:
Abstraction-Based Satisfiability Solving of Presburger Arithmetic.
CAV 2004: 308-320 |
| 23 | EE | Sagar Chaki,
Alex Groce,
Ofer Strichman:
Explaining abstract counterexamples.
SIGSOFT FSE 2004: 73-82 |
| 22 | EE | Edmund M. Clarke,
Daniel Kroening,
Joël Ouaknine,
Ofer Strichman:
Completeness and Complexity of Bounded Model Checking.
VMCAI 2004: 85-96 |
| 21 | EE | Ofer Strichman:
Deciding Disjunctive Linear Arithmetic with SAT
CoRR cs.LO/0402002: (2004) |
| 20 | EE | Ofer Strichman:
Accelerating Bounded Model Checking of Safety Properties.
Formal Methods in System Design 24(1): 5-24 (2004) |
| 19 | EE | Sagar Chaki,
Edmund M. Clarke,
Alex Groce,
Joël Ouaknine,
Ofer Strichman,
Karen Yorav:
Efficient Verification of Sequential and Concurrent C Programs.
Formal Methods in System Design 25(2-3): 129-166 (2004) |
| 18 | EE | Edmund M. Clarke,
Anubhav Gupta,
Ofer Strichman:
SAT-based counterexample-guided abstraction refinement.
IEEE Trans. on CAD of Integrated Circuits and Systems 23(7): 1113-1123 (2004) |
| 2003 |
| 17 | EE | Sagar Chaki,
Edmund M. Clarke,
Alex Groce,
Ofer Strichman:
Predicate Abstraction with Minimum Predicates.
CHARME 2003: 19-34 |
| 16 | EE | Daniel Kroening,
Ofer Strichman:
Efficient Computation of Recurrence Diameters.
VMCAI 2003: 298-309 |
| 15 | | Armin Biere,
Alessandro Cimatti,
Edmund M. Clarke,
Ofer Strichman,
Yunshan Zhu:
Bounded model checking.
Advances in Computers 58: 118-149 (2003) |
| 14 | EE | 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): 227 (2003) |
| 2002 |
| 13 | EE | Ofer Strichman,
Sanjit A. Seshia,
Randal E. Bryant:
Deciding Separation Formulas with SAT.
CAV 2002: 209-222 |
| 12 | EE | Edmund M. Clarke,
Anubhav Gupta,
James H. Kukula,
Ofer Strichman:
SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques.
CAV 2002: 265-279 |
| 11 | EE | Ofer Strichman:
On Solving Presburger and Linear Arithmetic with SAT.
FMCAD 2002: 160-170 |
| 10 | EE | Amir Pnueli,
Yoav Rodeh,
Ofer Strichman,
Michael Siegel:
The Small Model Property: How Small Can It Be?
Inf. Comput. 178(1): 279-293 (2002) |
| 2001 |
| 9 | EE | Yoav Rodeh,
Ofer Strichman:
Finite Instantiations in Equivalence Logic with Uninterpreted Functions.
CAV 2001: 144-154 |
| 8 | EE | Ofer Strichman:
Pruning Techniques for the SAT-Based Bounded Model Checking Problem.
CHARME 2001: 58-70 |
| 7 | EE | Amir Pnueli,
Yoav Rodeh,
Ofer Strichman:
Range Allocation for Equivalence Logic.
FSTTCS 2001: 317-333 |
| 2000 |
| 6 | | Ofer Strichman:
Tuning SAT Checkers for Bounded Model Checking.
CAV 2000: 480-494 |
| 1999 |
| 5 | EE | Amir Pnueli,
Yoav Rodeh,
Ofer Strichman,
Michael Siegel:
Deciding Equality Formulas by Small Domains Instantiations.
CAV 1999: 455-469 |
| 4 | EE | Amir Pnueli,
Ofer Strichman,
Michael Siegel:
Translation Validation: From SIGNAL to C.
Correct System Design 1999: 231-255 |
| 1998 |
| 3 | | Amir Pnueli,
Ofer Strichman,
Michael Siegel:
Translation Validation: From DC+ to C*.
FM-Trends 1998: 137-150 |
| 2 | EE | Amir Pnueli,
Ofer Strichman,
Michael Siegel:
Translation Validation for Synchronous Languages.
ICALP 1998: 235-246 |
| 1 | EE | Amir Pnueli,
Ofer Strichman,
Michael Siegel:
The Code Validation Tool CVT: Automatic Verification of a Compilation Process.
STTT 2(2): 192-201 (1998) |