My research and teaching interests are in programming languages, automated reasoning, and software engineering. The role, scale, and nature of software that affects our lives is ever changing. The goal of my research is to develop tools and techniques to improve the reliability and performance of software systems. My current research aims to develop explainable and scalable program analysis—tools that I would have wanted while I was working in the industry. Furthermore, the nature of software engineering is changing, spurred by the adoption of practical machine-learning systems; this change requires exploring fundamentally new ways of developing, verifying, and deploying software. A description of current projects can be found here.

I am looking for highly-motivated Ph.D. students to work on challenging research problems in the areas of machine learning, programming languages, and automated reasoning; if interested, please send me an email with a description of your research interests and your CV.

Recent News

08/2020 Paper accepted to SPLASH Onward! 2020.
07/2020 Two papers accepted to SAS 2020.
06/2020 Sung Kook Kim is the Runner Up for the GGCS 2020 Best Graduate Researcher Award
06/2020 Awarded Facebook Probability and Programming Research Award 2020
04/2020 Paper accepted to IFIP Networking 2020.
01/2020 Matthew Sotoudeh awarded second place in POPL 2020 Student Research Competition
01/2020 Our research on parallel abstract interpretation is used in two open-source abstract interpreters: NASA IKOS and Facebook SPARTA.
10/2019 Paper accepted to POPL 2020.
09/2019 Paper accepted to NeurIPS 2019 Workshop on Safety and Robustness in Decision Making
09/2019 Talk at Probability and Programming Workshop 2019
09/2019 Paper accepted to NeurIPS 2019
07/2019 Paper accepted to Globecom 2019
06/2019 Paper accepted to SMT 2019
05/2019 Paper accepted to ESEC/FSE 2019
05/2019 Awarded Facebook Probability and Programming Research Award 2019
11/2018 Daniel DeFreez awarded first place in ESEC/FSE 2018 Student Research Competition (SRC)
10/2018 Awarded Facebook Testing and Verification (TAV) Research Award 2018
07/2018 Paper accepted to ESEC/FSE 2018
06/2018 Awarded DECOR 2018 Research Award
03/2018  Poster paper accepted to ICSE 2018

Publications

Google Scholar / DBLP

  1. Analogy-Making as a Core Primitive in the Software Engineering Toolbox
    2020 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Onward!, 2020
    To appear
    Details
  2. Memory-efficient Fixpoint Computation
    27th Static Analysis Symposium (SAS), 2020
    To appear
    Details
  3. Abstract Neural Networks
    27th Static Analysis Symposium (SAS), 2020
    To appear
    Details
  4. A Deep Deterministic Policy Gradient Based Network Scheduler For Deadline-Driven Data Transfer
    2020 IFIP Networking Conference, 2020
    PDF     Details
  5. Deterministic Parallel Fixpoint Computation
    Proc. ACM Program. Lang. (POPL) , 2020
    PDF     ACM©     Details
  6. Correcting Deep Neural Networks with Small, Generalizing Patches
    NeurIPS 2019 Workshop on Safety and Robustness in Decision Making, 2019
    PDF     Details
  7. Computing Linear Restrictions of Neural Networks
    Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems (NeurIPS), 2019
    PDF     Details
  8. A Reinforcement Learning Based Network Scheduler For Deadline-Driven Data Transfers
    IEEE Global Communications Conference (GLOBECOM), 2019
    PDF     Details
  9. An SMT Approach To A Multiparty Economic Scheduling Problem
    17th International Workshop on Satisfiability Modulo Theories (SMT’19), 2019
    PDF     Details
  10. Effective Error-Specification Inference via Domain-Knowledge Expansion
    Proceedings of the 27th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE’19) , 2019
    PDF     ACM©     Details
  11. Path-Based Function Embedding and Its Application to Error-Handling Specification Mining
    Proceedings of the 26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE’18) , 2018
    PDF     ACM©     Details
  12. Path-Based Function Embeddings
    Proceedings of the 40th International Conference on Software Engineering: Companion Proceeedings, ICSE 2018, 2018
    PDF     ACM©     Details
  13. Scaling up Superoptimization
    Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2016
    PDF     ACM©     Details
  14. GreenThumb: superoptimizer construction framework
    Proceedings of the 25th International Conference on Compiler Construction (CC), 2016
    PDF     ACM©     Details
  15. Automating Abstract Interpretation
    17th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2016
    Invited paper
    PDF     Springer©     Details
  16. PostHat and All That: Automating Abstract Interpretation
    Electronic Notes in Theoretical Computer Science , 2015
    Fourth Workshop on Tools for Automatic Program Analysis (TAPAS 2013)
    PDF     Elsevier©     Details
  17. Satisfiability modulo abstraction for separation logic with linked lists
    2014 International Symposium on Model Checking of Software (SPIN), 2014
    PDF     ACM©     Details
  18. Property-Directed Shape Analysis
    26th International Conference on Computer Aided Verification (CAV), 2014
    PDF     Springer©     Details
  19. Through the Lens of Abstraction
    High Confidence Software and Systems Conference (HCSS), 2014
    PDF     Details
  20. A Generalization of Stålmarck’s Method
    19th International Symposium on Static Analysis (SAS), 2012
    PDF     Springer©     Details
  21. Bilateral Algorithms for Symbolic Abstraction
    19th International Symposium on Static Analysis (SAS), 2012
    PDF     Springer©     Details
  22. OpenNWA: A Nested-Word Automaton Library
    24th International Conference on Computer Aided Verification (CAV), 2012
    PDF     Springer©     Details
  23. A Method for Symbolic Computation of Abstract Operations
    24th International Conference on Computer Aided Verification (CAV), 2012
    PDF     Springer©     Details
  24. Instrumentation and sampling strategies for cooperative concurrency bug isolation
    Proceedings of the 25th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2010
    PDF     ACM©     Details
  25. There’s Plenty of Room at the Bottom: Analyzing and Verifying Machine Code
    22nd International Conference on Computer Aided Verification (CAV), 2010
    Invited paper
    PDF     Springer©     Details
  26. Directed Proof Generation for Machine Code
    22nd International Conference on Computer Aided Verification (CAV), 2010
    PDF     Springer©     Details
  27. Proofs from Tests
    IEEE Transactions on Software Engineering (TSE) (4) , 2010
    PDF     IEEE©     Details
  28. The Yogi Project: Software Property Checking via Static Analysis and Testing
    15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2009
    PDF     Springer©     Details
  29. Cooperative crug isolation
    Seventh International Workshop on Dynamic Analysis (WODA), 2009
    PDF     ACM©     Details
  30. Comprehensive path-sensitive data-flow analysis
    Sixth International Symposium on Code Generation and Optimization (CGO), 2008
    PDF     ACM©     Details

Teaching

F’20, F’19, F’18 ECS 240 Programming Languages (Graduate)
W’19, S’18 ECS 140A Programming Languages (Undergraduate)
W’20, F’17 Topics in Automated Reasoning and Program Analysis

Recent Service

PC FSTTCS 2020, CAV 2020, VSTTE 2019, SAS 2019, ASE 2018, ATVA 2018
ERC OOPSLA 2020, PLDI 2016

Students

Sung Kook Kim (Ph.D.)
Zhe Tao (Ph.D.)
Ashley Li (B.S.)
Matthew Sotoudeh (B.S.)

Former Students

Daniel DeFreez (Ph.D., 2019), Assistant Professor, Southern Oregon University
Mohamed Alkaoud (M.S.)  
Jonathan Castello (M.S.)  
Dana Iltis (M.S.)  
Jack Abukhovski (B.S.)  
Eric Li (B.S.)  
Max Nedorezov (B.S.)  
Zaid Al Rakabi (B.S.)  
James Sun (B.S.)  
Xinyuan Sun (B.S.)  
Scott Reichelt (B.S.)  

Theses

  1. Thakur, A. V. (2014, August). Symbolic Abstraction: Algorithms and Applications (Ph.D. dissertation). Computer Sciences Department, University of Wisconsin, Madison.
    PDF     Details
  2. Thakur, A. V. (2008, August). Comprehensive Path-sensitive Data-flow Analysis (M.Sc.(Engg.) thesis). Indian Institute of Science, Bangalore.
    PDF     Details