# Ofer Strichman

According to our database

^{1}, Ofer Strichman## Timeline

#### Legend:

Book In proceedings Article PhD thesis Other## Links

#### Homepages:

#### On csauthors.net:

## Bibliography

2018

Special issue: program equivalence.

Formal Methods in System Design, 2018

2017

Near-Optimal Course Scheduling at the Technion.

Interfaces, 2017

The impact of Entropy and Solution Density on selected SAT heuristics.

CoRR, 2017

Synthesizing Non-Vacuous Systems.

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2017

Decision-Making with Cross-Entropy for Self-Adaptation.

Proceedings of the 12th IEEE/ACM International Symposium on Software Engineering for Adaptive and Self-Managing Systems, 2017

2016

Decision Procedures - An Algorithmic Point of View, Second Edition

Texts in Theoretical Computer Science. An EATCS Series, Springer, ISBN: 978-3-662-50497-0, 2016

Learning general constraints in CSP.

Artif. Intell., 2016

Minimal unsatisfiable core extraction for SMT.

Proceedings of the 2016 Formal Methods in Computer-Aided Design, 2016

Regression Verification for Unbalanced Recursive Functions.

Proceedings of the FM 2016: Formal Methods, 2016

Cyclic Routing of Unmanned Aerial Vehicles.

Proceedings of the Integration of AI and OR Techniques in Constraint Programming, 2016

2015

Model Counting of Monotone Conjunctive Normal Form Formulas with Spectra.

INFORMS Journal on Computing, 2015

Proving mutual termination.

Formal Methods in System Design, 2015

Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation).

Formal Methods in System Design, 2015

Mining Backbone Literals in Incremental SAT - A New Kind of Incremental Data.

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2015, 2015

Learning General Constraints in CSP.

Proceedings of the Integration of AI and OR Techniques in Constraint Programming, 2015

Learning the Language of Error.

Proceedings of the Automated Technology for Verification and Analysis, 2015

2014

Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores.

JSAT, 2014

Ultimately Incremental SAT.

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2014, 2014

2013

Regression verification: proving the equivalence of similar programs.

Softw. Test., Verif. Reliab., 2013

Preface to the special issue "SI: Satisfiability Modulo Theories".

Formal Methods in System Design, 2013

Beyond vacuity: towards the strongest passing formula.

Formal Methods in System Design, 2013

Compositional Sequentialization of Periodic Programs.

Proceedings of the Verification, 2013

A New Class of Lineage Expressions over Probabilistic Databases Computable in P-Time.

Proceedings of the Scalable Uncertainty Management - 7th International Conference, 2013

Efficient MUS extraction with resolution.

Proceedings of the Formal Methods in Computer-Aided Design, 2013

Verifying periodic programs with priority inheritance locks.

Proceedings of the Formal Methods in Computer-Aided Design, 2013

2012

Regression Verification for Multi-threaded Programs.

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2012

Preprocessing in Incremental SAT.

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2012, 2012

Proving Mutual Termination of Programs.

Proceedings of the Hardware and Software: Verification and Testing, 2012

2011

A probabilistic analysis of coverage methods.

ACM Trans. Design Autom. Electr. Syst., 2011

Reducing the size of resolution proofs in linear time.

STTT, 2011

Faster Extraction of High-Level Minimal Unsatisfiable Cores.

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2011, 2011

Time-bounded analysis of real-time systems.

Proceedings of the International Conference on Formal Methods in Computer-Aided Design, 2011

Linear Completeness Thresholds for Bounded Model Checking.

Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

2010

Underapproximation for model-checking based on universal circuits.

Inf. Comput., 2010

Variants of LTL Query Checking.

Proceedings of the Hardware and Software: Verification and Testing, 2010

Inference Rules for Proving the Equivalence of Recursive Procedures.

Proceedings of the Time for Verification, 2010

A Proof-Producing CSP Solver.

Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence, 2010

2009

An abstraction-based decision procedure for bit-vector arithmetic.

STTT, 2009

HaifaSat: a SAT solver based on an Abstraction/Refinement model.

JSAT, 2009

Before and after vacuity.

Formal Methods in System Design, 2009

A framework for Satisfiability Modulo Theories.

Formal Asp. Comput., 2009

Decision diagrams for linear arithmetic.

Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, 2009

Regression verification.

Proceedings of the 46th Design Automation Conference, 2009

Regression Verification: Proving the Equivalence of Similar Programs.

Proceedings of the Computer Aided Verification, 21st International Conference, 2009

Translation Validation: From Simulink to C.

Proceedings of the Computer Aided Verification, 21st International Conference, 2009

2008

Decision Procedures - An Algorithmic Point of View

Texts in Theoretical Computer Science. An EATCS Series, Springer, ISBN: 978-3-540-74105-3, 2008

An approach for extracting a small unsatisfiable core.

Formal Methods in System Design, 2008

Three optimizations for Assume-Guarantee reasoning with L

^{*}.
Formal Methods in System Design, 2008

Generating Minimum Transitivity Constraints in P-time for Deciding Equality Logic.

Electr. Notes Theor. Comput. Sci., 2008

Inference rules for proving the equivalence of recursive procedures.

Acta Inf., 2008

Local Restarts.

Proceedings of the Theory and Applications of Satisfiability Testing, 2008

Linear-Time Reductions of Resolution Proofs.

Proceedings of the Hardware and Software: Verification and Testing, 2008

A Theory-Based Decision Heuristic for DPLL(T).

Proceedings of the Formal Methods in Computer-Aided Design, 2008

Beyond Vacuity: Towards the Strongest Passing Formula.

Proceedings of the Formal Methods in Computer-Aided Design, 2008

2007

Preface.

Electr. Notes Theor. Comput. Sci., 2007

Optimized L*-Based Assume-Guarantee Reasoning.

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Deciding Bit-Vector Arithmetic with Abstraction.

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Easier and More Informative Vacuity Checks.

Proceedings of the 5th ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2007), May 30, 2007

Underapproximation for Model-Checking Based on Random Cryptographic Constructions.

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2006

Error explanation with distance metrics.

STTT, 2006

Building small equality graphs for deciding equality logic with uninterpreted functions.

Inf. Comput., 2006

Reduced Functional Consistency of Uninterpreted Functions.

Electr. Notes Theor. Comput. Sci., 2006

Preface.

Electr. Notes Theor. Comput. Sci., 2006

Deriving Small Unsatisfiable Cores with Dominators.

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

2005

Computational challenges in bounded model checking.

STTT, 2005

Introductory paper.

STTT, 2005

Preface.

Electr. Notes Theor. Comput. Sci., 2005

Regression Verification - A Practical Way to Verify Programs.

Proceedings of the Verified Software: Theories, 2005

Cost-Effective Hyper-Resolution for Preprocessing CNF Formulas.

Proceedings of the Theory and Applications of Satisfiability Testing, 2005

Proof-guided underapproximation-widening for multi-process systems.

Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2005

HaifaSat: A New Robust SAT Solver.

Proceedings of the Hardware and Software Verification and Testing, 2005

Yet Another Decision Procedure for Equality Logic.

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

Abstraction Refinement for Bounded Model Checking.

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

2004

SAT-based counterexample-guided abstraction refinement.

IEEE Trans. on CAD of Integrated Circuits and Systems, 2004

Accelerating Bounded Model Checking of Safety Properties.

Formal Methods in System Design, 2004

Efficient Verification of Sequential and Concurrent C Programs.

Formal Methods in System Design, 2004

Deciding Disjunctive Linear Arithmetic with SAT

CoRR, 2004

Completeness and Complexity of Bounded Model Checking.

Proceedings of the Verification, 2004

Explaining abstract counterexamples.

Proceedings of the 12th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2004, Newport Beach, CA, USA, October 31, 2004

Range Allocation for Separation Logic.

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

Abstraction-Based Satisfiability Solving of Presburger Arithmetic.

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

2003

Erratum ("The small model property: how small can it be?" Volume 178, Number 1 [2002], pages 279-293).

Inf. Comput., 2003

Preface.

Electr. Notes Theor. Comput. Sci., 2003

Bounded model checking.

Advances in Computers, 2003

Efficient Computation of Recurrence Diameters.

Proceedings of the Verification, 2003

Predicate Abstraction with Minimum Predicates.

Proceedings of the Correct Hardware Design and Verification Methods, 2003

2002

The Small Model Property: How Small Can It Be?

Inf. Comput., 2002

On Solving Presburger and Linear Arithmetic with SAT.

Proceedings of the Formal Methods in Computer-Aided Design, 4th International Conference, 2002

Deciding Separation Formulas with SAT.

Proceedings of the Computer Aided Verification, 14th International Conference, 2002

SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques.

Proceedings of the Computer Aided Verification, 14th International Conference, 2002

2001

Using Simulation to Increase Efficiency in an Army Recruitment Office.

Interfaces, 2001

Range Allocation for Equivalence Logic.

Proceedings of the FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science, 2001

Pruning Techniques for the SAT-Based Bounded Model Checking Problem.

Proceedings of the Correct Hardware Design and Verification Methods, 2001

Finite Instantiations in Equivalence Logic with Uninterpreted Functions.

Proceedings of the Computer Aided Verification, 13th International Conference, 2001

2000

Tuning SAT Checkers for Bounded Model Checking.

Proceedings of the Computer Aided Verification, 12th International Conference, 2000

1999

Deciding Equality Formulas by Small Domains Instantiations.

Proceedings of the Computer Aided Verification, 11th International Conference, 1999

Translation Validation: From SIGNAL to C.

Proceedings of the Correct System Design, 1999

1998

The Code Validation Tool CVT: Automatic Verification of a Compilation Process.

STTT, 1998

Translation Validation for Synchronous Languages.

Proceedings of the Automata, Languages and Programming, 25th International Colloquium, 1998

Translation Validation: From DC+ to C*.

Proceedings of the Applied Formal Methods, 1998