CAV
2008
Springer
14 years 2 months ago
2008
Springer
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...
CAV
2008
Springer
14 years 2 months ago
2008
Springer
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...
CAV
2008
Springer
14 years 2 months ago
2008
Springer
We present CSIsat, an interpolating decision procedure for the quantifier-free theory of rational linear arithmetic and equality with uninterpreted function symbols. Our implementa...
CAV
2008
Springer
14 years 2 months ago
2008
Springer
Requirements of reactive systems are usually specified by classifying system executions as desirable and undesirable. To specify prioritized requirements, we propose to associate a...
CAV
2008
Springer
14 years 2 months ago
2008
Springer
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...
CAV
2008
Springer
14 years 2 months ago
2008
Springer
Abstract. We describe a method for synthesizing reasonable underapproximations to weakest preconditions for termination--a long-standing open problem. The paper provides experiment...
CAV
2008
Springer
14 years 2 months ago
2008
Springer
CAV
2008
Springer
14 years 2 months ago
2008
Springer
CAV
2008
Springer
14 years 2 months ago
2008
Springer
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...
CAV
2008
Springer
14 years 2 months ago
2008
Springer
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...