20 citations · 34 across the 10 of their papers we have counts for
4 papers · 1 filter
Unification-based Pointer Analysis without Oversharing
Jakub Kuderski, Jorge A. Navas, Arie Gurfinkel
Pointer analysis is indispensable for effectively verifying heap-manipulating programs. Even though it has been studied extensively, there are no publicly available pointer analyse…
Horn Clauses as an Intermediate Representation for Program Analysis and Transformation
Graeme Gange, Jorge A. Navas, Peter Schachte +2
Many recent analyses for conventional imperative programs begin by transforming programs into logic programs, capitalising on existing LP analyses and simple LP semantics. We propo…
A Partial-Order Approach to Array Content Analysis
Graeme Gange, Jorge A. Navas, Peter Schachte +2
We present a parametric abstract domain for array content analysis. The method maintains invariants for contiguous regions of the array, similar to the methods of Gopan, Reps and S…
Symbolic Execution for Verification
Joxan Jaffar, Jorge A. Navas, Andrew E. Santosa
In previous work, we presented a symbolic execution method which starts with a concrete model of the program but progressively abstracts away details only when these are known to b…