5 citations · 5 across the 3 of their papers we have counts for
5 papers
Automatic Inference of Relational Object Invariants
Yusen Su, Jorge A. Navas, Arie Gurfinkel +1
Relational object invariants (or representation invariants) are relational properties held by the fields of a (memory) object throughout its lifetime. For example, the length of a…
Ownership in low-level intermediate representation
Siddharth Priya, Arie Gurfinkel
The concept of ownership in high level languages can aid both the programmer and the compiler to reason about the validity of memory operations. Previously, ownership semantics has…
Synthesizing Modular Invariants for Synchronous Code
Pierre-Loic Garoche, Arie Gurfinkel, Temesghen Kahsai
In this paper, we explore different techniques to synthesize modular invariants for synchronous code encoded as Horn clauses. Modular invariants are a set of formulas that characte…
SMT-based Model Checking for Recursive Programs
Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki
We present an SMT-based symbolic model checking algorithm for safety verification of recursive programs. The algorithm is modular and analyzes procedures individually. Unlike other…
Robust Vacuity for Branching Temporal Logic
Arie Gurfinkel, Marsha Chechik
There is a growing interest in techniques for detecting whether a logic specification is satisfied too easily, or vacuously. For example, the specification "every request is eventu…