Matan Shachnai

Applied scientist and engineer - software correcteness, security, automated reasoning.

Github

Google Scholar

Contact
Research

Imagine a software system that is used by millions of people worldwide — a banking system, a phone, or an autonomous vehicle, for example. Now imagine if this system had bugs which could result in unauthorized access that could be used to steal important private information (financial or otherwise). Worse yet, what if it contained bugs which could be exploited and, in turn, endanger or harm people. These are the kind of real world problems I want to help prevent.

My research is led by the following questions:
1) How can we automatically generate software that does exactly what we intend it to?
2) How can we prove (i.e., formally verify) that software systems are free from costly or catastrophic bugs?
My goal is to construct robust and efficient tools and systems that allow developers of all levels to design formally correct software for safety critical systems.

Research Areas

Program Synthesis, Automated Reasoning, Formal Methods, Verification, Static Analysis

Publications

  • Matan Shachnai, Harishankar Vishwanathan, Srinivas Narayana, and Santosh Nagarakatte. 2025. Comparing the Precision of Abstract Operators in the eBPF Verifier using Differential Synthesis. Static Analysis Symposium (SAS 2025). (PDF)
  • Harishankar Vishwanathan, Matan Shachnai, Srinivas Narayana, and Santosh Nagarakatte. 2025. Automatic Synthesis of Abstract Operators for eBPF. Workshop on eBPF and Kernel Extensions (eBPF 2025). (PDF)
  • Matan Shachnai*, Harishankar Vishwanathan*, Srinivas Narayana, and Santosh Nagarakatte. 2024. Fixing Latent Unsound Abstract Operators in the eBPF Verifier of the Linux Kernel. Static Analysis Symposium (SAS 2024). (PDF)
  • Harishankar Vishwanathan*, Matan Shachnai*, Srinivas Narayana, and Santosh Nagarakatte. 2023. Verifying the Verifier: eBPF Range Analysis Verification. International Conference on Computer Aided Verification (CAV 2023). (PDF)
  • Harishankar Vishwanathan, Matan Shachnai, Srinivas Narayana, and Santosh Nagarakatte. 2022. Sound, Precise, and Fast Abstract Interpretation with Tristate Numbers. Symposium on Code Generation and Optimization (CGO 2022). (PDF) Distinguished Paper Award
  • Jay P. Lim, Matan Shachnai, and Santosh Nagarakatte. 2020. Approximating trigonometric functions for posits using the CORDIC method. International Conference on Computing Frontiers (CF 2020). (PDF)
    • * Denotes equal contribution
    Education

    Rutgers University    
      Ph.D. Computer Science -- 2026
    Dissertation: Practical Formal Methods for the Linux eBPF Verifer: Scalable Verification and Witness Generation

    Rutgers University    
      B.A. Honors in Computer Science (Summa Cum Laude) -- 2020

    Teaching

    CS 211: Computer Architecture - Teaching Assistant    
      Fall 2019, Fall 2020, Spring 2021

    Plain academic template! Here is the source of my homepage.