We define a new logic, STRAND, that allows reasoning with heapmanipulating programs using deductive verification and SMT solvers. STRAND logic (“STRucture ANd Data” logic) f...
Abstract. Techniques such as verification condition generation, preditraction, and expressive type systems reduce software verification to proving formulas in expressive logics. Pr...
Viktor Kuncak, Ruzica Piskac, Philippe Suter, Thom...
We define a new decidable logic for expressing and checking invariants of programs that manipulate dynamically-allocated objects via pointers and destructive pointer updates. The ...
Greta Yorsh, Alexander Moshe Rabinovich, Mooly Sag...
Our goal is to identify families of relations that are useful for reasoning about software. We describe such families using decidable quantifier-free classes of logical constraints...
Standard analysis on recursive data structures restrict their attention to shape properties (for instance, a program that manipulates a list returns a list), excluding properties t...