Abstract. This paper explores a way to apply model checking techniques to parallel programs that use the nonblocking primitives of the Message Passing Interface (MPI). The method h...
Interpolation is an important component of recent methods for program verification. It provides a natural and effective means for computing separation between the sets of ‘good...
Abstract. This paper is concerned with one of the basic problems in abstract interpretation, namely, for a given abstraction and a given set of concrete transformers (that express ...
Tal Lev-Ami, Mooly Sagiv, Neil Immerman, Thomas W....
Abstract. Several verification methods involve reasoning about multi-valued systems, in which an atomic proposition is interpreted at a state as a lattice element, rather than a B...
Abstract. This paper presents a novel shape analysis algorithm with local reasoning that is designed to analyze heap structures with structural invariants, such y-linked lists. The...
Abstract. In this paper we analyze the complexity of checking safety and termination properties, for a very simple, yet non-trivial, class of programs with singly-linked list data ...