Manuscripts

On the (Un)Interpretability of Ensembles: A Computational Analysis
Shahaf Bassan, Guy Amir, Meirav Zehavi, and Guy Katz
preprint, 2024

Shield Synthesis for LTL Modulo Theories
Andoni Rodriguez, Guy Amir, Davide Corsi, Cesar Sanchez, and Guy Katz
preprint, 2024
[paper]

Analyzing Adversarial Inputs in Deep Reinforcement Learning
Davide Corsi, Guy Amir, Guy Katz, and Alessandro Farinelli
preprint, 2024
[paper]

Publications

Enforcing Specific Behaviours via Constrained DRL and Scenario-Based Programming
Davide Corsi, Raz Yerushalmi, Guy Amir, Alessandro Farinelli, David Harel, and Guy Katz
International Conference on Neural Information Processing (ICONIP), 2024
[paper]

Hard to Explain: On the Computational Hardness of In-Distribution Model Interpretation
Guy Amir*, Shahaf Bassan*, and Guy Katz
European Conference on Artificial Intelligence (ECAI), 2024
[paper]

Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates
Udayan Mandal, Guy Amir, Haoze Wu, Ieva Daukantas, Fletcher Newell, Umberto Ravaioli, Baoluo Meng, Michael Durling, Milan Ganai, Tobey Shim, Guy Katz, and Clark Barrett
Formal Methods in Computer-Aided Design (FMCAD), 2024
[paper] [code]

Verifying the Generalization of Deep Learning to Out-of-Distribution Domains
Guy Amir, Osher Maayan, Tom Zelazny, Guy Katz, and Michael Schapira
Journal of Automated Reasoning (JAR), 2024
[paper] [code]

Local vs. Global Interpretability: A Computational Complexity Perspective
Shahaf Bassan, Guy Amir, and Guy Katz
International Conference on Machine Learning (ICML), 2024 (Spotlight)
[paper]

Verification-Guided Shielding for Deep Reinforcement Learning
Davide Corsi*, Guy Amir*, Andoni Rodriguez, Cesar Sanchez, Guy Katz, and Roy Fox
Reinforcement Learning Conference (RLC), 2024
[paper]

Safe and Reliable Training of Learning-Based Aerospace Controllers
Udayan Mandal, Guy Amir, Haoze Wu, Ieva Daukantas, Fletcher Lee Newell, Umberto Ravaioli, Baoluo Meng, Michael Richard Durling, Kerianne Hobbs, Milan Ganai, Tobey Shim, Guy Katz, and Clark Barrett
Digital Avionics Systems Conference (DASC), 2024
[paper] [code]

Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
Haoze Wu, Omri Isac, Aleksandar Zeljić, Teruhiro Tagomori, Matthew Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Shahaf Bassan, Ori Lahav, Min Wu, Min Zhang, Ekaterina Komendantskaya, Guy Katz, and Clark Barrett
Computer Aided Verification (CAV), 2024
[paper] [code]

Formally Explaining Neural Networks within Reactive Systems
Shahaf Bassan*, Guy Amir*, Davide Corsi, Idan Refaeli, and Guy Katz
Formal Methods in Computer-Aided Design (FMCAD), 2023
[paper] [code]

Verifying Generalization in Deep Learning
Guy Amir*, Osher Maayan*, Tom Zelazny, Guy Katz, and Michael Schapira
Computer Aided Verification (CAV), 2023
[paper] [code]

Verifying Learning-Based Robotic Navigation Systems
Guy Amir*, Davide Corsi*, Raz Yerushalmi, Luca Marzari, David Harel, Alessandro Farinelli, and Guy Katz
Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2023
[paper] [code] [supplementary video]

Enhancing Deep Reinforcement Learning with Scenario-Based Modeling
Raz Yerushalmi, Guy Amir, Achiya Elyasaf, David Harel, Guy Katz, and Assaf Marron
Springer Nature Computer Science (SNCS), 2023
[paper]

veriFIRE: Verifying an Industrial, Learning-Based Wildfire Detection System
Guy Amir, Ziv Freund, Guy Katz, Elad Mandelbaum and Idan Refaeli
Formal Methods (FM), 2023
[paper]

Micro and Macroevolution of Sea Anemone Venom Phenotype
Edward G. Smith, Joachim M. Surm, Jason Macrander, Adi Simhi, Guy Amir, Maria Y. Sachkova, Magda Lewandowska, Adam M. Reitzel, and Yehu Moran
Nature Communications, 2023
[paper]

Verification-Aided Deep Ensemble Selection
Guy Amir, Tom Zelazny, Guy Katz, and Michael Schapira
Formal Methods in Computer-Aided Design (FMCAD), 2022
[paper] [code]

Neural Network Robustness as a Verification Property: A Principled Case Study
Marco Casadio, Ekaterina Komendantskaya, Mathew Daggitt, Wen Kokke, Guy Katz, Guy Amir, and Idan Refaeli
Computer Aided Verification (CAV), 2022
[paper] [code]

Scenario-Assisted Deep Reinforcement Learning
Raz Yerushalmi, Guy Amir, Achiya Elyasaf, David Harel, Guy Katz, and Assaf Marron
Model-Driven Engineering and Software Development (MODELSWARD), 2022
[paper]

Towards Scalable Verification of Deep Reinforcement Learning
Guy Amir, Michael Schapira, and Guy Katz
Formal Methods in Computer-Aided Design (FMCAD), 2021
[paper] [code]

An SMT-Based Approach for Verifying Binarized Neural Networks
Guy Amir, Haoze Wu, Clark Barrett, and Guy Katz
Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2021
[paper] [code]

Use and Perceptions of Multi-Monitor Workstations: A Natural Experiment
Guy Amir, Ayala Prusak, Tal Reiss, Nir Zabari, and Dror Feitelson
Software Engineering Research and Industrial Practice (SER & IP), 2021
[paper]

Thesis

Efficient and Scalable Verification of Safety-Critical Systems
Guy Amir
Ph.D. Thesis, The Hebrew University of Jerusalem, 2024

Patents

Diffusion-Based Handedness Classification for Touch-Based Input
Adam Hakim, Guy Amir, Aviv Slobodkin (Microsoft R&D)
U.S. Patent 11,947,758-B2
[patent]

Training Quantization-Aware AMAC Computing
Yehonathan Refael, Gilad Kirshenboim, Guy Amir, Doug Burger (Microsoft R&D)
Provisional Patent Pending, 2022
[patent]