| 2026 | CAV | Learning to Split: A Reinforcement-Learning-Guided Splitting Heuristic for Neural Network Verification (Invited Talk). | Maya Swisa, Guy Katz |
| 2026 | MODELSWARD | On Integrating Large Language Models and Scenario-Based Modeling for Improving Software Reliability. | Ayelet Berzack, Guy Katz |
| 2026 | VMCAI | Proof Minimization in Neural Network Verification. | Omri Isac, Idan Refaeli, Haoze Wu, Clark W. Barrett, Guy Katz |
| 2025 | AAAI | Shield Synthesis for LTL Modulo Theories. | Andoni Rodrguez, Guy Amir, Davide Corsi, Csar Snchez, Guy Katz |
| 2025 | AISTATS | On the Computational Tractability of the (Many) Shapley Values. | Reda Marzouk, Shahaf Bassan, Guy Katz, Colin de la Higuera |
| 2025 | ENASE | A Study on the Comprehensibility of Behavioral Programming Variants. | Adiel Ashrov, Arnon Sturm, Achiya Elyasaf, Guy Katz |
| 2025 | ENASE | Exploring and Evaluating Interplays of BPpy with Deep Reinforcement Learning and Formal Methods. | Tom Yaacov, Gera Weiss, Adiel Ashrov, Guy Katz, Jules Zisser |
| 2025 | ESOP | Neural Network Verification is a Programming Language Challenge. | Lucas C. Cordeiro, Matthew L. Daggitt, Julien Girard-Satabin, Omri Isac, Taylor T. Johnson, Guy Katz, Ekaterina Komendantskaya, Augustin Lemesle, Edoardo Manino, Artjoms Sinkarovs, Haoze Wu |
| 2025 | ICML | What makes an Ensemble (Un) Interpretable? | Shahaf Bassan, Guy Amir, Meirav Zehavi, Guy Katz |
| 2025 | ICML | Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations. | Shahaf Bassan, Yizhak Yisrael Elboher, Tobias Ladner, Matthias Althoff, Guy Katz |
| 2025 | ITP | A Certified Proof Checker for Deep Neural Network Verification in Imandra. | Remi Desmartin, Omri Isac, Grant O. Passmore, Ekaterina Komendantskaya, Kathrin Stark, Guy Katz |
| 2025 | RV | Statistical Runtime Verification for LLMs via Robustness Estimation. | Natan Levy, Adiel Ashrov, Guy Katz |
| 2024 | CAV | Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. | Haoze Wu, Omri Isac, Aleksandar Zeljic, Teruhiro Tagomori, Matthew L. Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, Pei Huang, Ori Lahav, Min Wu, Min Zhang, Ekaterina Komendantskaya, Guy Katz, Clark W. Barrett |
| 2024 | ECAI | Hard to Explain: On the Computational Hardness of In-Distribution Model Interpretation. | Guy Amir, Shahaf Bassan, Guy Katz |
| 2024 | FMCAD | Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates. | Udayan Mandal, Guy Amir, Haoze Wu, Ieva Daukantas, Fletcher Lee Newell, Umberto J. Ravaioli, Baoluo Meng, Michael Durling, Milan Ganai, Tobey Shim, Guy Katz, Clark W. Barrett |
| 2024 | ICML | Local vs. Global Interpretability: A Computational Complexity Perspective. | Shahaf Bassan, Guy Amir, Guy Katz |
| 2024 | ICONIP | Enforcing Specific Behaviours via Constrained DRL and Scenario-Based Programming. | Davide Corsi, Raz Yerushalmi, Guy Amir, Alessandro Farinelli, David Harel, Guy Katz |
| 2024 | MODELSWARD | On Augmenting Scenario-Based Modeling with Generative AI. | David Harel, Guy Katz, Assaf Marron, Smadar Szekely |
| 2024 | VMCAI | Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training. | Jiaxu Tian, Dapeng Zhi, Si Liu, Peixin Wang, Guy Katz, Min Zhang |
| 2023 | CAV | Verifying Generalization in Deep Learning. | Guy Amir, Osher Maayan, Tom Zelazny, Guy Katz, Michael Schapira |
| 2023 | CONCUR | DNN Verification, Reachability, and the Exponential Function Problem. | Omri Isac, Yoni Zohar, Clark W. Barrett, Guy Katz |
| 2023 | FM | veriFIRE: Verifying an Industrial, Learning-Based Wildfire Detection System. | Guy Amir, Ziv Freund, Guy Katz, Elad Mandelbaum, Idan Refaeli |
| 2023 | FMCAD | Formally Explaining Neural Networks within Reactive Systems. | Shahaf Bassan, Guy Amir, Davide Corsi, Idan Refaeli, Guy Katz |
| 2023 | FMCAD | DelBugV: Delta-Debugging Neural Network Verifiers. | Raya Elsaleh, Guy Katz |
| 2023 | LOPSTR | Towards a Certified Proof Checker for Deep Neural Network Verification. | Remi Desmartin, Omri Isac, Grant O. Passmore, Kathrin Stark, Ekaterina Komendantskaya, Guy Katz |
| 2023 | LPAR | Tighter Abstract Queries in Neural Network Verification. | Elazar Cohen, Yizhak Yisrael Elboher, Clark W. Barrett, Guy Katz |
| 2023 | MODELSWARD | Enhancing Deep Learning with Scenario-Based Override Rules: A Case Study. | Adiel Ashrov, Guy Katz |
| 2023 | TACAS | Verifying Learning-Based Robotic Navigation Systems. | Guy Amir, Davide Corsi, Raz Yerushalmi, Luca Marzari, David Harel, Alessandro Farinelli, Guy Katz |
| 2023 | TACAS | Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks. | Shahaf Bassan, Guy Katz |
| 2023 | TACAS | OccRob: Efficient SMT-Based Occlusion Robustness Verification of Deep Neural Networks. | Xingwu Guo, Ziwei Zhou, Yueling Zhang, Guy Katz, Min Zhang |
| 2023 | VECoS | gRoMA: A Tool for Measuring the Global Robustness of Deep Neural Networks. | Natan Levy, Raz Yerushalmi, Guy Katz |
| 2022 | ATVA | An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks. | Matan Ostrovsky, Clark W. Barrett, Guy Katz |
| 2022 | CAV | Neural Network Robustness as a Verification Property: A Principled Case Study. | Marco Casadio, Ekaterina Komendantskaya, Matthew L. Daggitt, Wen Kokke, Guy Katz, Guy Amir, Idan Refaeli |
| 2022 | CAV | Minimal Multi-Layer Modifications of Deep Neural Networks. | Idan Refaeli, Guy Katz |
| 2022 | FMCAD | Verification-Aided Deep Ensemble Selection. | Guy Amir, Tom Zelazny, Guy Katz, Michael Schapira |
| 2022 | FMCAD | Neural Network Verification with Proof Production. | Omri Isac, Clark W. Barrett, Min Zhang, Guy Katz |
| 2022 | FMCAD | On Optimizing Back-Substitution Methods for Neural Network Verification. | Tom Zelazny, Haoze Wu, Clark W. Barrett, Guy Katz |
| 2022 | ICONIP | RoMA: A Method for Neural Network Robustness Measurement and Assessment. | Natan Levy, Guy Katz |
| 2022 | MODELSWARD | Scenario-assisted Deep Reinforcement Learning. | Raz Yerushalmi, Guy Amir, Achiya Elyasaf, David Harel, Guy Katz, Assaf Marron |
| 2022 | SEFM | Neural Network Verification Using Residual Reasoning. | Yizhak Yisrael Elboher, Elazar Cohen, Guy Katz |
| 2022 | TACAS | Efficient Neural Network Analysis with Sum-of-Infeasibilities. | Haoze Wu, Aleksandar Zeljic, Guy Katz, Clark W. Barrett |
| 2021 | FMCAD | Towards Scalable Verification of Deep Reinforcement Learning. | Guy Amir, Michael Schapira, Guy Katz |
| 2021 | FMCAD | Pruning and Slicing Neural Networks using Formal Verification. | Ori Lahav, Guy Katz |
| 2021 | MODELSWARD | Towards Repairing Scenario-Based Models with Rich Events. | Guy Katz |
| 2021 | SIGCOMM | Verifying learning-augmented systems. | Tomer Eliyahu, Yafim Kazak, Guy Katz, Michael Schapira |
| 2021 | TACAS | An SMT-Based Approach for Verifying Binarized Neural Networks. | Guy Amir, Haoze Wu, Clark W. Barrett, Guy Katz |
| 2020 | ATVA | Verifying Recurrent Neural Networks Using Invariant Inference. | Yuval Jacoby, Clark W. Barrett, Guy Katz |
| 2020 | CAV | An Abstraction-Based Framework for Neural Network Verification. | Yizhak Yisrael Elboher, Justin Gottschlich, Guy Katz |
| 2020 | FMCAD | Parallelization Techniques for Verifying Neural Networks. | Haoze Wu, Alex Ozdemir, Aleksandar Zeljic, Kyle Julian, Ahmed Irfan, Divya Gopinath, Sadjad Fouladi, Guy Katz, Corina S. Pasareanu, Clark W. Barrett |
| 2020 | LPAR | Minimal Modifications of Deep Neural Networks using Verification. | Ben Goldberger, Guy Katz, Yossi Adi, Joseph Keshet |
| 2020 | MODELSWARD | Guarded Deep Learning using Scenario-based Modeling. | Guy Katz |
| 2020 | MODELSWARD | Augmenting Deep Neural Networks with Scenario-Based Guard Rules. | Guy Katz |
| 2019 | CAV | The Marabou Framework for Verification and Analysis of Deep Neural Networks. | Guy Katz, Derek A. Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljic, David L. Dill, Mykel J. Kochenderfer, Clark W. Barrett |
| 2019 | MODELSWARD | Executing Scenario-Based Specification with Dynamic Generation of Rich Events. | David Harel, Guy Katz, Assaf Marron, Aviran Sadon, Gera Weiss |
| 2019 | MODELSWARD | On-the-Fly Construction of Composite Events in Scenario-Based Modeling using Constraint Solvers. | Guy Katz, Assaf Marron, Aviran Sadon, Gera Weiss |
| 2019 | SIGCOMM | Verifying Deep-RL-Driven Systems. | Yafim Kazak, Clark W. Barrett, Guy Katz, Michael Schapira |
| 2018 | ATVA | DeepSafe: A Data-Driven Approach for Assessing Robustness of Neural Networks. | Divya Gopinath, Guy Katz, Corina S. Pasareanu, Clark W. Barrett |
| 2017 | CAV | SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. | Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, Clark W. Barrett |
| 2017 | CAV | Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. | Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer |
| 2017 | MODELSWARD | Distributing Scenario-based Models: A Replicate-and-Project Approach. | Shlomi Steinberg, Joel Greenyer, Daniel Gritzner, David Harel, Guy Katz, Assaf Marron |
| 2017 | MODELSWARD | Efficient Distributed Execution of Multi-component Scenario-Based Models. | Shlomi Steinberg, Joel Greenyer, Daniel Gritzner, David Harel, Guy Katz, Assaf Marron |
| 2016 | FMCAD | Lazy proofs for DPLL(T)-based SMT solvers. | Guy Katz, Clark W. Barrett, Cesare Tinelli, Andrew Reynolds, Liana Hadarean |
| 2016 | MODELS | Scenario-Based Modeling and Synthesis for Reactive Systems with Dynamic System Structure in ScenarioTools. | Joel Greenyer, Daniel Gritzner, Guy Katz, Assaf Marron |
| 2016 | MODELS | Six (Im)possible Things before Breakfast: Building-Blocks and Design-Principles for Wise Computing. | Assaf Marron, Brit Arnon, Achiya Elyasaf, Michal Gordon, Guy Katz, Hadas Lapid, Rami Marelly, Dana Sherman, Smadar Szekely, Gera Weiss, David Harel |
| 2016 | MODELSWARD | An Initial Wise Development Environment for Behavioral Models. | David Harel, Guy Katz, Rami Marelly, Assaf Marron |
| 2015 | CONCUR | On the Succinctness of Idioms for Concurrent Programming. | David Harel, Guy Katz, Robby Lampert, Assaf Marron, Gera Weiss |
| 2015 | FMCAD | Theory-Aided Model Checking of Concurrent Transition Systems. | Guy Katz, Clark W. Barrett, David Harel |
| 2015 | MODELSWARD | The Effect of Concurrent Programming Idioms on Verification - A Position Paper. | David Harel, Guy Katz, Assaf Marron, Gera Weiss |
| 2013 | EMSOFT | On composing and proving the correctness of reactive behavior. | David Harel, Amir Kantor, Guy Katz, Assaf Marron, Lior Mizrahi, Gera Weiss |
| 2013 | LPAR | Relaxing Synchronization Constraints in Behavioral Programs. | David Harel, Amir Kantor, Guy Katz |
| 2013 | LPAR | On Module-Based Abstraction and Repair of Behavioral Programs. | Guy Katz |
| 2012 | ICECCS | Non-intrusive Repair of Reactive Programs. | David Harel, Guy Katz, Assaf Marron, Gera Weiss |
| 2011 | RecSys | Recommenders benchmark framework. | Aviram Dayan, Guy Katz, Naseem Biasdi, Lior Rokach, Bracha Shapira, Aykan Aydin, Roland Schwaiger, Radmila Fishel |