CAV
2009
Springer
15 years 4 days ago
2009
Springer
We present the key ideas in the design and implementation of Beaver, an SMT solver for quantifier-free finite-precision bit-vector logic (QF BV). Beaver uses an eager approach, enc...
CAV
2009
Springer
15 years 4 days ago
2009
Springer
This paper is concerned with the problem of computing the image of a set by a polynomial function. Such image computations constitute a crucial component in typical tools for set-b...
CAV
2009
Springer
15 years 4 days ago
2009
Springer
tope Abstract Domain Taylor1+ Khalil Ghorbal, Eric Goubault, and Sylvie Putot CEA, LIST, Modelisation and Analysis of Systems in Interaction, F-91191 Gif-sur-Yvette Cedex, France, ...
CAV
2009
Springer
15 years 4 days ago
2009
Springer
CAV
2009
Springer
15 years 4 days ago
2009
Springer
Counter Abstraction for Concurrent Software G?erard Basler1 , Michele Mazzucchi1 , Thomas Wahl1,2 , Daniel Kroening1,2 1 Computer Systems Institute, ETH Zurich, Switzerland 2 Compu...
CAV
2009
Springer
15 years 4 days ago
2009
Springer
Abstract. BeepBeep is a lightweight runtime monitor for Ajax web applications. Interface specifications are expressed internally in an extension of LTL with first-order quantificat...
CAV
2009
Springer
15 years 4 days ago
2009
Springer
We present VS3 , a tool that automatically verifies complex properties of programs and infers maximally weak preconditions and maximally strong postconditions by leveraging the pow...
CAV
2009
Springer
15 years 4 days ago
2009
Springer
Transactional memory (TM) is a promising paradigm for concurrent programming. This paper is an overview of our recent theoretical work on defining a theory of TM. We first recall s...
CAV
2009
Springer
15 years 4 days ago
2009
Springer
Abstract. Pseudo-code descriptions of STMs assume sequentially consistent program execution and atomicity of high-level STM operations like read, write, and commit. These assumptio...
CAV
2009
Springer
15 years 4 days ago
2009
Springer
Abstract. In this paper we present InvGen, an automatic linear arithmetic invariant generator for imperative programs. InvGen's unique feature is in its use of dynamic analysi...