In 1979, Cousot and Cousot gave a specification of the ?best? (most-precise) abstract transformer possible for a given concrete transformer and a given abstract domain. Unfortunately, their specification does not lead to ...

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 ...

New operating systems with security-specific system calls, such as the Capsicum capability system, allow programmers to write applications that satisfy strong security properties with significantly less effort than full ...

WALi-NWA is a C++ library for constructing, querying, and operating on nested-word automata. It is a portion of the WALi library, which provides types and operations for weighted automata. While the NWA portions of WALi ...

This paper considers some known abstract domains for affine-relation analysis (ARA), along with several variants, and studies how they relate to each other. We show that the abstract domains of Mueller-Olm/Seidl (MOS) ...

Traditionally, reference monitors have been used both to specify a policy of secure behaviors of an application, and to ensure that an application satisfies its specification. However, for recently proposed privilege-aware ...

This paper presents a new approach to the problem of verifying safety properties of concurrent programs with shared memory and interleaving semantics. The method described leverages recent work on context-bounded analysis ...