University of Minnesota
Software Engineering Center
/

You are here

Hung T. Pham

Education: 
  • PhD in Computer Science, University of Minnesota, 03/2014.
  • MS in Computer Science, University of Minnesota, 2012.
  • BS in Information Technology, Vietnam National University, Hanoi, 2008.
Biography: 
Hung Pham was a PhD student in computer science at the University of Minnesota. His research interests are in software verification methods and their applications in real-world software development processes.

Recent Publications

The Guardol Language and Verification System

Guardol is a domain-specific language designed to facilitate the construction of correct network guards operating over tree-shaped data. The Guardol system generates Ada code from Guardol programs and also provides specification and automated verification support. Guard programs and specifications are translated to higher order logic, deductively transformed to a form suitable for a SMT-style decision procedure for recursive functions over tree-structured data. The result is that difficult properties of Guardol programs can be proved fully automatically.

Introduction to the Guardol Language and Verification System

Guardol is a high-level programming language intended to facilitate the construction of correct network guards. The Guardol system generates Ada code from Guardol programs. It also provides specification and automated verification support: guard specifications are formally translated to SMT format and passed to a new decision procedure dealing with functions over tree-structured data. The result is that difficult properties of Guardol programs can be proved fully automatically.

FixBag: A Fixpoint Calculator for Quantified Bag Constraints

Abstract interpretation techniques have played a major role in advancing the state-of-the-art in program analysis. Traditionally, stand- alone tools for these techniques have been developed for the numerical domains which may be sucient for lower levels of program correctness. To analyze a wider range of programs, we have developed a tool to compute symbolic xpoints for quantied bag domain. This domain is useful for programs that deal with collections of values. Our tool is able to derive both loop invariants and method pre/post conditions via fixpoint

Pages