University of Minnesota
Software Engineering Center
/

You are here

Home

Hung T. Pham

External Links: 
http://www-users.cs.umn.edu/~hung/
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

Reasoning about Algebraic Datatypes with Abstractions

Reasoning about functions that operate over algebraic data types is an important problem for a large variety of applications. One application of particular interest is network applications that manipulate or reason about complex message structures, such as XML messages. This paper presents a decision procedure for reasoning about algebraic data types using abstractions that are provided by catamorphisms: fold functions that map instances of algebraic data types to values in a decidable domain.

Parameterized Abstractions for Reasoning about Algebraic Data Types

Reasoning about algebraic data types is an important problem for a variety of proof tasks. Recently, decision procedures have been proposed for algebraic data types that create suitable abstractions of values in the types. A class of abstractions created from catamorphism functions has been shown to be theoretically applicable to a wide variety of reasoning tasks as well as efficient in practice. However, in previous work, the decidability of catamorphism functions involving parameters in addition to the data type argument has not been studied.

RADA: A Tool for Reasoning about Algebraic Data Types with Abstractions

We present RADA, a portable, scalable tool for reasoning about formulas containing algebraic data types using catamorphism (fold) functions. It can work as a back-end for reasoning about recursive programs that manipulate algebraic types. RADA operates by successively unrolling catamorphisms and uses either CVC4 and Z3 as reasoning engines. We have used RADA for reasoning about functional implementations of complex data structures and to reason about guard applications that determine whether XML messages should be allowed to cross network security domains.

Pages