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]