| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Sagar Chaki, Arie Gurfinkel, Ofer Strichman |
Regression Verification for Multi-threaded Programs.  |
VMCAI  |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Laurent Fournier, Avi Ziv, Ekaterina Kutsy, Ofer Strichman |
A probabilistic analysis of coverage methods. |
ACM Trans. Design Autom. Electr. Syst. |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Omer Bar-Ilan, Oded Fuhrmann, Shlomo Hoory, Ohad Shacham, Ofer Strichman |
Reducing the size of resolution proofs in linear time. |
STTT |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Vadim Ryvchin, Ofer Strichman |
Faster Extraction of High-Level Minimal Unsatisfiable Cores. |
SAT |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Kroening, Joël Ouaknine, Ofer Strichman, Thomas Wahl, James Worrell |
Linear Completeness Thresholds for Bounded Model Checking. |
CAV |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Arie Matsliah, Ofer Strichman |
Underapproximation for model-checking based on universal circuits. |
Inf. Comput. |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Ofer Strichman, Stefan Szeider (eds.) |
Theory and Applications of Satisfiability Testing - SAT 2010, 13th International Conference, SAT 2010, Edinburgh, UK, July 11-14, 2010. Proceedings |
SAT |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Benny Godlin, Ofer Strichman |
Inference Rules for Proving the Equivalence of Recursive Procedures. |
Essays in Memory of Amir Pnueli |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Hana Chockler, Arie Gurfinkel, Ofer Strichman |
Variants of LTL Query Checking. |
Haifa Verification Conference |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael Veksler, Ofer Strichman |
A Proof-Producing CSP Solver. |
AAAI |
2010 |
DBLP BibTeX RDF |
|
| 1 | Daniel Kroening, Ofer Strichman |
A framework for Satisfiability Modulo Theories. |
Formal Asp. Comput. |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Roman Gershman, Ofer Strichman |
HaifaSat: a SAT solver based on an Abstraction/Refinement model. |
JSAT |
2009 |
DBLP BibTeX RDF |
|
| 1 | 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. |
STTT |
2009 |
DBLP DOI BibTeX RDF |
Decision-procedures, Bit-vector |
| 1 | Hana Chockler, Ofer Strichman |
Before and after vacuity. |
Formal Methods in System Design |
2009 |
DBLP DOI BibTeX RDF |
Vacuity, Model-checking, Complexity |
| 1 | Sagar Chaki, Arie Gurfinkel, Ofer Strichman |
Decision diagrams for linear arithmetic. |
FMCAD |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Benny Godlin, Ofer Strichman |
Regression verification. |
DAC |
2009 |
DBLP DOI BibTeX RDF |
software verification, equivalence checking |
| 1 | Michael Ryabtsev, Ofer Strichman |
Translation Validation: From Simulink to C. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Ofer Strichman |
Regression Verification: Proving the Equivalence of Similar Programs. |
CAV |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Benny Godlin, Ofer Strichman |
Inference rules for proving the equivalence of recursive procedures. |
Acta Inf. |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Mirron Rozanov, Ofer Strichman |
Generating Minimum Transitivity Constraints in P-time for Deciding Equality Logic. |
Electr. Notes Theor. Comput. Sci. |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Roman Gershman, Maya Koifman, Ofer Strichman |
An approach for extracting a small unsatisfiable core. |
Formal Methods in System Design |
2008 |
DBLP DOI BibTeX RDF |
Unsatisfiable core, SAT, Resolution |
| 1 | Sagar Chaki, Ofer Strichman |
Three optimizations for Assume-Guarantee reasoning with L*. |
Formal Methods in System Design |
2008 |
DBLP DOI BibTeX RDF |
Learning, Software verification, Compositionality, Assume-Guarantee |
| 1 | Dan Goldwasser, Ofer Strichman, Shai Fine |
A Theory-Based Decision Heuristic for DPLL(T). |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Hana Chockler, Arie Gurfinkel, Ofer Strichman |
Beyond Vacuity: Towards the Strongest Passing Formula. |
FMCAD |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Vadim Ryvchin, Ofer Strichman |
Local Restarts. |
SAT |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Omer Bar-Ilan, Oded Fuhrmann, Shlomo Hoory, Ohad Shacham, Ofer Strichman |
Linear-Time Reductions of Resolution Proofs. |
Haifa Verification Conference |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Ofer Strichman, Armin Biere |
Preface. |
Electr. Notes Theor. Comput. Sci. |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Hana Chockler, Ofer Strichman |
Easier and More Informative Vacuity Checks. |
MEMOCODE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady |
Deciding Bit-Vector Arithmetic with Abstraction. |
TACAS |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Sagar Chaki, Ofer Strichman |
Optimized L*-Based Assume-Guarantee Reasoning. |
TACAS |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Arie Matsliah, Ofer Strichman |
Underapproximation for Model-Checking Based on Random Cryptographic Constructions. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Yoav Rodeh, Ofer Strichman |
Building small equality graphs for deciding equality logic with uninterpreted functions. |
Inf. Comput. |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli, Ofer Strichman |
Reduced Functional Consistency of Uninterpreted Functions. |
Electr. Notes Theor. Comput. Sci. |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Armin Biere, Ofer Strichman |
Preface. |
Electr. Notes Theor. Comput. Sci. |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Alex Groce, Sagar Chaki, Daniel Kroening, Ofer Strichman |
Error explanation with distance metrics. |
STTT |
2006 |
DBLP DOI BibTeX RDF |
Error explanation, Model checking, Fault localization, Automated debugging |
| 1 | Roman Gershman, Maya Koifman, Ofer Strichman |
Deriving Small Unsatisfiable Cores with Dominators. |
CAV |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Armin Biere, Ofer Strichman |
Preface. |
Electr. Notes Theor. Comput. Sci. |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Armin Biere, Ofer Strichman |
Introductory paper. |
STTT |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman |
Computational challenges in bounded model checking. |
STTT |
2005 |
DBLP DOI BibTeX RDF |
Bonded-Model-checking, Completeness-Threshold, Complexity |
| 1 | Roman Gershman, Ofer Strichman |
Cost-Effective Hyper-Resolution for Preprocessing CNF Formulas. |
SAT |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Orna Grumberg, Flavio Lerda, Ofer Strichman, Michael Theobald |
Proof-guided underapproximation-widening for multi-process systems. |
POPL |
2005 |
DBLP DOI BibTeX RDF |
SAT proofs, underapproximation-widening, abstraction, software verification, bounded model checking |
| 1 | Ofer Strichman, Benny Godlin |
Regression Verification - A Practical Way to Verify Programs. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Orly Meir, Ofer Strichman |
Yet Another Decision Procedure for Equality Logic. |
CAV |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Anubhav Gupta, Ofer Strichman |
Abstraction Refinement for Bounded Model Checking. |
CAV |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Roman Gershman, Ofer Strichman |
HaifaSat: A New Robust SAT Solver. |
Haifa Verification Conference |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Edmund M. Clarke, Anubhav Gupta, Ofer Strichman |
SAT-based counterexample-guided abstraction refinement. |
IEEE Trans. on CAD of Integrated Circuits and Systems |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Ofer Strichman |
Deciding Disjunctive Linear Arithmetic with SAT |
CoRR |
2004 |
DBLP BibTeX RDF |
|
| 1 | 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 |
2004 |
DBLP DOI BibTeX RDF |
concurrency, process algebra, software verification, predicate abstraction, abstraction refinement |
| 1 | Ofer Strichman |
Accelerating Bounded Model Checking of Safety Properties. |
Formal Methods in System Design |
2004 |
DBLP DOI BibTeX RDF |
SAT, Bounded Model Checking |
| 1 | Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman |
Abstraction-Based Satisfiability Solving of Presburger Arithmetic. |
CAV |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Muralidhar Talupur, Nishant Sinha, Ofer Strichman, Amir Pnueli |
Range Allocation for Separation Logic. |
CAV |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman |
Completeness and Complexity of Bounded Model Checking. |
VMCAI |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Sagar Chaki, Alex Groce, Ofer Strichman |
Explaining abstract counterexamples. |
SIGSOFT FSE |
2004 |
DBLP DOI BibTeX RDF |
model checking, fault localization, predicate abstraction |
| 1 | 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. |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Ofer Strichman, Armin Biere |
Preface. |
Electr. Notes Theor. Comput. Sci. |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, Yunshan Zhu |
Bounded model checking. |
Advances in Computers |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Sagar Chaki, Edmund M. Clarke, Alex Groce, Ofer Strichman |
Predicate Abstraction with Minimum Predicates. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Kroening, Ofer Strichman |
Efficient Computation of Recurrence Diameters. |
VMCAI |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel |
The Small Model Property: How Small Can It Be? |
Inf. Comput. |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Ofer Strichman |
On Solving Presburger and Linear Arithmetic with SAT. |
FMCAD |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Ofer Strichman, Sanjit A. Seshia, Randal E. Bryant |
Deciding Separation Formulas with SAT. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Edmund M. Clarke, Anubhav Gupta, James H. Kukula, Ofer Strichman |
SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Ofer Strichman |
Pruning Techniques for the SAT-Based Bounded Model Checking Problem. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Yoav Rodeh, Ofer Strichman |
Finite Instantiations in Equivalence Logic with Uninterpreted Functions. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli, Yoav Rodeh, Ofer Strichman |
Range Allocation for Equivalence Logic. |
FSTTCS |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Ofer Strichman |
Tuning SAT Checkers for Bounded Model Checking. |
CAV |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli, Ofer Strichman, Michael Siegel |
Translation Validation: From SIGNAL to C. |
Correct System Design |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel |
Deciding Equality Formulas by Small Domains Instantiations. |
CAV |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli, Ofer Strichman, Michael Siegel |
The Code Validation Tool CVT: Automatic Verification of a Compilation Process. |
STTT |
1998 |
DBLP DOI BibTeX RDF |
Code validation, BDD, Industrial application, Compiler verification, Translation validation |
| 1 | Amir Pnueli, Ofer Strichman, Michael Siegel |
Translation Validation for Synchronous Languages. |
ICALP |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli, Ofer Strichman, Michael Siegel |
Translation Validation: From DC+ to C*. |
FM-Trends |
1998 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")