Ofer Strichman

CoRR, 2022

Automated Repair of Neural Networks.

[BibT_eX]

[DOI]

Dor Cohen

CoRR, 2022

Combining BMC and Complementary Approximate Reachability to Accelerate Bug-Finding.

[BibT_eX]

[DOI]

Proceedings of the 41st IEEE/ACM International Conference on Computer-Aided Design, 2022

2021

Vacuity in synthesis.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2021

Exploiting Isomorphic Subgraphs in SAT (Long version).

[BibT_eX]

[DOI]

Alexander Ivrii

CoRR, 2021

Real-time solving of computationally hard problems using optimal algorithm portfolios.

[BibT_eX]

[DOI]

Yair Nof

Ann. Math. Artif. Intell., 2021

Exploiting Isomorphic Subgraphs in SAT.

[BibT_eX]

[DOI]

Alexander Ivrii

Proceedings of the Formal Methods in Computer Aided Design, 2021

2020

Learning the Language of Software Errors.

[BibT_eX]

[DOI]

J. Artif. Intell. Res., 2020

A combination of 'pooling' with a prediction model can reduce by 73% the number of COVID-19 (Corona-virus) tests.

[BibT_eX]

[DOI]

CoRR, 2020

2019

Cyclic-routing of Unmanned Aerial Vehicles.

[BibT_eX]

[DOI]

J. Comput. Syst. Sci., 2019

Synthesizing Reactive Systems Using Robustness and Recovery Specifications.

[BibT_eX]

[DOI]

Proceedings of the 2019 Formal Methods in Computer Aided Design, 2019

2018

Special issue: program equivalence.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2018

The Impact of Entropy and Solution Density on Selected SAT Heuristics.

[BibT_eX]

[DOI]

Dor Cohen

Entropy, 2018

Program Equivalence (Dagstuhl Seminar 18151).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2018

2017

Near-Optimal Course Scheduling at the Technion.

[BibT_eX]

[DOI]

Interfaces, 2017

Synthesizing Non-Vacuous Systems.

[BibT_eX]

[DOI]

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

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

[BibT_eX]

[DOI]

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

[BibT_eX]

[DOI]

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

Learning general constraints in CSP.

[BibT_eX]

[DOI]

Michael Veksler

Artif. Intell., 2016

Minimal unsatisfiable core extraction for SMT.

[BibT_eX]

[DOI]

Ofer Guthmann

Anna Trostanetski

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

Regression Verification for Unbalanced Recursive Functions.

[BibT_eX]

[DOI]

Maor Veitsman

Proceedings of the FM 2016: Formal Methods, 2016

Cyclic Routing of Unmanned Aerial Vehicles.

[BibT_eX]

[DOI]

Nir Drucker

Michal Penn

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

2015

Model Counting of Monotone Conjunctive Normal Form Formulas with Spectra.

[BibT_eX]

[DOI]

Radislav Vaisman

Ilya B. Gertsbakh

INFORMS J. Comput., 2015

Proving mutual termination.

[BibT_eX]

[DOI]

Dima Elenbogen

Shmuel Katz

Formal Methods Syst. Des., 2015

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

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2015

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

[BibT_eX]

[DOI]

Alexander Ivrii

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

Learning the Language of Error.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2015

2014

Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2014

Ultimately Incremental SAT.

[BibT_eX]

[DOI]

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

2013

Regression verification: proving the equivalence of similar programs.

[BibT_eX]

[DOI]

Softw. Test. Verification Reliab., 2013

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

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2013

Beyond vacuity: towards the strongest passing formula.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2013

Compositional Sequentialization of Periodic Programs.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2013

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

[BibT_eX]

[DOI]

Batya Kenig

Avigdor Gal

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

Efficient MUS extraction with resolution.

[BibT_eX]

[DOI]

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

Verifying periodic programs with priority inheritance locks.

[BibT_eX]

[DOI]

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

2012

Regression Verification for Multi-threaded Programs.

[BibT_eX]

[DOI]

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

Preprocessing in Incremental SAT.

[BibT_eX]

[DOI]

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

Proving Mutual Termination of Programs.

[BibT_eX]

[DOI]

Dima Elenbogen

Shmuel Katz

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

2011

A probabilistic analysis of coverage methods.

[BibT_eX]

[DOI]

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

Reducing the size of resolution proofs in linear time.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2011

Faster Extraction of High-Level Minimal Unsatisfiable Cores.

[BibT_eX]

[DOI]

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

Time-bounded analysis of real-time systems.

[BibT_eX]

[DOI]

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

Linear Completeness Thresholds for Bounded Model Checking.

[BibT_eX]

[DOI]

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

2010

Underapproximation for model-checking based on universal circuits.

[BibT_eX]

[DOI]

Arie Matsliah

Inf. Comput., 2010

Variants of LTL Query Checking.

[BibT_eX]

[DOI]

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

A Proof-Producing CSP Solver.

[BibT_eX]

[DOI]

Michael Veksler

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

2009

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

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2009

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

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2009

Before and after vacuity.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2009

A framework for Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2009

Decision diagrams for linear arithmetic.

[BibT_eX]

[DOI]

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

Regression verification.

[BibT_eX]

[DOI]

Proceedings of the 46th Design Automation Conference, 2009

Regression Verification: Proving the Equivalence of Similar Programs.

[BibT_eX]

[DOI]

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

Translation Validation: From Simulink to C.

[BibT_eX]

[DOI]

Michael Ryabtsev

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

2008

Decision Procedures - An Algorithmic Point of View

[BibT_eX]

[DOI]

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

An approach for extracting a small unsatisfiable core.

[BibT_eX]

[DOI]

Maya Koifman

Formal Methods Syst. Des., 2008

Three optimizations for Assume-Guarantee reasoning with L<sup>*</sup>.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2008

Inference rules for proving the equivalence of recursive procedures.

[BibT_eX]

[DOI]

Acta Informatica, 2008

Local Restarts.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2008

Linear-Time Reductions of Resolution Proofs.

[BibT_eX]

[DOI]

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

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

[BibT_eX]

[DOI]

Dan Goldwasser

Shai Fine

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

2007

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

[BibT_eX]

[DOI]

Mirron Rozanov

Proceedings of the 5th International Workshop on Satisfiability Modulo Theories, 2007

Optimized L*-Based Assume-Guarantee Reasoning.

[BibT_eX]

[DOI]

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

Deciding Bit-Vector Arithmetic with Abstraction.

[BibT_eX]

[DOI]

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

Easier and More Informative Vacuity Checks.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Arie Matsliah

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

2006

Error explanation with distance metrics.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2006

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

[BibT_eX]

[DOI]

Yoav Rodeh

Inf. Comput., 2006

Deriving Small Unsatisfiable Cores with Dominators.

[BibT_eX]

[DOI]

Maya Koifman

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

2005

Computational challenges in bounded model checking.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2005

Introductory paper.

[BibT_eX]

[DOI]

Armin Biere

Int. J. Softw. Tools Technol. Transf., 2005

Reduced Functional Consistency of Uninterpreted Functions.

[BibT_eX]

[DOI]

Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning, 2005

Preface.

[BibT_eX]

[DOI]

Armin Biere

Proceedings of the Third International Workshop on Bounded Model Checking, 2005

Regression Verification - A Practical Way to Verify Programs.

[BibT_eX]

[DOI]

Proceedings of the Verified Software: Theories, 2005

Cost-Effective Hyper-Resolution for Preprocessing CNF Formulas.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2005

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

[BibT_eX]

[DOI]

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

HaifaSat: A New Robust SAT Solver.

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software Verification and Testing, 2005

Yet Another Decision Procedure for Equality Logic.

[BibT_eX]

[DOI]

Orly Meir

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

Abstraction Refinement for Bounded Model Checking.

[BibT_eX]

[DOI]

Anubhav Gupta

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

2004

SAT-based counterexample-guided abstraction refinement.

[BibT_eX]

[DOI]

Edmund M. Clarke

Anubhav Gupta

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2004

Accelerating Bounded Model Checking of Safety Properties.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2004

Efficient Verification of Sequential and Concurrent C Programs.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2004

Deciding Disjunctive Linear Arithmetic with SAT

[BibT_eX]

[DOI]

CoRR, 2004

Completeness and Complexity of Bounded Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2004

Explaining abstract counterexamples.

[BibT_eX]

[DOI]

Alex Groce

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.

[BibT_eX]

[DOI]

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

Abstraction-Based Satisfiability Solving of Presburger Arithmetic.

[BibT_eX]

[DOI]

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).

[BibT_eX]

[DOI]

Inf. Comput., 2003

Bounded model checking.

[BibT_eX]

[DOI]

Adv. Comput., 2003

Efficient Computation of Recurrence Diameters.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2003

Predicate Abstraction with Minimum Predicates.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 2003

2002

The Small Model Property: How Small Can It Be?

[BibT_eX]

[DOI]

Inf. Comput., 2002

On Solving Presburger and Linear Arithmetic with SAT.

[BibT_eX]

[DOI]

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

Deciding Separation Formulas with SAT.

[BibT_eX]

[DOI]

Sanjit A. Seshia

Randal E. Bryant

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

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

[BibT_eX]

[DOI]

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

2001

Using Simulation to Increase Efficiency in an Army Recruitment Office.

[BibT_eX]

[DOI]

Ofer Shtrichman

Rami Ben-Haim

Moshe Asher Pollatschek

Interfaces, 2001

Range Allocation for Equivalence Logic.

[BibT_eX]

[DOI]

Yoav Rodeh

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.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 2001

Finite Instantiations in Equivalence Logic with Uninterpreted Functions.

[BibT_eX]

[DOI]

Yoav Rodeh

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

2000

Tuning SAT Checkers for Bounded Model Checking.

[BibT_eX]

[DOI]

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

1999

Deciding Equality Formulas by Small Domains Instantiations.

[BibT_eX]

[DOI]

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

Translation Validation: From SIGNAL to C.

[BibT_eX]

[DOI]

Proceedings of the Correct System Design, 1999

1998

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

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 1998

Translation Validation for Synchronous Languages.

[BibT_eX]

[DOI]

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

Translation Validation: From DC+ to C*.

[BibT_eX]

[DOI]