## PUBLICATIONS

65.

veriFIRE: Verifying an Industrial, Learning-Based Wildfire Detection System

G. Amir, Z. Freund, G. Katz, E. Mandelbaum and I. Refaeli

Proc. 25th Int. Symposium on Formal Methods (FM)

Lubeck, Germany, March 2023

To appear

# 2023

48.

Global Optimization of Objective Functions Represented by ReLU Networks

C. Strong, H. Wu, A. Zeljic, K. Julian, G. Katz, C. Barrett and M. Kochenderfer

Journal of Machine Learning, 2021, pp. 1-28

[PDF]

47.

Pruning and Slicing Neural Networks using Formal Verification

O. Lahav and G. Katz

Proc. 21st Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), pp. 183-192

New Haven, Connecticut, USA, October 2021

[PDF]

46.

Towards Scalable Verification of Deep Reinforcement Learning

G. Amir, M. Schapira and G. Katz

Proc. 21st Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), pp. 193-203

New Haven, Connecticut, USA, October 2021

[PDF]

45.

Verifying Learning-Augmented Systems

T. Eliyahu, Y. Kazak, G. Katz and M. Schapira

Proc. Annual Conf. of the ACM Special Interest Group on Data Communication on the Applications, Technologies, Architectures, and Protocols for Computer Communication (SIGCOMM), pp. 305-318

Virtual event, August 2021

[PDF]

44.

Reluplex: a Calculus for Reasoning about Deep Neural Networks

G. Katz, C. Barrett, D. Dill, K. Julian and M. Kochenderfer

Formal Methods in System Design (FMSD), 2021

[PDF]

43.

Towards Combining Deep Learning, Verification, and Scenario-Based Programming

G. Katz and A. Elyasaf

Proc. 1st Workshop on Verification of Autonomous and Robotic Systems (VARS), pp. 1-3

Virtual event, May 2021

[PDF]

42.

An SMT-Based Approach for Verifying Binarized Neural Networks

G. Amir, H. Wu, C. Barrett and G. Katz

Proc. 27th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 203-222

Luxembourg, Luxembourg, April 2021

[PDF]

41.

Augmenting Deep Neural Networks with Scenario-Based Guard Rules

G. Katz

Communications in Computer and Information Science (CCIS) 1361, 2021, pp. 147-172

[PDF]

40.

Towards Repairing Scenario-Based Models with Rich Events

G. Katz

Proc. 9th Int. Conf. on Model-Driven Engineering and Software Development (MODELSWARD), pp. 362-372

Vienna, Austria, February 2021

[PDF]

# 2021

39.

Verifying Recurrent Neural Networks using Invariant Inference

Y. Jacoby, C. Barrett and G. Katz

Proc. 18th. Int. Symposium on Automated Technology for Verification and Analysis (ATVA), pp. 57-74

Hanoi, Vietnam, October 2020

[PDF]

38.

Parallelization Techniques for Verifying Neural Networks

H. Wu, A. Ozdemir, A. Zeljic, A. Irfan, K. Julian, D. Gopinath, S. Fouladi, G. Katz, C. Pasareanu and C. Barrett

Proc. 20th Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), pp. 128-137

Haifa, Israel, September 2020

[PDF]

37.

An Abstraction-Based Framework for Neural Network Verification

Y. Elboher, J. Gottschlich and G. Katz

Proc. 32nd Int. Conf. on Computer Aided Verification (CAV), pp. 43-65

Los Angeles, California, USA, July 2020

[PDF]

36.

Minimal Modifications of Deep Neural Networks using Verification

B. Goldberger, Y. Adi, J. Keshet and G. Katz

Proc. 23rd Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), pp. 260-278

Alicante, Spain, May 2020

[PDF]

35.

Simplifying Neural Networks using Formal Verification

S. Gokulanathan, A. Feldsher, A. Malca, C. Barrett and G. Katz

Proc. 12th NASA Formal Methods Symposium (NFM), pp. 85-93

Moffett Field, California, USA, May 2020

[PDF]

34.

Guarded Deep Learning using Scenario-Based Modeling

G. Katz

Proc. 8th Int. Conf. on Model-Driven Engineering and Software Development (MODELSWARD), pp. 126-136

Valletta, Malta, February 2020

[PDF]

33.

Executing Scenario-Based Specification with Dynamic Generation of Rich Events

D. Harel, G. Katz, A. Marron, A. Sadon and G. Weiss

Communications in Computer and Information Science (CCIS) 1161, 2020, pp. 246–274

[PDF]

# 2020

32.

Verifying Deep-RL-Driven Systems

Y. Kazak, C. Barrett, G. Katz and M. Schapira

Proc. 1st ACM SIGCOMM Workshop on Network Meets AI & ML (NetAI), pp. 83-89

Beijing, China, August 2019

[PDF]

31.

The Marabou Framework for Verification and Analysis of Deep Neural Networks

G. Katz, D. Huang, D. Ibeling, K. Julian, C. Lazarus, R. Lim, P. Shah, S. Thakoor, H. Wu, A. Zeljic, D. Dill, M. Kochenderfer and C. Barrett

Proc. 31st Int. Conf. on Computer Aided Verification (CAV), pp. 443-452

New York City, New York, USA, July 2019

[PDF]

30.

On-the-Fly Construction of Composite Events in Scenario-Based Modeling Using Constraint Solvers

G. Katz, A. Marron, A. Sadon and G. Weiss

Proc. 7th Int. Conf. on Model-Driven Engineering and Software Development (MODELSWARD), pp. 143-156

Prague, Czech Republic, February 2019

[PDF]

# 2019

64.

BBReach: Tight and Scalable Black-Box Reachability Analysis of Deep Reinforcement Learning Systems

J. Tian, D. Zhi, S. Liu, P. Wang, G. Katz, and M. Zhang

Arxiv Technical Report, November 2022

[Arxiv]

63.

RoMA: A Method for Neural Network Robustness Measurement and Assessment

N. Levy and G. Katz

Proc. 29th Int. Conf. on Neural Information Processing (ICONIP)

New Delhi, India, November 2022

To appear

62.

Efficiently Finding Adversarial Examples with DNN Preprocessing

A. Chauhan, and M. Afzal, and H. Karmarkar, Y. Elboher, and K. Madhukar and G. Katz

Arxiv Technical Report, November 2022

[Arxiv]

61.

Towards Formal Approximated Minimal Explanations of Neural Networks

S. Bassan and G. Katz

Arxiv Technical Report, October 2022

[Arxiv]

60.

Tighter Abstract Queries in Neural Network Verification

E. Cohen, Y. Elboher, C. Barrett and G. Katz

Arxiv Technical Report, October 2022

[Arxiv]

59.

An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks

M. Ostrovsky, C. Barrett and G. Katz

Proc. 20th. Int. Symposium on Automated Technology for Verification and Analysis (ATVA), pp.391-396

Beijing, China, October 2022

[PDF]

58.

On Reducing Over-Approximation Errors for Neural Network Verification

T. Zelazny, H. Wu, C. Barrett and G. Katz

Proc. 22nd Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), pp. 17-26

Trento, Italy, October 2022

[PDF]

57.

Neural Network Verification with Proof Production

O. Isac, C. Barrett, M. Zhang and G. Katz

Proc. 22nd Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), pp. 38-48

Trento, Italy, October 2022

[PDF]

56.

Verification-Aided Deep Ensemble Selection

G. Amir, G. Katz and M. Schapira

Proc. 22nd Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), pp. 27-37

Trento, Italy, October 2022

[PDF]

55.

Neural Network Verification using Residual Reasoning

Y. Elboher, E. Cohen and G. Katz

Proc. 20th Int. Conf. on Software Engineering and Formal Methods (SEFM), pp 173-189

Berlin, Germany, September 2022

[PDF]

54.

Neural Network Robustness as a Verification Property: A Principled Case Study

M. Casadio, E. Komendantskaya, M. Daggitt, W. Kokke, G. Katz, G. Amir and I. Refaeli

Proc. 34th Int. Conf. on Computer Aided Verification (CAV), pp. 219-231

Haifa, Israel, August 2022

[PDF]

53.

Minimal Multi-Layer Modifications of Deep Neural Networks

I. Refaeli and G. Katz

Proc. 5th Workshop on Formal Methods for ML-Enabled Autonomous Systems (FoMLAS)

Haifa, Israel, July 2022

To appear

52.

Constrained Reinforcement Learning for Robotics via Scenario-Based Programming

D. Corsi, R. Yerushalmi, G. Amir, A. Farinelli, D. Harel and G. Katz

Arxiv Technical Report, June 2022

[Arxiv]

51.

Verifying Learning-Based Robotic Navigation Systems

G. Amir, D. Corsi, R. Yerushalmi, L. Marzari, D. Harel, A. Farinelli and G. Katz

Arxiv Technical Report, May 2022

[Arxiv]

50.

Efficient Neural Network Analysis with Sum-of-Infeasibilities

H. Wu, A. Zeljic, G. Katz and C. Barrett

Proc. 28th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS),

pp. 143-163

Munich, Germany, April 2022

[PDF]

49.

Scenario-Assisted Deep Reinforcement Learning

R. Yerushalmi, G. Amir, A. Elyasaf, D. Harel, G. Katz and A. Marron

Proc. 10th Int. Conf. on Model-Driven Engineering and Software Development (MODELSWARD), pp. 310-319

Virtual event, February 2022

[PDF]

# 2022

29.

Efficient Distributed Execution of Multi-Component Scenario-Based Models

S. Steinberg, J. Greenyer, D. Gritzner, D. Harel, G. Katz and A. Marron

Communications in Computer and Information Science (CCIS) 880, 2018, pp. 449-483

[PDF]

28.

DeepSafe: A Data-Driven Approach for Assessing Robustness of Neural Networks

D. Gopinath, G. Katz, C. Pasareanu and C. Barrett

Proc. 16th. Int. Symposium on Automated Technology for Verification and Analysis (ATVA), pp. 3-19

Los Angeles, California, USA, October 2018

[PDF]

27.

Wise Computing: Toward Endowing System Development with Proactive Wisdom

D. Harel, G. Katz, R. Marelly and A. Marron

IEEE Computer 51(2), 2018, pp. 14-26

[PDF]

26.

Toward Scalable Verification for Safety-Critical Deep Networks

L. Kuper, G. Katz, J. Gottschlich, K. Julian, C. Barrett and M. Kochenderfer

Arxiv Technical Report, January 2018

[Arxiv]

# 2018

25.

ScenarioTools - A Tool Suite for the Scenario-based Modeling and Analysis of Reactive Systems

J. Greenyer, D. Gritzner, T. Gutjahr, F. König, N. Glade, A. Marron and G. Katz

Journal of Science of Computer Programming (J. SCP) 149, 2017, pp. 15-27

[PDF]

24.

Provably Minimally-Distorted Adversarial Examples

N. Carlini, G. Katz, C. Barrett and D. Dill

Arxiv Technical Report, September 2017

[Arxiv]

23.

Towards Proving the Adversarial Robustness of Deep Neural Networks

G. Katz, C. Barrett, D. Dill, K. Julian and M. Kochenderfer

Proc. 1st Workshop on Formal Verification of Autonomous Vehicles (FVAV), pp. 19-26

Turin, Italy, September 2017

[PDF]

22.

Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks

G. Katz, C. Barrett, D. Dill, K. Julian and M. Kochenderfer

Proc. 29th Int. Conf. on Computer Aided Verification (CAV), pp. 97-117

Heidelberg, Germany, July 2017

[PDF]

21.

SMTCoq: A Plug-In for Integrating SMT Solvers into Coq

B. Ekici, A. Mebsout, C. Tinelli, C. Keller, G. Katz, A. Reynolds and C. Barrett

Proc. 29th Int. Conf. on Computer Aided Verification (CAV), pp. 126-133

Heidelberg, Germany, July 2017

[PDF]

20.

Distributing Scenario-Based Models: A Replicate-and-Project Approach

S. Steinberg, J. Greenyer, D. Gritzner, D. Harel, G. Katz and A. Marron

Proc. 5th Int. Conf. on Model-Driven Engineering and Software Development (MODELSWARD), pp. 182-195

Porto, Portugal, February 2017

[PDF]

# 2017

19.

First Steps Towards a Wise Development Environment for Behavioral Models

D. Harel, G. Katz, R. Marelly and A. Marron

International Journal of Information System Modeling and Design (IJISMD), 7(3), 2016, pp. 1-22

[PDF]

18.

Lazy Proofs for DPLL(T)-Based SMT Solvers

G. Katz, C. Barrett, C. Tinelli, A. Reynolds and L. Hadarean

Proc. 16th Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), pp. 93-100

Mountain View, California, USA, October 2016

[PDF]

17.

Scenario-Based Modeling and Synthesis for Reactive Systems with Dynamic System Structure in ScenarioTools

J. Greenyer, D. Gritzner, G. Katz and A. Marron

Proc. 19th ACM/IEEE Int. Conf. on Model Driven Engineering Languages and Systems (MODELS), Demo Session, pp. 16-23

Saint-Malo, France, October 2016

[PDF]

16.

Six (Im)possible Things before Breakfast: Building-Blocks and Design-Principles for Wise Computing

A. Marron, B. Arnon, A. Elyasaf, M. Gordon, G. Katz, H. Lapid, R. Marelly, D. Sherman, S. Szekely, G. Weiss and D. Harel

Proc. 19th ACM/IEEE Int. Conf. on Model Driven Engineering Languages and Systems (MODELS), Poster Session, pp. 94-100

Saint-Malo, France, October 2016

[PDF]

15.

Extending SMTCoq, a Certified Checker for SMT (Extended Abstract)

B. Ekici, G. Katz, C. Keller, A. Mebsout, A. Reynolds and C. Tinelli

Proc. 1st Int. Workshop on Hammers for Type Theories (HATT), pp. 21-29

Coimbra, Portugal, July 2016

[PDF]

14.

Distributed Execution of Scenario-Based Specifications of Structurally Dynamic Cyber-Physical Systems

J. Greenyer, D. Gritzner, G. Katz, A. Marron, N. Glade, T. Gutjahr and F. König

Proc. 3rd Int. Conf. on System-Integrated Intelligence: New Challenges for Product and Production Engineering (SYSINT), pp. 552-559

Paderborn, Germany, June 2016

[PDF]

13.

An Initial Wise Development Environment for Behavioral Models

D. Harel, G. Katz, R. Marelly and A. Marron

Proc. 4th Int. Conf. on Model-Driven Engineering and Software Development (MODELSWARD), pp. 600-612

Rome, Italy, February 2016

[PDF]

# 2016

12.

Theory-Aided Model Checking of Concurrent Transition Systems

G. Katz, C. Barrett and D. Harel

Proc. 15th Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), pp. 81-88

Austin, Texas, USA, September 2015

11.

On Concurrency Idioms and their Effect on Program Analysis

G. Katz

Ph.D. Thesis, The Weizmann Institute of Science

Rehovot, Israel, December 2015

[PDF]

10.

On the Succinctness of Idioms for Concurrent Programming

D. Harel, G. Katz, R. Lampert, A. Marron and G. Weiss

Proc. 26th Int. Conf. on Concurrency Theory (CONCUR), pp. 85-99

Madrid, Spain, September 2015

9.

Towards Behavioral Programming in Distributed Architectures

D. Harel, A. Kantor, G. Katz, A. Marron, G. Weiss and G. Wiener

Journal of Science of Computer Programming (J. SCP) 98, 2015, pp. 233-267

[PDF]

8.

The Effect of Concurrent Programming Idioms on Verification

D. Harel, G. Katz, A. Marron and G. Weiss

Proc. 3rd Int. Conf. on Model-Driven Engineering and Software Development (MODELSWARD), pp. 363-369

Angers, France, February 2015

[PDF]

# 2015

7.

Scaling-Up Behavioral Programming: Steps from Basic Principles to Application Architectures

D. Harel and G. Katz

Proc. 4th SPLASH Workshop on Programming based on Actors, Agents and Decentralized Control (AGERE!), pp. 95-108

Portland, Oregon, USA, October 2014

6.

Non-Intrusive Repair of Safety and Liveness Violations in Reactive Programs

D. Harel, G. Katz, A. Marron and G. Weiss

LNCS Transactions on Computational Collective Intelligence (TCCI) 16, 2014, pp. 1-33

[PDF]

# 2014

5.

On Module-Based Abstraction and Repair of Behavioral Programs

G. Katz

Proc. 19th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), pp. 518-535

Stellenbosch, South Africa, December 2013

4.

Relaxing Synchronization Constraints in Behavioral Programs

D. Harel, A. Kantor and G. Katz

Proc. 19th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), pp. 355-372

Stellenbosch, South Africa, December 2013

3.

On Composing and Proving the Correctness of Reactive Behavior

D. Harel, A. Kantor, G. Katz, A. Marron, L. Mizrahi and G. Weiss

Proc. 13th Int. Conf. on Embedded Software (EMSOFT), pp. 1-10

Montréal, Canada, September 2013

# 2013

2.

Non-Intrusive Repair of Reactive Programs

D. Harel, G. Katz, A. Marron and G. Weiss

Proc. 17th IEEE Int. Conf. on Engineering of Complex Computer Systems (ICECCS), pp. 3-12

Paris, France, July 2012

[PDF]

1.

Non-Intrusive Repair of Behavioral Programs

G. Katz

M.Sc. Thesis, The Weizmann Institute of Science

Rehovot, Israel, March 2012

[PDF]