Arie Gurfinkel

Dr. Arie Gurfinkel is a Professor in the Department of Electrical and Computer Engineering at the University of Waterloo, with a cross appointment at the Cheriton School of Computer Science.

His research focuses on addressing the challenges associated with developing, testing, and verifying complex computer systems. As computer systems become increasingly smaller, faster, more pervasive, mobile, and interconnected, ensuring their correctness is vital. Dr. Gurfinkel’s work aims to automate and improve the process of developing reliable systems.

Dr. Gurfinkel's research areas include Automated Program Analysis, Software Model Checking, Automated Reasoning, and Abstract Interpretation.

• Automated Program Analysis

• Software Model Checking

• Automated Reasoning

• Abstract Interpretation

• 2007, Doctorate Computer Science, University of Toronto, Canada

• CS 447 - Software Testing, Quality Assurance, and Maintenance
  • Taught in 2020, 2021, 2022
• CS 647 - Software Testing, Quality Assurance and Maintenance
  • Taught in 2020, 2021, 2022
• ECE 351 - Compilers
  • Taught in 2020, 2021, 2022, 2023, 2024
• ECE 453 - Software Testing, Quality Assurance, and Maintenance
  • Taught in 2020, 2021, 2022
• ECE 650 - Methods and Tools for Software Engineering
  • Taught in 2020, 2022, 2024
• ECE 653 - Software Testing, Quality Assurance and Maintenance
  • Taught in 2023

* Only courses taught in the past 5 years are displayed.

• Andreas Katis and Grigory Fedyukovich and Huajun Guo and Andrew Gacek and John Backes and Arie Gurfinkel and Michael W. Whalen, Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts, CoRR, , 2017

• Anvesh Komuravelli and Arie Gurfinkel and Sagar Chaki, SMT-based model checking for recursive programs, Formal Methods in System Design, 175, 2016

• Andreas Katis and Grigory Fedyukovich and Andrew Gacek and John D. Backes and Arie Gurfinkel and Michael W. Whalen, Synthesis from Assume-Guarantee Contracts using Skolemized Proofs of Realizability, CoRR, , 2016

• Sagar Chaki and Arie Gurfinkel and Ofer Strichman, Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation), Formal Methods in System Design, 287, 2015

• Arie Gurfinkel and Temesghen Kahsai and Jorge A. Navas, Algorithmic logic-based verification, {SIGLOG} News, 29, 2015

• Anvesh Komuravelli and Nikolaj Bj{\\o}rner and Arie Gurfinkel and Kenneth L. McMillan, Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays, CoRR, , 2015

• Anvesh Komuravelli and Arie Gurfinkel and Sagar Chaki, SMT-based Model Checking for Recursive Programs, CoRR, , 2014

• Hana Chockler and Arie Gurfinkel and Ofer Strichman, Beyond vacuity: towards the strongest passing formula, Formal Methods in System Design, 552, 2013

• Anvesh Komuravelli and Arie Gurfinkel and Sagar Chaki and Edmund M. Clarke, Automatic Abstraction in SMT-Based Unbounded Software Model Checking, CoRR, , 2013

• Naghmeh Ghafari and Arie Gurfinkel and Nils Klarlund and Richard J. Trefler, Reachability Problems in Piecewise {FIFO} Systems, {ACM} Trans. Comput. Log., , 2012