Publications

2017

"Learning Support Sets in IC3 and Quip: the Good, the Bad, and the Ugly" Ryan Berryhill, Alexander Ivrii, Neil Veira and Andreas Veneris, FMCAD 2017 [pdf]

"K-Induction without Unrolling" Arie Gurfinkel and Alexander Ivrii, FMCAD 2017 [pdf]

2016

"The Art of Semi-Formal Bug Hunting" Pradeep Kumar Nalla, Raj Kumar Gajavelly, Jason Baumgartner, Hari Mony, Robert Kanzelman, Alexander Ivrii ICCAD, 2016

2015

"Pushing to the Top" Arie Gurfinkel, Alexander Ivrii, FMCAD 2015 [pdf]

2014

"Small Inductive Safe Invariants" Alexander Ivrii, Arie Gurfinkel and Anton Belov Formal Methods in Computer-Aided Design, 2014

"Generating Linear Invariants for Model Checking" Gadi Aleksandrowicz, Alexander Ivrii, Oded Margalit, and Dan Rasin Haifa Verification Conference, 2014

"Automatic Verification of Floating Point Units" U. Krautz, V. Paruthi, A. Arunagiri, S. Kumar, S. Pujar, T. Babinsky Design Automation Conference,2014. [pdf]

"Verification of Galois Field Based Circuits by Formal Reasoning Based on Computational Algebraic Geometry" A. Lvov, L. A. Lastras-Montaño, B. Trager, V. Paruthi, R. Shadowen, A. El-Zein Formal Methods in System Design,2014. [pdf]

"Scalable reachability analysis via automated dynamic netlist-based hint generation" J. Xu, M. Williams, H. Mony, J. Baumgartner Journal of Formal Methods in System Design,2014. [pdf]

"Effective Liveness Verification Using a Transformation-Based Framework" P.K. Nalla, R.J. Gajavelly, H. Mony, J. Baumgartner, R. Kanzelman VLSI Design, 2014. [pdf]

2013

"GLA: gate-level abstraction revisited" A. Mishchenko, N. Eén, R. K. Brayton, J. Baumgartner, H. Mony, P.K. Nalla Design Automation and Test in Europe,2013. [pdf]

"Generalized counterexamples to liveness properties" G. Aleksandrowicz, J. Baumgartner, A. Ivrii, Z. Nevo Formal Methods in Computer-Aided Design,2013. [pdf]

"Using cross-entropy for satisfiability" H. Chockler, A. Ivrii, A. Matsliah, S.F. Rollini, N. Sharygina Symposium on Applied Computing,2013. [pdf]

2012

"Enhanced reachability analysis via automated dynamic netlist-based hint generation" J. Xu, M. Williams, H. Mony, J. Baumgartner Formal Methods in Computer-Aided Design, 2012. [pdf]

"IC3-guided abstraction" J. Baumgartner, A. Ivrii, A. Matsliah, H. Mony Formal Methods in Computer-Aided Design, 2012. [pdf]

"Formal verification of error correcting circuits using computational algebraic geometry" A. Lvov, L.A. Lastras-Montano, V. Paruthi, R. Shadowen, A. El-Zein Formal Methods in Computer-Aided Design, 2012. [pdf]

"On Efficient Computation of Variable MUSes" A. Belov, A. Ivrii, A. Matsliah, J. Marques-Silva Sat, 2012. [pdf]

"Augmenting Clause Learning with Implied Literals" A. Matsliah, A. Sabharwal, H. Samulowitz Sat, 2012. [pdf]

"Computing Interpolants without Proofs" H. Chockler, A. Ivrii, A. Matsliah Haifa Verification Conference, 2012. [pdf]

"Perfect Hashing and CNF Encodings of Cardinality Constraints" Y. Ben-Haim, A. Ivrii, O. Margalit, A. Matsliah Sat, 2012. [pdf]

2011

"Incremental formal verification of hardware" H. Chockler, A. Ivrii, A. Matsliah, S. Moran, Z. Nevo Formal Methods in Computer-Aided Design, 2011. [pdf]

"Functional verification of the IBM POWER7 microprocessor and POWER7 multiprocessor systems" K.D. Schubert, W. Roesner, J. M. Ludden, J. Jackson, J. Buchert, V. Paruthi, M. Behm, A. Ziv, J. Schumann, C. Meissner, J. Koesters, J. Hsu, B. Brock IBM Journal of Research and Development, 2011.

"Optimal redundancy removal without fixedpoint computation" M. L. Case, J. Baumgartner, H. Mony and R. L. Kanzelman Formal Methods in Computer Aided Design, 2011. [pdf]

"Approximate reachability with combined symbolic and ternary simulation" M. L. Case, J. Baumgartner, H. Mony and R. L. Kanzelman Formal Methods in Computer Aided Design, 2011. [pdf]

"Hybrid verification of a hardware modular reduction engine" J. Sawada, P. Sandon, V. Paruthi, J. Baumgartner, M. L. Case and H. Mony Formal Methods in Computer Aided Design, 2011. [pdf]

2010

"Large-scale Application of Formal Verification: From Fiction to Fact" V. Paruthi Formal Methods in Computer-Aided Design, 2010. [pdf]

"Formal Verification of Arbiters using Property Strengthening and Underapproximations" G. Auerbach, F. Copty, V.Paruthi Formal Methods in Computer-Aided Design, 2010. [pdf]

"Coping with Moore's Law (and More): Supporting Arrays in State-of-the-Art Model Checkers" J. Baumgartner, M. L. Case and H. Mony Formal Methods in Computer Aided Design, 2010. [pdf]

2009

"Formal Verification of Correctness and Performance of Random Priority-based Arbiters" K. Kailas, V. Paruthi, B. Monwai Formal Methods in Computer-Aided Design, 2009. [pdf]

"Enhanced Verification by Temporal Decomposition" M. L. Case, H. Mony, J. Baumgartner and R. Kanzelman Formal Methods in Computer Aided Design, 2009. [pdf]

"Scalable Conditional Equivalence Checking: An Automated Invariant-Generation Based Approach" J. Baumgartner, H. Mony, M. Case, J. Sawada and K. Yorav Formal Methods in Computer Aided Design, 2009. [pdf]

"Scalable Liveness Checking via Property-Preserving Transformations" J. Baumgartner and H. Mony, Design Automation and Test in Europe, 2009. [pdf]

"Speculative-Reduction based Scalable Redundancy Identification" H. Mony, J. Baumgartner, A. Mishchenko and R. K. Brayton, Design Automation and Test in Europe, 2009. [pdf]

"On Invariants to Characterize the State Space for Sequential Logic Synthesis and Formal Verification Invariant-Strengthened Elimination of Dependent State Elements" Michael L Case, PhD Thesis. The University of California, Berkeley, CA, 2009. [pdf]

2008

"Optimal Constraint-Preserving Netlist Simplification" J. Baumgartner, H. Mony and A. Aziz, Formal Methods in Computer-Aided Design, 2008. [pdf]

"Invariant Strengthened Elimination of Dependent State Elements" M. L. Case, A. Mishchenko, R. K. Brayton, J. Baumgartner and H. Mony, Formal Methods in Computer-Aided Design, 2008. [pdf]

"Merging Nodes Under Sequential Observability" M. L. Case, V. N. Kravets, A. Mishchenko and R. K. Brayton, Design Automation Conference, 2008. [pdf]

"Sequential Redundancy Identification using Transformation-Based Verification" Hari Mony, PhD Thesis. The University of Texas, Austin, TX, 2008. [pdf]

2007

"Formal Verification of Partial Good Self-Test Fencing Structures" A. Seigler, G. V. Huben and H.Mony, Formal Methods in Computer-Aided Design, 2007. [pdf]

2006

"Enabling Large-Scale Pervasive Logic Verification through Multi-Algorithmic Formal Reasoning." J. Baumgartner, T. Gloekler, D. Shanmugam, R. Seigler, G. V. Huben, H. Mony, P. Roessler, and B. Ramanandray, Formal Methods in Computer-Aided Design, San Jose, CA. November 2006. [pdf]

"Scalable Sequential Equivalence Checking across Arbitrary Design Transformations." J. Baumgartner, H. Mony, V. Paruthi, R. Kanzelman and G. Janssen, International Conference on Computer Design, San Jose, CA. October 2006. [pdf]

2005

"Automatic Verification of Fused-Multiply-Add FPUs." C. Jacobi, K. Weber, V. Paruthi, and J. Baumgartner, Design Automation and Test in Europe, 2005. [pdf]

"Maximal Input Reduction of Sequential Netlists via Synergistic Reparameterization and Localization Strategies." J. Baumgartner and H. Mony, Correct Hardware Design and Verification Methods, 2005. [pdf]

"Exploiting Constraints in Transformation-Based Verification." H. Mony, J. Baumgartner and A. Aziz, Correct Hardware Design and Verification Methods, 2005. [pdf]

"Efficient Symbolic Simulation via Dynamic Scheduling, Don't Caring, and Case Splitting." V. Paruthi, C. Jacobi and K. Weber, Correct Hardware Design and Verification Methods, 2005. [pdf]

"Scalable Compositional Minimization via Static Analysis." F. A. Zaraket, J. Baumgartner and A. Aziz, International Conference on Computer-Aided Design, 2005. [pdf]

"Exploiting Suspected Redundancy without Proving It" H. Mony, J. Baumgartner, V. Paruthi, R. Kanzelman, Design Automation Conference , 2005. [pdf]

2004

"Scalable Automated Verification via Expert-System Guided Transformations." H. Mony, J. Baumgartner, V. Paruthi, R. Kanzelman and A. Kuehlmann, Conference on Formal Methods in Computer-Aided Design, 2004. [pdf]

"Enhanced Diameter Bounding via Structural Transformation." J. Baumgartner and A. Kuehlmann, Design Automation and Test in Europe, 2004. [pdf]

2003

"An Abstraction Algorithm for Verification of Level-Sensitive Latch-Based Netlists." J. Baumgartner, T. Heyman, V. Singhal, and A. Aziz, Journal of Formal Methods in System Design, Volume 23, pp. 39-65, 2003. [pdf]

2002

"Robust Boolean Reasoning for Equivalence Checking and Functional Property Verification." A. Kuehlmann, V. Paruthi, F. Krohm and M.K. Ganai, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Volume 21, pp. 1377-1394, December 2002. [pdf]

"Property Checking via Structural Analysis." J. Baumgartner, A. Kuehlmann, and J. Abraham, Conference on Computer-Aided Verification, 2002. [pdf]

"Automatic Structural Abstraction Techniques for Enhanced Verification." J. Baumgartner, PhD Thesis. The University of Texas, Austin, TX, 2002. [pdf]

2001

"Circuit Based Boolean Reasoning." A. Kuehlmann, M.K. Ganai, and V. Paruthi, Design Automation Conference, 2001. [pdf]

"Design of a Pointerless BDD Package." Geert Janssen, International Workshop on Logic & Synthesis, 2001. [pdf]

"Transformation-Based Verification Using Generalized Retiming." A. Kuehlmann and J. Baumgartner, Conference on Computer-Aided Verification, 2001. [pdf]

"Min-Area Retiming on Flexible Circuit Structures." J. Baumgartner and A. Kuehlmann, International Conference on Computer-Aided Design, 2001. [pdf]

2000

"An Abstraction Algorithm for Verification of Generalized C-Slow Designs." J. Baumgartner, A. Tripp, A. Aziz, V. Singhal, and F. Andersen, Conference on Computer-Aided Verification, 2000. [pdf]

"Equivalence Checking combining a Structural SAT-solver, BDDs and Simulation." V. Paruthi and A. Kuehlmann, International Conference on Computer Design, 2000. [pdf]

"On-the-Fly Compression of Logical Circuits." M.K. Ganai and A. Kuehlmann, International Workshop on Logic & Synthesis, 2000. [pdf]

1999

"Model Checking the IBM Gigahertz Processor: An Abstraction Algorithm for High-Performance Netlists." J. Baumgartner, T. Heyman, V. Singhal, and A. Aziz, Conference on Computer-Aided Verification, 1999. [pdf]

1997

"Equivalence Checking using Cuts and Heaps." A. Kuehlmann and F. Krohm, Design Automation Conference, 1997. [pdf]

1996

"The Use of Random Simulation in Formal Verification." F. Krohm, A. Kuehlmann, and A. Mets, International Conference on Computer Design, 1996. [pdf]