Vu 2011 San Francistco ThanhVu (Vũ) Nguyen's Website


Information

I will be a postdoc in the CS dept at UMD in Fall 2014.

Education

Work Experience

Curriculum Vitae (CV)


Research

My research interests lie in the intersection of software engineering and programming languages, with a particular focus on using static and dynamic analyses for automatic invariant generation and program repair.

Common words in my recent publications
  • Program Verification and Analysis, Dynamic and Static Invariant Generation, Program Repairs
  • Evolutionary Computing, Genetic Algorithm, Genetic Programming, Ant-Based Optimization System

Publications

Journal

  1. ThanhVu Nguyen, Deepak Kapur, Westley Weimer, Stephanie Forrest, "DIG: A Dynamic Invariant Generator for Polynomial and Array Invariants", ACM Trans. on Software Engineering and Methodology (TOSEM), 2014, to appear.

  2. Kapur, D., Zhang, Z., Zhao, H., Horbach, M., Lu, Q., Nguyen, T., "Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants", Automated Reasoning and Mathematics: Essays in Memory of William McCune, 2013, pp. 189 --- 228.
    paper, abstract
    Abstract: Geometric heuristics for the quantifier elimination approach presented by Kapur (2004) are investigated to automatically derive loop invariants expressing weakly relational numerical properties (such as l <= x <= h or l <= +/-x +/-y <= h) for imperative programs. Such properties have been successfully used to analyze commercial software consisting of hundreds of thousands of lines of code (using for example, the Astree tool based on abstract interpretation framework proposed by Cousot and his group). The main attraction of the proposed approach is its much lower complexity in contrast to the abstract interpretation approach (O(n^2) in contrast to O(n^4), where n is the number of variables) with the ability to still generate invariants of comparable strength. This approach has been generalized to consider disjunctive invariants of the similar form, expressed using maximum function (such as max(x+a,y+b,z+c,d) <= max(x+e,y+f,z+g,h)), thus enabling automatic generation of a subclass of disjunctive invariants for imperative programs as well.
  3. Claire Le Goues, ThanhVu Nguyen, Stephanie Forrest, Westley Weimer, "GenProg: A Generic Method for Automated Software Repair", IEEE Trans. Software Engineering (TSE), January/February 2012.
    paper
  4. Westley Weimer, Stephanie Forrest, Claire Le Goues, ThanhVu Nguyen, "Automatic Program Repair With Evolutionary Computation", Communications of the ACM (CACM) Vol. 53 No. 5, May 2010, pp. 109 ---116.
    paper
  5. Bui, T., T. Nguyen, C. Patel, and K. Phan, "An Ant-Based Algorithm for Coloring Graphs", Journal of Discrete Applied Mathematics (DAM), Vol. 156(2), 2008, pp. 190 --- 200.
    paper
  6. Smith, J and T. Nguyen, "Autonomous and cooperative robotic behavior based on fuzzy logic and genetic programming", Integrated Computer-Aided Engineering (ICAE), Vol. 14(2), 2007, pp. 141 --- 159.
    paper

Conference

  1. ThanhVu Nguyen, Deepak Kapur, Westley Weimer, Stephanie Forrest, "Using Dynamic Analysis to Generate Disjunctive Invariants", International Conference on Software Engineering (ICSE), 2014.
    paper, presentation, project site, abstract
    Abstract: Program invariants are important for defect detection, program verification, and program repair. However, existing techniques have limited support for important classes of invariants such as disjunctions, which express the semantics of conditional statements. We propose a method for generating disjunctive invariants over numerical domains, which are inexpressible using classical convex polyhedra. Using dynamic analysis and reformulating the problem in non-standard ``max-plus'' and ``min-plus'' algebras, our method constructs hulls over program trace points. Critically, we introduce and infer a weak class of such invariants that balances expressive power against the computational cost of generating nonconvex shapes in high dimensions. Existing dynamic inference techniques often generate spurious invariants that fit some program traces but do not generalize. With the insight that generating dynamic invariants is easy, we propose to verify these invariants statically using k-inductive SMT theorem proving which allows us to validate invariants that are not classically inductive. Results on difficult kernels involving nonlinear arithmetic and abstract arrays suggest that this hybrid approach efficiently generates and proves correct program invariants.
  2. ThanhVu Nguyen, Deepak Kapur, Westley Weimer, Stephanie Forrest, "Using Dynamic Analysis to Discover Polynomial and Array Invariants", International Conference on Software Engineering (ICSE), 2012.
    ACM SIGSOFT Distinguished Paper
    paper, presentation, project site, abstract
    Abstract: Dynamic invariant analysis identifies likely properties over variables from observed program traces. These properties can aid programmers in refactoring, documenting, and debugging tasks by making dynamic patterns visible statically. Two useful forms of invariants involve relations among polynomials over program variables and relations among array variables. Current dynamic analysis methods support such invariants in only very limited forms. We combine mathematical techniques that have not previously been applied to this problem, namely equation solving, polyhedra construction, and SMT solving, to bring new capabilities to dynamic invariant detection. Using these methods, we show how to find equalities and inequalities among nonlinear polynomials over program variables, and linear relations among array variables of multiple dimensions. Preliminary experiments on 24 mathematical algorithms and an implementation of AES encryption provide evidence that the approach is effective at finding these invariants.
  3. Weimer, W., T. Nguyen, C. Le Goues, and S. Forrest, "Automatically Finding Patches Using Genetic Programming", International Conference on Software Engineering (ICSE), 2009.
    ACM SIGSOFT Distinguished Paper and Manfred Paul Award for Excellence in Software: Theory and Practice
    paper, project site, abstract
    Abstract: Automatic program repair has been a longstanding goal in software engineering, yet debugging remains a largely manual process. We introduce a fully automated method for locating and repairing bugs in software. The approach works on off-the-shelf legacy applications and does not require formal specifications, program annotations or special coding practices. Once a program fault is discovered, an extended form of genetic programming is used to evolve program variants until one is found that both retains required functionality and also avoids the defect in question. Standard test cases are used to exercise the fault and to encode program requirements. After a successful repair has been discovered, it is minimized using structural differencing algorithms and delta debugging. We describe the proposed method and report experimental results demonstrating that it can successfully repair ten different C programs totaling 63,000 lines in under 200 seconds, on average.
  4. Forrest, S., W. Weimer, T. Nguyen, and C. Le Goues, "A Genetic Programming Approach to Automated Software Repair", Genetic and Evolutionary Computation Conference (GECCO), 2009.
    Best Paper in the Genetic Programming Track
    paper
  5. Bui, T., T. Nguyen, and J. Rizzo, "Parallel Shared Memory Strategies for Ant-Based Optimization Algorithms", Genetic and Evolutionary Computation Conference (GECCO), 2009.
    Best Paper in the Ant Colony Optimization and Swarm Intelligence track
    paper, presentation, supporting materials, abstract
    Abstract: This paper describes a general scheme to convert sequential ant-based algorithms into parallel shared memory algorithms. The scheme is applied to an ant-based algorithm for the maximum clique problem. Extensive experimental results indicate that the parallel version provides noticeable improvements to the running time while maintaining comparable solution quality to that of the sequential version.
  6. Smith, J and T. Nguyen, "Fuzzy decision trees for planning and autonomous control of a coordinated team of UAVs", Proc. International Society for Optical Engineering (SPIE), 6567, 2007.
    paper
  7. Smith, J and T. Nguyen, "Genetic program based data mining of fuzzy decision trees and methods of improving convergence and reducing bloat", Proc. International Society for Optical Engineering (SPIE), 6570, 2007.
    paper
  8. Smith, J. and T. Nguyen, "Guiding Genetic Program Based DataMining Using Fuzzy Rules", Proc. 7th International Conference for Intelligent Data Engineering and Automated Learning (IDEAL), 4224, 2006, pp. 1337 --- 1345.
    paper
  9. Smith, J. and T. Nguyen, "Evolutionary Data Mining Approach to Creating Digital Logic", Proc. 3rd International Conference on Informatics in Control, Automation and Robotics (ICINCO), 2006, pp. 107 --- 113.
    paper
  10. Smith, J. and T. Nguyen, "Fuzzy Logic Based UAV Allocation and Coordination", Proc. 3rd International Conference on Informatics in Control, Automation and Robotics (ICINCO), 2006, pp. 9 --- 18.
    Best Paper
    Also appears in Informatics in Control, Automation and Robotics, Lecture Notes in Electrical Engineering, Vol. 15(2), 2008, pp. 81 --- 94.
    paper
  11. Bui, T. and T. Nguyen, "An Agent-Based Algorithm for Generalized Graph Colorings", Proc. 8th Annual Conference on Genetic and Evolutionary Computation Conference (GECCO), 2006, pp. 19 --- 26.
    Erdős number: 4 (through Thang N. Bui).
    paper, presentation
  12. Smith, J. and T. Nguyen, "Fuzzy Logic Based Resource Manager for a Team of UAVs", Proc. 25th International Conference of the North American Fuzzy Information Processing Society (NAFIPS), 2006, pp. 463 --- 470.
    paper
  13. Smith, J. and T. Nguyen, "Creating Fuzzy Decision Algorithms Using Genetic Program Based Data Mining", Proc. 25th International Conference of the North American Fuzzy Information Processing Society (NAFIPS), 2006, pp. 471 --- 477.
    paper
  14. Smith, J. and T. Nguyen, "Resource Manager for an Autonomous Coordinated Team of UAVs", Proc. International Society for Optical Engineering (SPIE), 6235, 2006, pp. 118 --- 129.
    paper
  15. Smith, J. and T. Nguyen, "Genetic Program Based Data Mining to Reverse Engineer Digital Logic", Proc. International Society for Optical Engineering (SPIE), 6241, 2006, pp. 24 --- 35.
    paper
  16. Smith, J. and T. Nguyen, "Distributed Autonomous Systems: Resource Management, Planning and Control Algorithms", Proc. International Society for Optical Engineering (SPIE), 5809, 2005, pp. 65 --- 76.
    paper
  17. Smith, J. and T. Nguyen, "Data-Mining-Based Automated Reverse Engineering and Defect Discovery", Proc. International Society for Optical Engineering (SPIE), 5812, 2005, pp. 232 --- 242.
    paper

Workshops

  1. Nguyen, T., W. Weimer, C. Le Goues, and S. Forrest, Extended Abstract: "Using Execution Paths to Evolve Software Patches", IEEE International Conference on Software Testing, Verification, and Validation Workshops (ICSTW), pp.152-153, 2009.
    Best Short Paper and Best Presentation
    paper, presentation
  2. Viamontes, G., M. Amduka, J. Russo, M. Craven, and T. Nguyen, Poster: "Efficient Memoization Strategies for Object Recognition with a Multi-Core Architecture", Proc. 11th Annual High Performance Embedded Computing Workshop (HPEC), 2007.
    Outstanding Submission
    paper

Others

  1. Forrest, S., T. Nguyen, W. Weimer, C. Le Goues, "Fixing software bugs in 10 minutes or less using evolutionary computation", Human-Computer Competition THE 6th ANNUAL (2009) "HUMIES" AWARDS, 2009
    Winner (Gold)
  2. Nguyen, T., W. Weimer, C. Le Goues, and S. Forrest, "Fixing Real Bugs in Real Programs using Evolutionary Computing", Computer Science University of New Mexico Student Conference (CSUSC), 2009
    paper
  3. Nguyen, T., W. Weimer, C. Le Goues, and S. Forrest, Poster: "Evolving Software Repairs Using Genetic Programming", Darwin’s Legacy Symposium, University of New Mexico, 2009.
  4. Bezerra, G and T. Nguyen, "Modeling the Spread of Infection Diseases using an Agent-based Spatial Network", Computer Science University of New Mexico Student Conference (CSUSC), 2008 paper
  5. T. Nguyen, "Graphs Coloring with Ants", Penn State Graduate Research Exhibition, 2006.
  6. T. Nguyen, Poster: "Planning and Control Phases for Cooperative Teams of Unmanned Aerial Vehicles", Penn State Graduate Research Exhibition, 2006
  7. T. Nguyen, Poster: "Reverse Engineering and Exploiting Radars through Evolutionary Computing", Penn State Graduate Research Exhibition, 2006

Thesis


Projects


Vietnamese Stuff

canh truc

Tên tôi là Nguyễn Huy Thanh Vũ, được sinh tại Sài Gòn, Việt Nam. Năm 11 tuổi tôi cùng gia đình qua Hoa Kỳ định cư theo diện H.O (Bố tôi là phi công trong Quân Lực Việt Nam Cộng Hoà).

Gia đình tôi hiện đang ở bang Pennsylvania, tôi cũng đã học ở trường Penn State một thời gian. Hiện nay tôi đang theo chương trình tiến sĩ khoa Điện Toán tại đại học New Mexico. Những nghiên cứu của tôi thuộc lãnh vực thông minh nhân tạo.

Mặc dù trưởng thành ở nước ngoài, nhưng tôi cố gắng tìm hiểu và giữ gìn những gì về nước Việt trước kia qua những sách vở thi ca sưu tầm được. Ngoài thể thao, sở thích chính của tôi là đọc tiểu thuyết, truyện ngắn, hoặc các văn học nước ngoài dịch sang tiếng Việt. Tôi ít khi nghe nhạc hoặc xem TV nhưng tất cả những ca khúc tôi thích đều là những tác phẩm tiền chiến.

Đã có một thời gian tôi rất say mê thi luật và cũng tập làm thơ (các môn tiêu dao khác như cầm, kỳ, hoạ, tử vi tôi đều biết qua). Nhưng qua bao sáng tác mà không để đời được gì, tôi quyết định chỉ tập trung vào khoa học vậy, nhất nghệ tinh .. nhất thân vinh :]

My writings


email Email (PGP key) homepage http://tvn.no-ip.org