Connect with us:    

IBM Research YouTube IBM Research Blog

Formal Quality Technologies (FQT)

Our focus is on Cloud Quality and Verification. We build technologies and solutions to improve the quality of the cloud computing stack (SaaS, PaaS and IaaS), concentrating on policy management and network security.

Our expertise covers a wide spectrum of technologies in the space of hardware and software verification, automated reasoning, networking and cloud computing.
With our vast expertise in verification technologies, we support IBM product teams and participate in research activities that advance automated reasoning science and cloud computing technology.

 

Shai Doron, Manager Formal Quality Technologies, IBM Research - Haifa

Shai Doron,
Manager, Formal Quality Technologies,
IBM Research - Haifa

Research

Network-Policy Analysis

Microservices-based architecture lies at the heart of many modern cloud applications. In such architectures, services communicate using lightweight protocols that are governed by network policies. We are developing a tool that builds a semantic model for a given set of network policies, allowing various analyses to be performed.

Read More

 
 

RuleBase SixthSense Edition

RuleBase SixthSense Edition represents the third generation of successful formal verification technology in IBM. The tool combines powerful property checking capabilities with advanced sequential equivalence checking technology and a unique transformation-based verification framework.

Read More

 
 

Publications

Author Title Conference/Journal Year  
R. Gal, H. Kermany, A. Ivrii, Z. Nevo, A. Ziv Late breaking results: Friends - finding related interesting events via neighbor detection Design Automation Conference, (DAC) 2020 2020 Link
Rohit Dureja; Jason Baumgartner; Robert Kanzelman; Mark Williams; Kristin Y. Rozier Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration FMCAD 2020 2020 Link
Raj Kumar Gajavelly, Jason Baumgartner, Alexander Ivrii, Robert L. Kanzelman, Shiladitya Ghosh Input Elimination Transformations for Scalable Verification and Trace Reconstruction FMCAD 2019 2019 Link
Rohit Dureja, Jason Baumgartner, Alexander Ivrii, Robert Kanzelman, Kristin Y. Rozier Boosting Verification Scalability via Structural Grouping and Semantic Partitioning of Properties FMCAD 2019 2019 Link
Ryan Berryhill, Alexander Ivrii, Andreas G. Veneris Finding All Minimal Safe Inductive Sets SAT 2018 2018 Link
Alexander Ivrii, Ziv Nevo, Jason Baumgartner k-FAIR = k-LIVENESS + FAIR Revisiting SAT-based Liveness Algorithms FMCAD 2018 2018 Link
Ryan Berryhill, Alexander Ivrii, Neil Veira and Andreas Veneris Learning Support Sets in IC3 and Quip: the Good, the Bad, and the Ugly FMCAD 2017 Link
Arie Gurfinkel and Alexander Ivrii K-Induction without Unrolling FMCAD 2017 Link
Pradeep Kumar Nalla, Raj Kumar Gajavelly, Jason Baumgartner, Hari Mony, Robert Kanzelman, Alexander Ivrii The Art of Semi-Formal Bug Hunting ICCAD 2016 Link
S. Bergman, G. Bobok, W. Kowalski, S. Koyfman, S. Moran, Z. Nevo, A. Orni, V. Paruthi, W. Roesner, G. Shurek, V. Vuyyuru Designer-Level Verification – an Industrial Experience Story DATE 2015 2015 Link
Arie Gurfinkel, Alexander Ivrii Pushing to the Top FMCAD 2015 Link
Alexander Ivrii, Arie Gurfinkel and Anton Belov Small Inductive Safe Invariants Formal Methods in Computer-Aided Design 2014 Link
Gadi Aleksandrowicz, Alexander Ivrii, Oded Margalit, and Dan Rasin Generating Linear Invariants for Model Checking Haifa Verification Conference 2014  
U. Krautz, V. Paruthi, A. Arunagiri, S. Kumar, S. Pujar, T. Babinsky Automatic Verification of Floating Point Units Design Automation Conference 2014 Link
A. Lvov, L. A. Lastras-Montaño, B. Trager, V. Paruthi, R. Shadowen, A. El-Zein Verification of Galois Field Based Circuits by Formal Reasoning Based on Computational Algebraic Geometry Formal Methods in System Design 2014 Link
J. Xu, M. Williams, H. Mony, J. Baumgartner Scalable reachability analysis via automated dynamic netlist-based hint generation Journal of Formal Methods in System Design 2014 Link
P.K. Nalla, R.J. Gajavelly, H. Mony, J. Baumgartner, R. Kanzelman Effective Liveness Verification Using a Transformation-Based Framework VLSI Design 2014 Link
A. Mishchenko, N. Eén, R. K. Brayton, J. Baumgartner, H. Mony, P.K. Nalla GLA: gate-level abstraction revisited Design Automation and Test in Europe 2013 Link
G. Aleksandrowicz, J. Baumgartner, A. Ivrii, Z. Nevo Generalized counterexamples to liveness properties Formal Methods in Computer-Aided Design 2013 Link
H. Chockler, A. Ivrii, A. Matsliah, S.F. Rollini, N. Sharygina Using cross-entropy for satisfiability Symposium on Applied Computing 2013 Link
J. Xu, M. Williams, H. Mony, J. Baumgartner Enhanced reachability analysis via automated dynamic netlist-based hint generation Formal Methods in Computer-Aided Design 2012 Link
J. Baumgartner, A. Ivrii, A. Matsliah, H. Mony IC3-guided abstraction Formal Methods in Computer-Aided Design 2012 Link
A. Lvov, L.A. Lastras-Montano, V. Paruthi, R. Shadowen, A. El-Zein Formal verification of error correcting circuits using computational algebraic geometry Formal Methods in Computer-Aided Design 2012 Link
A. Belov, A. Ivrii, A. Matsliah, J. Marques-Silva On Efficient Computation of Variable MUSes Sat 2012 Link
A. Matsliah, A. Sabharwal, H. Samulowitz Augmenting Clause Learning with Implied Literals Sat 2012 Link
H. Chockler, A. Ivrii, A. Matsliah Computing Interpolants without Proofs Haifa Verification Conference 2012 Link
Y. Ben-Haim, A. Ivrii, O. Margalit, A. Matsliah Perfect Hashing and CNF Encodings of Cardinality Constraints Sat 2012 Link
H. Chockler, A. Ivrii, A. Matsliah, S. Moran, Z. Nevo Incremental formal verification of hardware Formal Methods in Computer-Aided Design 2011 Link
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 Functional verification of the IBM POWER7 microprocessor and POWER7 multiprocessor systems IBM Journal of Research and Development 2011 Link
M. L. Case, J. Baumgartner, H. Mony and R. L. Kanzelman Optimal redundancy removal without fixedpoint computation Formal Methods in Computer Aided Design 2011 Link
M. L. Case, J. Baumgartner, H. Mony and R. L. Kanzelman Approximate reachability with combined symbolic and ternary simulation Formal Methods in Computer Aided Design 2011 Link
J. Sawada, P. Sandon, V. Paruthi, J. Baumgartner, M. L. Case and H. Mony Hybrid verification of a hardware modular reduction engine Formal Methods in Computer Aided Design 2011 Link
V. Paruthi Large-scale Application of Formal Verification: From Fiction to Fact Formal Methods in Computer-Aided Design 2010 Link
G. Auerbach, F. Copty, V.Paruthi Formal Verification of Arbiters using Property Strengthening and Underapproximations Formal Methods in Computer-Aided Design 2010 Link
J. Baumgartner, M. L. Case and H. Mony Coping with Moore's Law (and More): Supporting Arrays in State-of-the-Art Model Checkers Formal Methods in Computer Aided Design 2010 Link