16 citations · 58 across the 8 of their papers we have counts for
8 papers
On Spatial Conjunction as Second-Order Logic
Viktor Kuncak, Martin Rinard
Spatial conjunction is a powerful construct for reasoning about dynamically allocated data structures, as well as concurrent, distributed and mobile computation. While researchers…
On computing the fixpoint of a set of boolean equations
Viktor Kuncak, K. Rustan M. Leino
This paper presents a method for computing a least fixpoint of a system of equations over booleans. The resulting computation can be significantly shorter than the result of iterat…
On Generalized Records and Spatial Conjunction in Role Logic
Viktor Kuncak, Martin Rinard
We have previously introduced role logic as a notation for describing properties of relational structures in shape analysis, databases and knowledge bases. A natural fragment of ro…
On Role Logic
Viktor Kuncak, Martin Rinard
We present role logic, a notation for describing properties of relational structures in shape analysis, databases, and knowledge bases. We construct role logic using the ideas of d…
On the Theory of Structural Subtyping
Viktor Kuncak, Martin Rinard
We show that the first-order theory of structural subtyping of non-recursive types is decidable. Let be a language consisting of function symbols (representing type constructor…
Typestate Checking and Regular Graph Constraints
Viktor Kuncak, Martin Rinard
We introduce regular graph constraints and explore their decidability properties. The motivation for regular graph constraints is 1) type checking of changing types of objects in t…