Incremental formal verification of hardware. - Hana Chockler; Alexander Ivrii; Arie Matsliah; Shiri Moran; Ziv Nevo (FMCAD, 2011)

IC3-guided abstraction. - Jason Baumgartner; Alexander Ivrii; Arie Matsliah; Hari Mony (FMCAD, 2012)

Computing Interpolants without Proofs. - Hana Chockler; Alexander Ivrii; Arie Matsliah (Haifa Verification Conference, 2012)

On Efficient Computation of Variable MUSes. - Anton Belov; Alexander Ivrii; Arie Matsliah; João Marques-Silva 001 (SAT, 2012)

Perfect Hashing and CNF Encodings of Cardinality Constraints. - Yael Ben-Haim; Alexander Ivrii; Oded Margalit; Arie Matsliah (SAT, 2012)

Generalized counterexamples to liveness properties. - Gadi Aleksandrowicz; Jason Baumgartner; Alexander Ivrii; Ziv Nevo (FMCAD, 2013)

Using cross-entropy for satisfiability. - Hana Chockler; Alexander Ivrii; Arie Matsliah; Simone Fulvio Rollini; Natasha Sharygina (SAC, 2013)

Small inductive safe invariants. - Alexander Ivrii; Arie Gurfinkel; Anton Belov (FMCAD, 2014)

Generating Modulo-2 Linear Invariants for Hardware Model Checking. - Gadi Aleksandrowicz; Alexander Ivrii; Oded Margalit; Dan Rasin (Haifa Verification Conference, 2014)

Pushing to the Top. - Arie Gurfinkel; Alexander Ivrii (FMCAD, 2015)

Speeding up MUS Extraction with Preprocessing and Chunking. - Valeriy Balabanov; Alexander Ivrii (SAT, 2015)

Mining Backbone Literals in Incremental SAT - A New Kind of Incremental Data. - Alexander Ivrii; Vadim Ryvchin; Ofer Strichman (SAT, 2015)

Constrained Sampling and Counting: Universal Hashing Meets SAT Solving. - Kuldeep S. Meel; Moshe Y. Vardi; Supratik Chakraborty; Daniel J. Fremont; Sanjit A. Seshia; Dror Fried; Alexander Ivrii; Sharad Malik (AAAI Workshop: Beyond NP, 2016)

The art of semi-formal bug hunting. - Pradeep Kumar Nalla; Raj Kumar Gajavelly; Jason Baumgartner; Hari Mony; Robert Kanzelman; Alexander Ivrii (ICCAD, 2016)

On computing minimal independent support and its applications to sampling and counting. - Alexander Ivrii; Sharad Malik; Kuldeep S. Meel; Moshe Y. Vardi (Constraints An Int. J., 2016)

Learning support sets in IC3 and Quip: The good, the bad, and the ugly. - Ryan Berryhill; Alexander Ivrii; Neil Veira; Andreas G. Veneris (FMCAD, 2017)

K-induction without unrolling. - Arie Gurfinkel; Alexander Ivrii (FMCAD, 2017)

The Computational Complexity of Structure-Based Causality. - Gadi Aleksandrowicz; Hana Chockler; Joseph Y. Halpern; Alexander Ivrii (J. Artif. Intell. Res., 2017)

k-FAIR = k-LIVENESS + FAIR Revisiting SAT-based Liveness Algorithms. - Alexander Ivrii; Ziv Nevo; Jason Baumgartner (FMCAD, 2018)

Finding All Minimal Safe Inductive Sets. - Ryan Berryhill; Alexander Ivrii; Andreas G. Veneris (SAT, 2018)

Boosting Verification Scalability via Structural Grouping and Semantic Partitioning of Properties. - Rohit Dureja; Jason Baumgartner; Alexander Ivrii; Robert Kanzelman; Kristin Y. Rozier (FMCAD, 2019)

Input Elimination Transformations for Scalable Verification and Trace Reconstruction. - Raj Kumar Gajavelly; Jason Baumgartner; Alexander Ivrii; Robert L. Kanzelman; Shiladitya Ghosh (FMCAD, 2019)

Late Breaking Results: FRIENDS - Finding Related Interesting Events via Neighbor Detection. - Raviv Gal; Haim Kermany; Alexander Ivrii; Ziv Nevo; Avi Ziv (DAC, 2020)

IC3 with Internal Signals. - Rohit Dureja; Arie Gurfinkel; Alexander Ivrii; Yakir Vizel (FMCAD, 2021)

Exploiting Isomorphic Subgraphs in SAT. - Alexander Ivrii; Ofer Strichman (FMCAD, 2021)

Exploiting Isomorphic Subgraphs in SAT (Long version). - Alexander Ivrii; Ofer Strichman (CoRR, 2021)

LightSABRE: A Lightweight and Enhanced SABRE Algorithm. - Henry Zou; Matthew Treinish; Kevin Hartman; Alexander Ivrii; Jake Lishman (CoRR, 2024)

Linear circuit synthesis using weighted Steiner trees. - Michele Nir Gavrielov; Alexander Ivrii; Shelly Garion (Quantum Inf. Comput., 2024)