Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
CAV
2008
Springer
170views Hardware» more  CAV 2008»
11 years 10 months ago
Local Proofs for Linear-Time Properties of Concurrent Programs
Abstract. This paper develops a local reasoning method to check lineartime temporal properties of concurrent programs. In practice, it is often infeasible to model check over the p...
Ariel Cohen 0002, Kedar S. Namjoshi
CAV
2008
Springer
89views Hardware» more  CAV 2008»
11 years 10 months ago
Inferring Congruence Equations Using SAT
This paper proposes a new approach for deriving invariants that are systems of congruence equations where the modulo is a power of 2. The technique is an amalgam of SAT-solving, wh...
Andy King, Harald Søndergaard
CAV
2008
Springer
139views Hardware» more  CAV 2008»
11 years 10 months ago
CSIsat: Interpolation for LA+EUF
We present CSIsat, an interpolating decision procedure for the quantifier-free theory of rational linear arithmetic and equality with uninterpreted function symbols. Our implementa...
Dirk Beyer, Damien Zufferey, Rupak Majumdar
CAV
2008
Springer
80views Hardware» more  CAV 2008»
11 years 10 months ago
Ranking Automata and Games for Prioritized Requirements
Requirements of reactive systems are usually specified by classifying system executions as desirable and undesirable. To specify prioritized requirements, we propose to associate a...
Rajeev Alur, Aditya Kanade, Gera Weiss
CAV
2008
Springer
99views Hardware» more  CAV 2008»
11 years 10 months ago
Correcting a Space-Efficient Simulation Algorithm
Although there are many efficient algorithms for calculating the simulation preorder on finite Kripke structures, only two have been proposed of which the space complexity is of t...
Rob J. van Glabbeek, Bas Ploeger
CAV
2008
Springer
104views Hardware» more  CAV 2008»
11 years 10 months ago
Proving Conditional Termination
Abstract. We describe a method for synthesizing reasonable underapproximations to weakest preconditions for termination--a long-standing open problem. The paper provides experiment...
Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Ryb...
CAV
2008
Springer
112views Hardware» more  CAV 2008»
11 years 10 months ago
Automated Assume-Guarantee Reasoning by Abstraction Refinement
Mihaela Gheorghiu Bobaru, Corina S. Pasareanu, Dim...
CAV
2008
Springer
104views Hardware» more  CAV 2008»
11 years 10 months ago
Semi-external LTL Model Checking
Stefan Edelkamp, Peter Sanders, Pavel Simecek
CAV
2008
Springer
125views Hardware» more  CAV 2008»
11 years 10 months ago
Application of Formal Word-Level Analysis to Constrained Random Simulation
Abstract. Constrained random simulation is supported by constraint solvers integrated within simulators. These constraint solvers need to be fast and memory efficient to maintain s...
Hyondeuk Kim, HoonSang Jin, Kavita Ravi, Petr Spac...
CAV
2008
Springer
115views Hardware» more  CAV 2008»
11 years 10 months ago
An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths
This paper proposes a new approach for proving arithmetic correctness of data paths in System-on-Chip modules. It complements existing techniques which are, for reasons of complexi...
Oliver Wienand, Markus Wedler, Dominik Stoffel, Wo...
books