Runtime Checking for Separation Logic (2007)
Nguyen, Huu Hai, Kuncak, Viktor, Chin, Wei Ngan
Separation logic is a popular approach for specifying properties of recursive mutable data structures. Several existing systems verify a subclass of separation logic specifications using static...
Automated Verification of Shape and Size (2007)
Nguyen, Huu Hai, David, Cristina, Qin, Shengchao, Chin, Wei Ngan
Despite their popularity and importance, pointer based programs remain a major challenge for program verification. In this paper, we propose an automated verification system that is concise, precise...
Automated Verification of Shape and Size (2007)
Nguyen, Huu Hai, David, Cristina, Qin, Shengchao, Chin, Wei Ngan
Despite their popularity and importance, pointer based programs remain a major challenge for program verification. In this paper, we propose an automated verification system that is concise, precise...
Using Cyclic Memory Allocation to Eliminate Memory Leaks (2005)
Nguyen, Huu Hai, Rinard, Martin C.
We present and evaluate a new memory management technique for eliminating memory leaks in programs with dynamic memory allocation. This technique observes the execution of the program on a sequence...
Using Cyclic Memory Allocation to Eliminate Memory Leaks (2005)
Nguyen, Huu Hai, Rinard, Martin C.
We present and evaluate a new memory management technique for eliminating memory leaks in programs with dynamic memory allocation. This technique observes the execution of the program on a sequence...
Using Cyclic Memory Allocation to Eliminate Memory Leaks (2005)
Nguyen, Huu Hai, Rinard, Martin
We present and evaluate a new memory management technique foreliminating memory leaks in programs with dynamic memoryallocation. This technique observes the execution of the program on asequence of...
Using Cyclic Memory Allocation to Eliminate Memory Leaks (2005)
Nguyen, Huu Hai, Rinard, Martin
We present and evaluate a new memory management technique foreliminating memory leaks in programs with dynamic memoryallocation. This technique observes the execution of the program on asequence of...
Memory Usage Inference for Object-Oriented Programs (2004)
Nguyen, Huu Hai, Chin, Wei Ngan, Qin, Shengchao, Rinard, Martin C.
We present a type-based approach to statically derive symbolic closed-form formulae that characterize the bounds of heap memory usages of programs written in object-oriented languages. Given a...
Memory Usage Inference for Object-Oriented Programs (2004)
Nguyen, Huu Hai, Chin, Wei Ngan, Qin, Shengchao, Rinard, Martin C.
We present a type-based approach to statically derive symbolic closed-form formulae that characterize the bounds of heap memory usages of programs written in object-oriented languages. Given a...
An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic (2004)
Kuncak, Viktor, Nguyen, Huu Hai, Rinard, Martin
We describe an algorithm for deciding the first-order multisorted theory BAPA, which combines 1) Boolean algebras of sets of uninterpreted elements (BA) and 2) Presburger arithmetic operations (PA)....
An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic (2004)
Kuncak, Viktor, Nguyen, Huu Hai, Rinard, Martin
We describe an algorithm for deciding the first-order multisorted theory BAPA, which combines 1) Boolean algebras of sets of uninterpreted elements (BA) and 2) Presburger arithmetic operations (PA)....