2 citations · 5 across the 4 of their papers we have counts for
5 papers
Deciding Separation Logic with Pointer Arithmetic and Inductive Definitions
Wanyun Su, Zhilin Wu, Mihaela Sighireanu
Pointer arithmetic is widely used in low-level programs, e.g. memory allocators. The specification of such programs usually requires using pointer arithmetic inside inductive defin…
Exploiting Pointer Analysis in Memory Models for Deductive Verification
Bouillaguet Quentin, Bobot François, Sighireanu Mihaela +1
Cooperation between verification methods is crucial to tackle the challenging problem of software verification. The paper focuses on the verification of C programs using pointers a…
Hierarchical Shape Abstraction for Analysis of Free-List Memory Allocators
Bin Fang, Mihaela Sighireanu
We propose a hierarchical abstract domain for the analysis of free-list memory allocators that tracks shape and numerical properties about both the heap and the free lists. Our dom…
On Automated Lemma Generation for Separation Logic with Inductive Definitions
Constantin Enea, Mihaela Sighireanu, Zhilin Wu
Separation Logic with inductive definitions is a well-known approach for deductive verification of programs that manipulate dynamic data structures. Deciding verification condition…
A Generic Framework for Reasoning about Dynamic Networks of Infinite-State Processes
Ahmed Bouajjani, Cezara Dragoi, Constantin Enea +2
We propose a framework for reasoning about unbounded dynamic networks of infinite-state processes. We propose Constrained Petri Nets (CPN) as generic models for these networks. The…