About Me

I am a post-doctoral fellow at Stanford University, working with Prof. Clark Barrett. I completed my Ph.D (in 2015) and M.Sc. (in 2012) degrees at the Weizmann Institute of Science, Israel. My adviser there was Prof. David Harel. I completed my B.Sc. in 2007, at the Open University of Israel.

My research interests lie at the intersection between Software Engineering and Formal Methods, and in particular in the application of formal methods to lightweight parallel programming models. I am especially interested in SMT solving and its applications to software engineering. Recently I have also become interested in developing techniques for verifying the correctness of software generated using machine learning.

News: In spring 2018 I will be joining the School of Computer Science and Engineering at the Hebrew University of Jerusalem. I am looking for highly motivated graduate students and postdocs.

Contact Information

Guy Katz
Stanford University
Computer Science Department
353 Serra Mall, Gates building, Office 444
Stanford, CA 94305
Email: guyk at stanford dot edu

Publications

  1. D. Harel, G. Katz, R. Marelly and A. Marron. Wise Computing: Towards Endowing System Development with True Wisdom. IEEE Computer. To appear.

  2. J. Greenyer, D. Gritzner, T. Gutjahr, F. König, N. Glade, A. Marron and G. Katz. ScenarioTools - A Tool Suite for the Scenario-based Modeling and Analysis of Reactive Systems. Journal of Science of Computer Programming (J. SCP) 149, 2017, pp. 15-27. [PDF]

  3. D. Gopinath, G. Katz, C. Pasareanu and C. Barrett. DeepSafe: A Data-driven Approach for Checking Adversarial Robustness in Neural Networks. Arxiv Technical Report. October 2017. [link]

  4. N. Carlini, G. Katz, C. Barrett and D. Dill. Ground-Truth Adversarial Examples. Arxiv Technical Report. September 2017. [link]

  5. G. Katz, C. Barrett, D. Dill, K. Julian and M. Kochenderfer. Towards Proving the Adversarial Robustness of Deep Neural Networks. Proc. 1st Workshop on Formal Verification of Autonomous Vehicles (FVAV), pp. 19-26. Turin, Italy, September 2017. [PDF]

  6. G. Katz, C. Barrett, D. Dill, K. Julian and M. Kochenderfer. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. Proc. 29th Int. Conf. on Computer Aided Verification (CAV), pp. 97-117. Heidelberg, Germany, July 2017. [PDF] [Supplementary]

  7. B. Ekici, A. Mebsout, C. Tinelli, C. Keller, G. Katz, A. Reynolds and C. Barrett. SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. Proc. 29th Int. Conf. on Computer Aided Verification (CAV), pp. 126-133. Heidelberg, Germany, July 2017. [PDF]

  8. S. Steinberg, J. Greenyer, D. Gritzner, D. Harel, G. Katz and A. Marron. Distributing Scenario-Based Models: A Replicate-and-Project Approach. Proc. 5th Int. Conf. on Model-Driven Engineering and Software Development (MODELSWARD), pp. 182-195. Porto, Portugal, February 2017. [PDF]

  9. D. Harel, G. Katz, R. Marelly and A. Marron. First Steps Towards a Wise Development Environment for Behavioral Models. International Journal of Information System Modeling and Design (IJISMD), 7(3), 2016, pp. 1-22. [PDF]

  10. G. Katz, C. Barrett, C. Tinelli, A. Reynolds and L. Hadarean. Lazy Proofs for DPLL(T)-Based SMT Solvers. Proc. 16th Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), pp. 93-100. Mountain View, California, USA, October 2016. [PDF]

  11. J. Greenyer, D. Gritzner, G. Katz and A. Marron. Scenario-Based Modeling and Synthesis for Reactive Systems with Dynamic System Structure in ScenarioTools. 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]

  12. A. Marron, B. Arnon, A. Elyasaf, M. Gordon, G. Katz, H. Lapid, R. Marelly, D. Sherman, S. Szekely, G. Weiss and D. Harel. Six (Im)possible Things before Breakfast: Building-Blocks and Design-Principles for Wise Computing. 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]

  13. B. Ekici, G. Katz, C. Keller, A. Mebsout, A. Reynolds and C. Tinelli. Extending SMTCoq, a Certified Checker for SMT (Extended Abstract). Proc. 1st Int. Workshop on Hammers for Type Theories (HATT), pp. 21-29. Coimbra, Portugal, July 2016. [PDF]

  14. J. Greenyer, D. Gritzner, G. Katz, A. Marron, N. Glade, T. Gutjahr and F. König. Distributed Execution of Scenario-Based Specifications of Structurally Dynamic Cyber-Physical Systems. Proc. 3rd Int. Conf. on System-Integrated Intelligence: New Challenges for Product and Production Engineering (SYSINT), pp. 552-559. Paderborn, Germany, June 2016. [PDF]

  15. D. Harel, G. Katz, R. Marelly and A. Marron. An Initial Wise Development Environment for Behavioral Models. Proc. 4th Int. Conf. on Model-Driven Engineering and Software Development (MODELSWARD), pp. 600-612. Rome, Italy, February 2016. [PDF]

  16. G. Katz, C. Barrett and D. Harel. Theory-Aided Model Checking of Concurrent Transition Systems. Proc. 15th Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), pp. 81-88. Austin, Texas, USA, September 2015. [PDF] [Supplementary]

  17. D. Harel, G. Katz. R. Lampert, A. Marron and G. Weiss. On the Succinctness of Idioms for Concurrent Programming. Proc. 26th Int. Conf. on Concurrency Theory (CONCUR), pp. 85-99. Madrid, Spain, September 2015. [PDF] [Supplementary]

  18. D. Harel, A. Kantor, G. Katz. A. Marron, G. Weiss and G. Wiener. Towards Behavioral Programming in Distributed Architectures. Journal of Science of Computer Programming (J. SCP) 98, 2015, pp. 233-267. [PDF]

  19. D. Harel, G. Katz, A. Marron and G. Weiss. The Effect of Concurrent Programming Idioms on Verification. Proc. 3rd Int. Conf. on Model-Driven Engineering and Software Development (MODELSWARD), pp. 363-369. Angers, France, February 2015. [PDF]

  20. D. Harel and G. Katz. Scaling-Up Behavioral Programming: Steps from Basic Principles to Application Architectures. Proc. 4th SPLASH Workshop on Programming based on Actors, Agents and Decentralized Control (AGERE!), pp. 95-108. Portland, Oregon, USA, October 2014. [PDF] [Supplementary]

  21. D. Harel, G. Katz, A. Marron and G. Weiss. Non-Intrusive Repair of Safety and Liveness Violations in Reactive Programs. LNCS Transactions on Computational Collective Intelligence (TCCI) 16, 2014, pp. 1-33. [PDF]

  22. G. Katz. On Module-Based Abstraction and Repair of Behavioral Programs. Proc. 19th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), pp. 518-535. Stellenbosch, South Africa, December 2013. [PDF] [Supplementary]

  23. D. Harel, A. Kantor and G. Katz. Relaxing Synchronization Constraints in Behavioral Programs. Proc. 19th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), pp. 355-372. Stellenbosch, South Africa, December 2013. [PDF] [Supplementary]

  24. D. Harel, A. Kantor, G. Katz, A. Marron, L. Mizrahi and G. Weiss. On Composing and Proving the Correctness of Reactive Behavior. Proc. 13th Int. Conf. on Embedded Software (EMSOFT), pp. 1-10. Montréal, Canada, September 2013. [PDF] [Supplementary]

  25. D. Harel, G. Katz, A. Marron and G. Weiss. Non-Intrusive Repair of Reactive Programs. Proc. 17th IEEE Int. Conf. on Engineering of Complex Computer Systems (ICECCS), pp. 3-12. Paris, France, July 2012. [PDF]

Theses

  1. On Concurrency Idioms and their Effect on Program Analysis. Ph.D. Thesis. The Weizmann Institute of Science, Rehovot, Israel, December 2015. [PDF]

  2. Non-Intrusive Repair of Behavioral Programs. M.Sc. Thesis. The Weizmann Institute of Science, Rehovot, Israel, March 2012. [PDF]

Reluplex

Reluplex is an SMT-based method for verifying properties of deep neural networks.

For details about the method, see the following paper:
G. Katz, C. Barrett, D. Dill, K. Julian and M. Kochenderfer. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. Proc. 29th Int. Conf. on Computer Aided Verification (CAV). Heidelberg, Germany, July 2017. To appear. [PDF] [Supplementary]

The proof-of-concept implementation described in the paper is available [here].