About Me
I was born in Vietnam, 1983. In 2005, I got my Bachelor degree in Computer Science from College of Technology, Vietnam National University, Hanoi. From 2005 to 2009, I worked as software engineer in Hanoi, Vietnam. In 2011, I earned Master degree in Computer Science from Uppsala University, Sweden. From 1st November, 2011 to now, I am a Ph.d student under the supervision of Prof.Bengt Jonsson and Prof.Parosh Abdulla in Algorithmic Program Verification
and Upmarc verification center, Department of Technology, Uppsala University, Sweden.
Project
My project is to develop techniques for automatically proving correctness of, and finding the errors in, highly concurrent algorithms and software. Currently, We are working on shape analysis of concurrent programs with dynamic data structures by using automata approach. We are corporating with Brno University of Technology to extend the framework called Forester to verify concurrent algorithms such as concurrents queues and stacks
Publications
2011
Master Thesis: Formal Verification of Skiplist Algorithms
Abstract: We consider the problem of automatically verifying correctness of concurrent algorithms with an unbounded number of threads that access a shared heap. Such algorithms are used, e.g., to implement data structures in common concurrency libraries. Here, we consider algorithms in which each heap node has several pointer field, in particular algorithms that manipulate skiplist-like data structures. For such algorithms, we propose a methodology for generating and checking program invariants. Particular difficulties are incurred by the necessity to use universal quantification over heap nodes. We present a suitable form for such invariants, together with techniques for inferring them and checking their validity.
2013
Conference Papers
-
Veri?cation of heap manipulating programs with ordered data by extended forest automata. In Automated Technology for Verification and Analysis: ATVA 2013, volume 8172 of Lecture Notes in Computer Science, pp 224-239, Springer Berlin/Heidelberg, 2013. (DOI, fulltext:postprint
).
Abstract of the paper: We present a general framework for verifying programs with complex dynamic linked data structures whose correctness depends on ordering relations between stored data values. The underlying formalism of our framework is that of forest automata (FA), which has previously been developed for verification of heap-manipulating programs. We extend FA by constraints between data elements associated with nodes of the heaps represented by FA, and we present extended versions of all operations needed for using the extended FA in a fully-automated verification approach, based on abstract interpretation. We have implemented our approach as an extension of the Forester tool and successfully applied it to a number of programs dealing with data structures such as various forms of singly- and doubly-linked lists, binary search trees, as well as skip lists.