Ph.D. (Monash University, 1985)
M.Sc. (University of Melbourne, 1981)
B.Sc. (Honours, University of Melbourne, 1979)
651 67346

Research Areas

  • Programming Languages & Software Engineering
  • Algorithms & Theory

Research Interests

  • Program Analysis
  • Theorem-Proving
  • Combinatorial Optimization
  • Programming Languages and Applications


Joxan Jaffar received his B.Sc.(Hons, 1st class) and M.Sc. from Melbourne University in 1979 and 1981, and his Ph.D. from Monash University in 1985. From 1982 through 1986, he was a Lecturer in Monash, and from 1986 through 1995, he was a Research Staff Member and Project Leader in the IBM. T.J. Watson Research Center, Yorktown Heights, New York. He joined NUS in 1995, became Head of the Department of Computer Science in 1998, and Dean of the School of Computing from 2001-2007. Amongst his main early contributions are the principles of constraint logic programming, and the widely-used CLP(R) system. His current interests are in programming languages and constraint solving, with some emphasis on symbolic execution methods for verification, analysis and testing. His current research tool Tracer-X performs dynamic symbolic execution with interpolation, which supports his analysis algorithms for quantitative analysis, memory usage, and string constraint reasoning.

Current Projects

  • Tracer-X: A symbolic execution system for C/C++ based on interpolation
  • Automatic Induction: development of inference rules that can be automatically applied for inductive reasoning over data structures.
  • Quantitative Analysis: to discover resource bounds for critical embedded software.
  • String solving: algorithms for the security reasoning about string constraints which are prevalent in web applications.
  • Memory Analysis: to protect against memory errors and insecure memory usage.

Selected Publications

  • M.T. Trinh, D.H. Chu and J. Jaffar, Model Counting for
    Recursively-Defined Strings, ACM Conf. on Computer-Aided Verification
    (CAV), 2017.

  • Chu Duc Hiep, Joxan Jaffar and Rasool Maghareh, Precise Cache Timing
    Analysis via Symbolic Simulation, Conf. on Real-Time Applications and
    Application (RTAS), 2016

  • M.T. Trinh, D.H. Chu and J. Jaffar, Progressive Reasoning over
    Recursively-Defined Strings, ACM Conf. on Computer-Aided Verification
    (CAV), 2016

  • D.H. Chu and J. Jaffar and M.T. Trinh, Automatic Induction Proofs
    of Data-Structures in Imperative Programs, Conf on Programming
    Language Design and Implementation (PLDI), 2015.

  • D.H. Chu, J. Jaffar and V. Murali, Lazy Symbolic Execution for
    Enhanced Learning, Runtime Verification (RV) 2014.

Awards & Honours

Teaching (2019/2020)

  • CS6215: Advanced Topics in Program Analysis
  • CS5218: Principles of Program Analysis