Recommenders benchmark framework. - Aviram Dayan; Guy Katz; Naseem Biasdi; Lior Rokach; Bracha Shapira; Aykan Aydin; Roland Schwaiger; Radmila Fishel (RecSys, 2011)

Non-intrusive Repair of Reactive Programs. - David Harel; Guy Katz; Assaf Marron; Gera Weiss (ICECCS, 2012)

On composing and proving the correctness of reactive behavior. - David Harel; Amir Kantor; Guy Katz; Assaf Marron; Lior Mizrahi; Gera Weiss (EMSOFT, 2013)

Relaxing Synchronization Constraints in Behavioral Programs. - David Harel; Amir Kantor; Guy Katz (LPAR, 2013)

On Module-Based Abstraction and Repair of Behavioral Programs. - Guy Katz (LPAR, 2013)

Scaling-Up Behavioral Programming: Steps from Basic Principles to Application Architectures. - David Harel; Guy Katz (AGERE!@SPLASH, 2014)

Non-intrusive Repair of Safety and Liveness Violations in Reactive Programs. - David Harel; Guy Katz; Assaf Marron; Gera Weiss (Trans. Comput. Collect. Intell., 2014)

On the Succinctness of Idioms for Concurrent Programming. - David Harel; Guy Katz; Robby Lampert; Assaf Marron; Gera Weiss (CONCUR, 2015)

Theory-Aided Model Checking of Concurrent Transition Systems. - Guy Katz; Clark W. Barrett; David Harel (FMCAD, 2015)

The Effect of Concurrent Programming Idioms on Verification - A Position Paper. - David Harel; Guy Katz; Assaf Marron; Gera Weiss (MODELSWARD, 2015)

Wise Computing: Towards Endowing System Development with True Wisdom. - David Harel; Guy Katz; Rami Marelly; Assaf Marron (CoRR, 2015)

Towards behavioral programming in distributed architectures. - David Harel; Amir Kantor; Guy Katz; Assaf Marron; Gera Weiss; Guy Wiener (Sci. Comput. Program., 2015)

Lazy proofs for DPLL(T)-based SMT solvers. - Guy Katz; Clark W. Barrett; Cesare Tinelli; Andrew Reynolds 001; Liana Hadarean (FMCAD, 2016)

Scenario-Based Modeling and Synthesis for Reactive Systems with Dynamic System Structure in ScenarioTools. - Joel Greenyer; Daniel Gritzner; Guy Katz; Assaf Marron (D&P@MoDELS, 2016)

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 (D&P@MoDELS, 2016)

An Initial Wise Development Environment for Behavioral Models. - David Harel; Guy Katz; Rami Marelly; Assaf Marron (MODELSWARD, 2016)

Extending SMTCoq, a Certified Checker for SMT (Extended Abstract). - Burak Ekici; Guy Katz; Chantal Keller; Alain Mebsout; Andrew J. Reynolds; Cesare Tinelli (HaTT@IJCAR, 2016)

First Steps Towards a Wise Development Environment for Behavioral Models. - David Harel; Guy Katz; Rami Marelly; Assaf Marron (Int. J. Inf. Syst. Model. Des., 2016)

SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. - Burak Ekici; Alain Mebsout; Cesare Tinelli; Chantal Keller; Guy Katz; Andrew Reynolds 001; Clark W. Barrett (CAV (2), 2017)

Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. - Guy Katz; Clark W. Barrett; David L. Dill; Kyle Julian; Mykel J. Kochenderfer (CAV (1), 2017)

Distributing Scenario-based Models: A Replicate-and-Project Approach. - Shlomi Steinberg; Joel Greenyer; Daniel Gritzner; David Harel; Guy Katz; Assaf Marron (MODELSWARD, 2017)

Efficient Distributed Execution of Multi-component Scenario-Based Models. - Shlomi Steinberg; Joel Greenyer; Daniel Gritzner; David Harel; Guy Katz; Assaf Marron (MODELSWARD (Revised Selected Papers), 2017)

Towards Proving the Adversarial Robustness of Deep Neural Networks. - Guy Katz; Clark W. Barrett; David L. Dill; Kyle Julian; Mykel J. Kochenderfer (FVAV@iFM, 2017)

Ground-Truth Adversarial Examples. - Nicholas Carlini; Guy Katz; Clark W. Barrett; David L. Dill (CoRR, 2017)

DeepSafe: A Data-driven Approach for Checking Adversarial Robustness in Neural Networks. - Divya Gopinath; Guy Katz; Corina S. Pasareanu; Clark W. Barrett (CoRR, 2017)

ScenarioTools - A tool suite for the scenario-based modeling and analysis of reactive systems. - Joel Greenyer; Daniel Gritzner; Timo Gutjahr; Florian König; Nils Glade; Assaf Marron; Guy Katz (Sci. Comput. Program., 2017)

DeepSafe: A Data-Driven Approach for Assessing Robustness of Neural Networks. - Divya Gopinath; Guy Katz; Corina S. Pasareanu; Clark W. Barrett (ATVA, 2018)

Wise Computing: Toward Endowing System Development with Proactive Wisdom. - David Harel; Guy Katz; Rami Marelly; Assaf Marron (Computer, 2018)

Toward Scalable Verification for Safety-Critical Deep Networks. - Lindsey Kuper; Guy Katz; Justin Gottschlich; Kyle Julian; Clark W. Barrett; Mykel J. Kochenderfer (CoRR, 2018)

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 003; Shantanu Thakoor; Haoze Wu 001; Aleksandar Zeljic; David L. Dill; Mykel J. Kochenderfer; et al. (CAV (1), 2019)

Executing Scenario-Based Specification with Dynamic Generation of Rich Events. - David Harel; Guy Katz; Assaf Marron; Aviran Sadon; Gera Weiss (MODELSWARD (Revised Selected Papers), 2019)

On-the-Fly Construction of Composite Events in Scenario-Based Modeling using Constraint Solvers. - Guy Katz; Assaf Marron; Aviran Sadon; Gera Weiss (MODELSWARD, 2019)

Verifying Deep-RL-Driven Systems. - Yafim Kazak; Clark W. Barrett; Guy Katz; Michael Schapira (NetAI@SIGCOMM, 2019)

Simplifying Neural Networks with the Marabou Verification Engine. - Sumathi Gokulanathan; Alexander Feldsher; Adi Malca; Clark W. Barrett; Guy Katz (CoRR, 2019)

Verifying Recurrent Neural Networks Using Invariant Inference. - Yuval Jacoby; Clark W. Barrett; Guy Katz (ATVA, 2020)

An Abstraction-Based Framework for Neural Network Verification. - Yizhak Yisrael Elboher; Justin Gottschlich; Guy Katz (CAV (1), 2020)

Parallelization Techniques for Verifying Neural Networks. - Haoze Wu 001; Alex Ozdemir; Aleksandar Zeljic; Kyle Julian; Ahmed Irfan; Divya Gopinath; Sadjad Fouladi; Guy Katz; Corina S. Pasareanu; Clark W. Barrett (FMCAD, 2020)

Minimal Modifications of Deep Neural Networks using Verification. - Ben Goldberger; Guy Katz; Yossi Adi; Joseph Keshet (LPAR, 2020)

Guarded Deep Learning using Scenario-based Modeling. - Guy Katz (MODELSWARD, 2020)

Augmenting Deep Neural Networks with Scenario-Based Guard Rules. - Guy Katz (MODELSWARD (Revised Selected Papers), 2020)

Simplifying Neural Networks Using Formal Verification. - Sumathi Gokulanathan; Alexander Feldsher; Adi Malca; Clark W. Barrett; Guy Katz (NFM, 2020)

Towards Scalable Verification of Deep Reinforcement Learning. - Guy Amir; Michael Schapira; Guy Katz (FMCAD, 2021)

Pruning and Slicing Neural Networks using Formal Verification. - Ori Lahav 002; Guy Katz (FMCAD, 2021)

Towards Repairing Scenario-Based Models with Rich Events. - Guy Katz (MODELSWARD, 2021)

Verifying learning-augmented systems. - Tomer Eliyahu; Yafim Kazak; Guy Katz; Michael Schapira (SIGCOMM, 2021)

Invited Talk: Using SMT and Abstraction-Refinement for Neural Network Verification. - Guy Katz (SMT, 2021)

An SMT-Based Approach for Verifying Binarized Neural Networks. - Guy Amir; Haoze Wu 001; Clark W. Barrett; Guy Katz (TACAS (2), 2021)

Towards Scalable Verification of RL-Driven Systems. - Guy Amir; Michael Schapira; Guy Katz (CoRR, 2021)

An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks. - Matan Ostrovsky; Clark W. Barrett; Guy Katz (ATVA, 2022)

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 (CAV (1), 2022)

Minimal Multi-Layer Modifications of Deep Neural Networks. - Idan Refaeli; Guy Katz (NSV/FoMLAS@CAV, 2022)

Verification-Aided Deep Ensemble Selection. - Guy Amir; Tom Zelazny; Guy Katz; Michael Schapira (FMCAD, 2022)

Neural Network Verification with Proof Production. - Omri Isac; Clark W. Barrett; Min Zhang 002; Guy Katz (FMCAD, 2022)

On Optimizing Back-Substitution Methods for Neural Network Verification. - Tom Zelazny; Haoze Wu 001; Clark W. Barrett; Guy Katz (FMCAD, 2022)

RoMA: A Method for Neural Network Robustness Measurement and Assessment. - Natan Levy; Guy Katz (ICONIP (4), 2022)

Scenario-assisted Deep Reinforcement Learning. - Raz Yerushalmi; Guy Amir; Achiya Elyasaf; David Harel; Guy Katz; Assaf Marron (MODELSWARD, 2022)

Neural Network Verification Using Residual Reasoning. - Yizhak Yisrael Elboher; Elazar Cohen; Guy Katz (SEFM, 2022)

Efficient Neural Network Analysis with Sum-of-Infeasibilities. - Haoze Wu 001; Aleksandar Zeljic; Guy Katz; Clark W. Barrett (TACAS (1), 2022)

Verification-Aided Deep Ensemble Selection. - Guy Amir; Guy Katz; Michael Schapira (CoRR, 2022)

Constrained Reinforcement Learning for Robotics via Scenario-Based Programming. - Davide Corsi; Raz Yerushalmi; Guy Amir; Alessandro Farinelli; David Harel; Guy Katz (CoRR, 2022)

Towards Formal Approximated Minimal Explanations of Neural Networks. - Shahaf Bassan; Guy Katz (CoRR, 2022)

Efficiently Finding Adversarial Examples with DNN Preprocessing. - Avriti Chauhan; Mohammad Afzal; Hrishikesh Karmarkar; Yizhak Yisrael Elboher; Kumar Madhukar; Guy Katz (CoRR, 2022)

BBReach: Tight and Scalable Black-Box Reachability Analysis of Deep Reinforcement Learning Systems. - Jiaxu Tian; Dapeng Zhi; Si Liu 003; Peixin Wang; Guy Katz; Min Zhang 002 (CoRR, 2022)

Artifact for Paper Efficient Neural Network Analysis with Sum-of-Infeasibilities. - Haoze Wu 001; Aleksandar Zeljic; Guy Katz; Clark W. Barrett (Zenodo, 2022)

Reluplex: a calculus for reasoning about deep neural networks. - Guy Katz; Clark W. Barrett; David L. Dill; Kyle Julian; Mykel J. Kochenderfer (Formal Methods Syst. Des., 2022)

Verifying Generalization in Deep Learning. - Guy Amir; Osher Maayan; Tom Zelazny; Guy Katz; Michael Schapira (CAV (2), 2023)

DNN Verification, Reachability, and the Exponential Function Problem. - Omri Isac; Yoni Zohar; Clark W. Barrett; Guy Katz (CONCUR, 2023)

veriFIRE: Verifying an Industrial, Learning-Based Wildfire Detection System. - Guy Amir; Ziv Freund; Guy Katz; Elad Mandelbaum; Idan Refaeli (FM, 2023)

Formally Explaining Neural Networks within Reactive Systems. - Shahaf Bassan; Guy Amir; Davide Corsi; Idan Refaeli; Guy Katz (FMCAD, 2023)

DelBugV: Delta-Debugging Neural Network Verifiers. - Raya Elsaleh; Guy Katz (FMCAD, 2023)

Towards a Certified Proof Checker for Deep Neural Network Verification. - Remi Desmartin; Omri Isac; Grant O. Passmore; Kathrin Stark; Ekaterina Komendantskaya; Guy Katz (LOPSTR, 2023)

Tighter Abstract Queries in Neural Network Verification. - Elazar Cohen; Yizhak Yisrael Elboher; Clark W. Barrett; Guy Katz (LPAR, 2023)

Enhancing Deep Learning with Scenario-Based Override Rules: A Case Study. - Adiel Ashrov; Guy Katz (MODELSWARD, 2023)

Verifying Learning-Based Robotic Navigation Systems. - Guy Amir; Davide Corsi; Raz Yerushalmi; Luca Marzari; David Harel; Alessandro Farinelli; Guy Katz (TACAS (1), 2023)

Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks. - Shahaf Bassan; Guy Katz (TACAS (1), 2023)

OccRob: Efficient SMT-Based Occlusion Robustness Verification of Deep Neural Networks. - Xingwu Guo; Ziwei Zhou; Yueling Zhang; Guy Katz; Min Zhang 002 (TACAS (1), 2023)

gRoMA: A Tool for Measuring the Global Robustness of Deep Neural Networks. - Natan Levy; Raz Yerushalmi; Guy Katz (AISoLA, 2023)

gRoMA: a Tool for Measuring Deep Neural Networks Global Robustness. - Natan Levy; Raz Yerushalmi; Guy Katz (CoRR, 2023)

On Reducing Undesirable Behavior in Deep Reinforcement Learning Models. - Ophir M. Carmel; Guy Katz (CoRR, 2023)

Enhancing Deep Reinforcement Learning with Scenario-Based Modeling. - Raz Yerushalmi; Guy Amir; Achiya Elyasaf; David Harel; Guy Katz; Assaf Marron (SN Comput. Sci., 2023)

Global optimization of objective functions represented by ReLU networks. - Christopher A. Strong; Haoze Wu 001; Aleksandar Zeljic; Kyle D. Julian; Guy Katz; Clark W. Barrett; Mykel J. Kochenderfer (Mach. Learn., 2023)

Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. - Haoze Wu 001; Omri Isac; Aleksandar Zeljic; Teruhiro Tagomori; Matthew L. Daggitt; Wen Kokke; Idan Refaeli; Guy Amir; Kyle Julian; Shahaf Bassan; Pei Huang 002; Ori Lahav 002; et al. (CAV (2), 2024)

Hard to Explain: On the Computational Hardness of In-Distribution Model Interpretation. - Guy Amir; Shahaf Bassan; Guy Katz (ECAI, 2024)

Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates. - Udayan Mandal; Guy Amir; Haoze Wu 001; Ieva Daukantas; Fletcher Lee Newell; Umberto J. Ravaioli; Baoluo Meng; Michael Durling; Milan Ganai; Tobey Shim; Guy Katz; Clark W. Barrett (FMCAD, 2024)

Local vs. Global Interpretability: A Computational Complexity Perspective. - Shahaf Bassan; Guy Amir; Guy Katz (ICML, 2024)

Enforcing Specific Behaviours via Constrained DRL and Scenario-Based Programming. - Davide Corsi; Raz Yerushalmi; Guy Amir; Alessandro Farinelli; David Harel; Guy Katz (ICONIP (11), 2024)

Learning DNN Abstractions using Gradient Descent. - Diganta Mukhopadhyay; Sanaa Siddiqui; Hrishikesh Karmarkar; Kumar Madhukar; Guy Katz (ASE, 2024)

On Augmenting Scenario-Based Modeling with Generative AI. - David Harel; Guy Katz; Assaf Marron; Smadar Szekely (MODELSWARD, 2024)

Verification-Guided Shielding for Deep Reinforcement Learning. - Davide Corsi; Guy Amir; Andoni Rodríguez; Guy Katz; César Sánchez 001; Roy Fox (RLJ, 2024)

Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training. - Jiaxu Tian; Dapeng Zhi; Si Liu 003; Peixin Wang; Guy Katz; Min Zhang 002 (VMCAI (2), 2024)

DEM: A Method for Certifying Deep Neural Network Classifier Outputs in Aerospace. - Guy Katz; Natan Levy; Idan Refaeli; Raz Yerushalmi (CoRR, 2024)

Robustness Assessment of a Runway Object Classifier for Safe Aircraft Taxiing. - Yizhak Yisrael Elboher; Raya Elsaleh; Omri Isac; Mélanie Ducoffe; Audrey Galametz; Guillaume Povéda; Ryma Boumazouza; Noémie Cohen; Guy Katz (CoRR, 2024)

Analyzing Adversarial Inputs in Deep Reinforcement Learning. - Davide Corsi; Guy Amir; Guy Katz; Alessandro Farinelli (CoRR, 2024)

NLP Verification: Towards a General Methodology for Certifying Robustness. - Marco Casadio; Tanvi Dinkar; Ekaterina Komendantskaya; Luca Arnaboldi 001; Omri Isac; Matthew L. Daggitt; Guy Katz; Verena Rieser; Oliver Lemon (CoRR, 2024)

A Certified Proof Checker for Deep Neural Network Verification. - Remi Desmartin; Omri Isac; Ekaterina Komendantskaya; Kathrin Stark; Grant O. Passmore; Guy Katz (CoRR, 2024)

Formal Verification of Object Detection. - Avraham Raviv; Yizhak Yisrael Elboher; Michelle Aluf-Medina; Yael Leibovich Weiss; Omer Cohen; Roy Assa; Guy Katz; Hillel Kugler (CoRR, 2024)

Safe and Reliable Training of Learning-Based Aerospace Controllers. - Udayan Mandal; Guy Amir; Haoze Wu 001; Ieva Daukantas; Fletcher Lee Newell; Umberto J. Ravaioli; Baoluo Meng; Michael Durling; Kerianne Hobbs; Milan Ganai; Tobey Shim; Guy Katz; et al. (CoRR, 2024)

On Reducing Undesirable Behavior in Deep-Reinforcement-Learning-Based Software. - Ophir M. Carmel; Guy Katz (Proc. ACM Softw. Eng., 2024)

On applying residual reasoning within neural network verification. - Yizhak Yisrael Elboher; Elazar Cohen; Guy Katz (Softw. Syst. Model., 2024)

Verifying the Generalization of Deep Learning to Out-of-Distribution Domains. - Guy Amir; Osher Maayan; Tom Zelazny; Guy Katz; Michael Schapira (J. Autom. Reason., 2024)

Shield Synthesis for LTL Modulo Theories. - Andoni Rodríguez; Guy Amir; Davide Corsi; César Sánchez 001; Guy Katz (AAAI, 2025)

On the Computational Tractability of the (Many) Shapley Values. - Reda Marzouk; Shahaf Bassan; Guy Katz; Colin de la Higuera (AISTATS, 2025)

A Study on the Comprehensibility of Behavioral Programming Variants. - Adiel Ashrov; Arnon Sturm; Achiya Elyasaf; Guy Katz (ENASE, 2025)

Exploring and Evaluating Interplays of BPpy with Deep Reinforcement Learning and Formal Methods. - Tom Yaacov; Gera Weiss; Adiel Ashrov; Guy Katz; Jules Zisser (ENASE, 2025)

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 001 (ESOP (1), 2025)

Proof-Driven Clause Learning in Neural Network Verification. - Omri Isac; Idan Refaeli; Haoze Wu 001; Clark W. Barrett; Guy Katz (CoRR, 2025)

Towards Robust LLMs: an Adversarial Robustness Measurement Framework. - Natan Levy; Adiel Ashrov; Guy Katz (CoRR, 2025)

What makes an Ensemble (Un) Interpretable? - Shahaf Bassan; Guy Amir; Meirav Zehavi; Guy Katz (CoRR, 2025)

Explaining, Fast and Slow: Abstraction and Refinement of Provable Explanations. - Shahaf Bassan; Yizhak Yisrael Elboher; Tobias Ladner; Matthias Althoff; Guy Katz (CoRR, 2025)

Abstraction-Based Proof Production in Formal Verification of Neural Networks. - Yizhak Yisrael Elboher; Omri Isac; Guy Katz; Tobias Ladner; Haoze Wu 001 (CoRR, 2025)