3 citations · 7 across the 6 of their papers we have counts for
7 papers
TracerX: Dynamic Symbolic Execution with Interpolation
Joxan Jaffar, Rasool Maghareh, Sangharatna Godboley +1
Dynamic Symbolic Execution (DSE) is an important method for the testing of programs. An important system on DSE is KLEE which inputs a C/C++ program annotated with symbolic variabl…
Shape Neutral Analysis of Graph-based Data-structures
Gregory J. Duck, Joxan Jaffar, Roland H. C. Yap
Malformed data-structures can lead to runtime errors such as arbitrary memory access or corruption. Despite this, reasoning over data-structure properties for low-level heap manipu…
Incremental Quantitative Analysis on Dynamic Costs
Duc-Hiep Chu, Joxan Jaffar, Vijayaraghavan Murali
In quantitative program analysis, values are assigned to execution traces to represent a quality measure. Such analyses cover important applications, e.g. resource usage. Examining…
Automatic Reasoning on Recursive Data-Structures with Sharing
Duc-Hiep Chu, Joxan Jaffar
We consider the problem of automatically verifying programs which manipulate arbitrary data structures. Our specification language is expressive, contains a notion of \emph{separat…
A Framework to Synergize Partial Order Reduction with State Interpolation
Duc-Hiep Chu, Joxan Jaffar
We address the problem of reasoning about interleavings in safety verification of concurrent programs. In the literature, there are two prominent techniques for pruning the search…
Automating Proofs of Data-Structure Properties in Imperative Programs
Duc-Hiep Chu, Joxan Jaffar, Minh-Thai Trinh
We consider the problem of automated reasoning about dynamically manipulated data structures. The state-of-the-art methods are limited to the unfold-and-match (U+M) paradigm, where…