This paper addresses the problem of proving a given invariance property phi of a loop in a numeric program, by inferring automatically a stronger inductive invariant psi. The algorithm we present is based on both abstract ...

This paper addresses the analysis of concurrent programs with shared memory. Such an analysis is undecidable in the presence of multiple procedures. One approach used in recent work obtains decidability by providing only ...

Extended weighted pushdown systems (EWPDSs) are an extension of pushdown systems that incorporate infinite-state data abstractions. Nested-word automata (NWAs) are able to recognize languages that exhibit context-free ...

A dataflow query asks for the set of reachable (abstract) states, given a starting set of states. In this paper, we show how to optimize multiple queries on the same program (each with a different starting set of states) ...

This paper gives an account of Staalmarck's method for validity checking of propositional-logic formulas, and explains each of the key components in terms of concepts from the field of abstract interpretation. We then ...

There is growing interest in analyzing executables to look for bugs and security vulnerabilities. This paper describes the design and implementation of a language for describing the semantics of an instruction set, along ...

Recently, Esparza et al. generalized Newton's method -- a numerical-analysis algorithm for finding roots of real-valued functions -- to a method for finding fixed-points of systems of equations over semirings. Their method ...