Program Analysis Research @ GIST

We are interested in various research topics for improving the safety and reliability of software, including:

• Formal verification for proving the absence of vulnerabilities and errors in software.
• Symbolic execution for finding vulnerabilities and errors in software.
• Testing SMT solvers for enhancing the reliability of verification and symbolic execution tools.
• Efficient decision procedures for first-order theories for making formal verification and symbolic execution more practical.

---

Introduction to Our Research

• Introduction to Program Analysis Techniques with Applications to Smart Contract Security.
  8 Sep 2023. GIST EECS Colloquium
  [slides]

---

Recent Research Projects

• Automatically fixing security vulnerabilities in smart contracts
  [FSE'23 paper] [slides]



• Automatically finding critical bugs in SMT solvers
  [ICSE'23 paper] [slides]



• Automatically finding security vulnerabilities in smart contracts
  [USENIX Security'21 paper] [slides] [media]



• Automatically verifying the safety of smart contracts
  [IEEE S&P'20 paper] [slides]



• Automatically generating feedback for functional programming assignments
  [OOPSLA'18 paper] [slides]