Department of Computer Science
35 Olden Street, Princeton, NJ 08540-5233
Office: 220 Computer Science
Phone: +1 609-258-8017
Fax: +1 609-258-1771
Email: aartig (at) cs (dot) princeton (dot) edu
My research interests are in formal verification of systems, program analysis, and automatic decision procedures for logics. I am currently serving on the Steering Committee of the International Conference on Computer Aided Verification (CAV). I received a PhD in Computer Science from Carnegie Mellon University.
Before joining the CS department at Princeton, I was at NEC Labs America where I led research in systems analysis and verification. At NEC, my group and I designed techniques for verifying programs, and helped in their successful deployment on large industrial software projects.
- Foundations: formal methods, model checking, program analysis, automated synthesis, SAT/SMT solvers
- Applications: verification of software, hardware, networks, distributed systems
- ACM Conference on Programming Language Design and Implementation (PLDI) 2023: Distinguished Paper Award
- IEEE International Conference on Network Protocols (ICNP) 2022: Best Paper Award
- Design, Automation, and Test in Europe (DATE) 2021: Best Paper Award (Track D)
- ACM Transactions on Design Automation of Electronic Systems 2020: Best Paper Award
- IEEE Micro Top Pick 2018: Honorable Mention (also nominated for Best Paper at MICRO-51 conference)
- ACM Fellow: 2017 (for contributions to system analysis and verification techniques and their transfer to industrial practice)
Recent Invited Talks
- Invited Keynote at the Federated Logic Conferences (FLoC), August 2022: SMT-based Verification of Distributed Network Control Planes.
- Bryant Discoveries Day at FLoC, August 2022: BDD (R)evolution: Extending Across Generations.
- Invited talk at the Indian Association for Research in Computing Science (IARCS) Verification Series, June 2022: Formal Verification of Distributed Network Control Planes.
- Invited talk at the Cambridge Isaac Newton Institute Workshop on Verified Software: From Theory to Practice, May 2021: Abstract Interpretation of Distributed Network Control Planes.
- Invited Keynote at the 23rd International Conference on Theory and Applications of Satisfiability Testing (SAT), July 2020: With a little help from structured friends
- Invited talk at the 11th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), July 2019: Verifying Network Control Planes
- Invited talk, The Best of Model Checking: Workshop in honor of Orna Grumberg, July 2019: Abstractions due to Symmetry in Network Control Planes
- Invited Tutorial at the Third SAT+SMT School (India), December 2018: Automated Verification of Programs and Networks using SAT/SMT
- SyLVer: Synthesis, Learning, and Verification
- Instruction Level Abstraction (ILA): in collaboration with Sharad Malik group
- Network Verification: in collaboration with Dave Walker and Ryan Beckett
- Yueling Zhang (ECNU, China): September 2017 -- June 2018