Sciweavers

157
Voted
CAV
2009
Springer
105views Hardware» more  CAV 2009»
16 years 7 months ago
Transactional Memory: Glimmer of a Theory
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...
Rachid Guerraoui, Michal Kapalka
CAV
2009
Springer
177views Hardware» more  CAV 2009»
16 years 7 months ago
Software Transactional Memory on Relaxed Memory Models
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...
Rachid Guerraoui, Thomas A. Henzinger, Vasu Singh
CAV
2009
Springer
164views Hardware» more  CAV 2009»
16 years 7 months ago
InvGen: An Efficient Invariant Generator
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...
Ashutosh Gupta, Andrey Rybalchenko
CAV
2009
Springer
171views Hardware» more  CAV 2009»
16 years 7 months ago
CalFuzzer: An Extensible Active Testing Framework for Concurrent Programs
Active testing has recently been introduced to effectively test concurrent programs. Active testing works in two phases. It first uses predictive off-the-shelf static or dynamic pr...
Pallavi Joshi, Mayur Naik, Chang-Seo Park, Koushik...
CAV
2009
Springer
133views Hardware» more  CAV 2009»
16 years 7 months ago
Cardinality Abstraction for Declarative Networking Applications
ity Abstraction for Declarative Networking Applications Juan A. Navarro P?erez, Andrey Rybalchenko, and Atul Singh Max Planck Institute for Software Systems (MPI-SWS) Declarative N...
Andrey Rybalchenko, Atul Singh, Juan Antonio Navar...
CAV
2009
Springer
141views Hardware» more  CAV 2009»
16 years 7 months ago
Apron: A Library of Numerical Abstract Domains for Static Analysis
Library of Numerical Abstract Domains for Static Analysis Bertrand Jeannet1 and Antoine Min?e2 1 INRIA Rh^one-Alpes, Grenoble, France, Bertrand.Jeannet@inrialpes.fr 2 CNRS, ?Ecole ...
Antoine Miné, Bertrand Jeannet
CAV
2009
Springer
136views Hardware» more  CAV 2009»
16 years 7 months ago
Intra-module Inference
Abstract. Contract-based property checkers hold the potential for precise, scalable, and incremental reasoning. However, it is difficult to apply such checkers to large program mod...
Shuvendu K. Lahiri, Shaz Qadeer, Juan P. Galeotti,...
CAV
2009
Springer
206views Hardware» more  CAV 2009»
16 years 7 months ago
D-Finder: A Tool for Compositional Deadlock Detection and Verification
D-Finder tool implements a compositional method for the verification of component-based systems described in BIP language encompassing multi-party interaction. For deadlock detecti...
Saddek Bensalem, Marius Bozga, Thanh-Hung Nguyen, ...
141
Voted
CAV
2009
Springer
127views Hardware» more  CAV 2009»
16 years 7 months ago
Incremental Instance Generation in Local Reasoning
Swen Jacobs
CAV
2009
Springer
123views Hardware» more  CAV 2009»
16 years 7 months ago
Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models
Aditya Kanade, Rajeev Alur, Franjo Ivancic, S. Ram...