|
Search the dblp DataBase
Ofer Strichman:
[Publications]
[Author Rank by year]
[Co-authors]
[Prefers]
[Cites]
[Cited by]
Publications of Author
- Amir Pnueli, Ofer Strichman, Michael Siegel
Translation Validation: From SIGNAL to C. [Citation Graph (0, 0)][DBLP] Correct System Design, 1999, pp:231-255 [Conf]
- Edmund M. Clarke, Anubhav Gupta, James H. Kukula, Ofer Strichman
SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques. [Citation Graph (0, 0)][DBLP] CAV, 2002, pp:265-279 [Conf]
- Roman Gershman, Maya Koifman, Ofer Strichman
Deriving Small Unsatisfiable Cores with Dominators. [Citation Graph (0, 0)][DBLP] CAV, 2006, pp:109-122 [Conf]
- Anubhav Gupta, Ofer Strichman
Abstraction Refinement for Bounded Model Checking. [Citation Graph (0, 0)][DBLP] CAV, 2005, pp:112-124 [Conf]
- Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman
Abstraction-Based Satisfiability Solving of Presburger Arithmetic. [Citation Graph (0, 0)][DBLP] CAV, 2004, pp:308-320 [Conf]
- Orly Meir, Ofer Strichman
Yet Another Decision Procedure for Equality Logic. [Citation Graph (0, 0)][DBLP] CAV, 2005, pp:307-320 [Conf]
- Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel
Deciding Equality Formulas by Small Domains Instantiations. [Citation Graph (0, 0)][DBLP] CAV, 1999, pp:455-469 [Conf]
- Yoav Rodeh, Ofer Strichman
Finite Instantiations in Equivalence Logic with Uninterpreted Functions. [Citation Graph (0, 0)][DBLP] CAV, 2001, pp:144-154 [Conf]
- Ofer Strichman
Tuning SAT Checkers for Bounded Model Checking. [Citation Graph (0, 0)][DBLP] CAV, 2000, pp:480-494 [Conf]
- Ofer Strichman, Sanjit A. Seshia, Randal E. Bryant
Deciding Separation Formulas with SAT. [Citation Graph (0, 0)][DBLP] CAV, 2002, pp:209-222 [Conf]
- Muralidhar Talupur, Nishant Sinha, Ofer Strichman, Amir Pnueli
Range Allocation for Separation Logic. [Citation Graph (0, 0)][DBLP] CAV, 2004, pp:148-161 [Conf]
- Sagar Chaki, Edmund M. Clarke, Alex Groce, Ofer Strichman
Predicate Abstraction with Minimum Predicates. [Citation Graph (0, 0)][DBLP] CHARME, 2003, pp:19-34 [Conf]
- Ofer Strichman
Pruning Techniques for the SAT-Based Bounded Model Checking Problem. [Citation Graph (0, 0)][DBLP] CHARME, 2001, pp:58-70 [Conf]
- Amir Pnueli, Ofer Strichman, Michael Siegel
Translation Validation: From DC+ to C*. [Citation Graph (0, 0)][DBLP] FM-Trends, 1998, pp:137-150 [Conf]
- Ofer Strichman
On Solving Presburger and Linear Arithmetic with SAT. [Citation Graph (0, 0)][DBLP] FMCAD, 2002, pp:160-170 [Conf]
- Amir Pnueli, Yoav Rodeh, Ofer Strichman
Range Allocation for Equivalence Logic. [Citation Graph (0, 0)][DBLP] FSTTCS, 2001, pp:317-333 [Conf]
- Roman Gershman, Ofer Strichman
HaifaSat: A New Robust SAT Solver. [Citation Graph (0, 0)][DBLP] Haifa Verification Conference, 2005, pp:76-89 [Conf]
- Amir Pnueli, Ofer Strichman, Michael Siegel
Translation Validation for Synchronous Languages. [Citation Graph (0, 0)][DBLP] ICALP, 1998, pp:235-246 [Conf]
- Orna Grumberg, Flavio Lerda, Ofer Strichman, Michael Theobald
Proof-guided underapproximation-widening for multi-process systems. [Citation Graph (0, 0)][DBLP] POPL, 2005, pp:122-131 [Conf]
- Roman Gershman, Ofer Strichman
Cost-Effective Hyper-Resolution for Preprocessing CNF Formulas. [Citation Graph (0, 0)][DBLP] SAT, 2005, pp:423-429 [Conf]
- Sagar Chaki, Alex Groce, Ofer Strichman
Explaining abstract counterexamples. [Citation Graph (0, 0)][DBLP] SIGSOFT FSE, 2004, pp:73-82 [Conf]
- Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman
Completeness and Complexity of Bounded Model Checking. [Citation Graph (0, 0)][DBLP] VMCAI, 2004, pp:85-96 [Conf]
- Daniel Kroening, Ofer Strichman
Efficient Computation of Recurrence Diameters. [Citation Graph (0, 0)][DBLP] VMCAI, 2003, pp:298-309 [Conf]
- Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, Yunshan Zhu
Bounded model checking. [Citation Graph (0, 0)][DBLP] Advances in Computers, 2003, v:58, n:, pp:118-149 [Journal]
- Ofer Strichman
Deciding Disjunctive Linear Arithmetic with SAT [Citation Graph (0, 0)][DBLP] CoRR, 2004, v:0, n:, pp:- [Journal]
- Armin Biere, Ofer Strichman
Preface. [Citation Graph (0, 0)][DBLP] Electr. Notes Theor. Comput. Sci., 2005, v:119, n:2, pp:1-0 [Journal]
- Armin Biere, Ofer Strichman
Preface. [Citation Graph (0, 0)][DBLP] Electr. Notes Theor. Comput. Sci., 2006, v:144, n:1, pp:1-0 [Journal]
- Amir Pnueli, Ofer Strichman
Reduced Functional Consistency of Uninterpreted Functions. [Citation Graph (0, 0)][DBLP] Electr. Notes Theor. Comput. Sci., 2006, v:144, n:2, pp:53-65 [Journal]
- Ofer Strichman, Armin Biere
Preface. [Citation Graph (0, 0)][DBLP] Electr. Notes Theor. Comput. Sci., 2007, v:174, n:3, pp:1-2 [Journal]
- Sagar Chaki, Edmund M. Clarke, Alex Groce, Joël Ouaknine, Ofer Strichman, Karen Yorav
Efficient Verification of Sequential and Concurrent C Programs. [Citation Graph (0, 0)][DBLP] Formal Methods in System Design, 2004, v:25, n:2-3, pp:129-166 [Journal]
- Ofer Strichman
Accelerating Bounded Model Checking of Safety Properties. [Citation Graph (0, 0)][DBLP] Formal Methods in System Design, 2004, v:24, n:1, pp:5-24 [Journal]
- 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). [Citation Graph (0, 0)][DBLP] Inf. Comput., 2003, v:184, n:1, pp:227- [Journal]
- Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel
The Small Model Property: How Small Can It Be? [Citation Graph (0, 0)][DBLP] Inf. Comput., 2002, v:178, n:1, pp:279-293 [Journal]
- Yoav Rodeh, Ofer Strichman
Building small equality graphs for deciding equality logic with uninterpreted functions. [Citation Graph (0, 0)][DBLP] Inf. Comput., 2006, v:204, n:1, pp:26-59 [Journal]
- Armin Biere, Ofer Strichman
Introductory paper. [Citation Graph (0, 0)][DBLP] STTT, 2005, v:7, n:2, pp:87-88 [Journal]
- Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman
Computational challenges in bounded model checking. [Citation Graph (0, 0)][DBLP] STTT, 2005, v:7, n:2, pp:174-183 [Journal]
- Amir Pnueli, Ofer Strichman, Michael Siegel
The Code Validation Tool CVT: Automatic Verification of a Compilation Process. [Citation Graph (0, 0)][DBLP] STTT, 1998, v:2, n:2, pp:192-201 [Journal]
- Alex Groce, Sagar Chaki, Daniel Kroening, Ofer Strichman
Error explanation with distance metrics. [Citation Graph (0, 0)][DBLP] STTT, 2006, v:8, n:3, pp:229-247 [Journal]
- Edmund M. Clarke, Anubhav Gupta, Ofer Strichman
SAT-based counterexample-guided abstraction refinement. [Citation Graph (0, 0)][DBLP] IEEE Trans. on CAD of Integrated Circuits and Systems, 2004, v:23, n:7, pp:1113-1123 [Journal]
- Arie Matsliah, Ofer Strichman
Underapproximation for Model-Checking Based on Random Cryptographic Constructions. [Citation Graph (0, 0)][DBLP] CAV, 2007, pp:339-351 [Conf]
- Hana Chockler, Ofer Strichman
Easier and More Informative Vacuity Checks. [Citation Graph (0, 0)][DBLP] MEMOCODE, 2007, pp:189-198 [Conf]
- Sagar Chaki, Ofer Strichman
Optimized L*-Based Assume-Guarantee Reasoning. [Citation Graph (0, 0)][DBLP] TACAS, 2007, pp:276-291 [Conf]
- Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady
Deciding Bit-Vector Arithmetic with Abstraction. [Citation Graph (0, 0)][DBLP] TACAS, 2007, pp:358-372 [Conf]
A Proof-Producing CSP Solver. [Citation Graph (, )][DBLP]
Inference Rules for Proving the Equivalence of Recursive Procedures. [Citation Graph (, )][DBLP]
Regression Verification: Proving the Equivalence of Similar Programs. [Citation Graph (, )][DBLP]
Translation Validation: From Simulink to C. [Citation Graph (, )][DBLP]
Regression verification. [Citation Graph (, )][DBLP]
Beyond Vacuity: Towards the Strongest Passing Formula. [Citation Graph (, )][DBLP]
A Theory-Based Decision Heuristic for DPLL(T). [Citation Graph (, )][DBLP]
Decision diagrams for linear arithmetic. [Citation Graph (, )][DBLP]
Linear-Time Reductions of Resolution Proofs. [Citation Graph (, )][DBLP]
Local Restarts. [Citation Graph (, )][DBLP]
Regression Verification - A Practical Way to Verify Programs. [Citation Graph (, )][DBLP]
Inference rules for proving the equivalence of recursive procedures. [Citation Graph (, )][DBLP]
Generating Minimum Transitivity Constraints in P-time for Deciding Equality Logic. [Citation Graph (, )][DBLP]
Search in 0.008secs, Finished in 0.011secs
|