CAV
2007
Springer
14 years 5 months ago
2007
Springer
We present a simple and effective approximated backward reachability algorithm for parameterized systems with existentially and universally quantified global conditions. The indivi...
CAV
2007
Springer
14 years 5 months ago
2007
Springer
Abstract. A recent approach to automated assume-guarantee reasoning (AGR) for concurrent systems relies on computing environment assumptions for components using the L algorithm fo...
CAV
2007
Springer
14 years 7 months ago
2007
Springer
This paper explores the concept of locality in proofs of global safety properties of asynchronously composed, multi-process programs. Model checking on the full state space is ofte...
CAV
2007
Springer
14 years 7 months ago
2007
Springer
CAV
2007
Springer
14 years 7 months ago
2007
Springer
Abstract. While effective methods for bit-level verification of low-level properties exist, system-level properties that entail reasoning about a significant part of the design p...
CAV
2007
Springer
14 years 7 months ago
2007
Springer
In this paper we propose a complete chain for synthesizing controllers from high-level specifications. From real-time properties expressed in the logic MTL we generate, under boun...
CAV
2007
Springer
14 years 7 months ago
2007
Springer
lued Abstraction for Continuous-Time Markov Chains⋆ Joost-Pieter Katoen1 , Daniel Klink1 , Martin Leucker2 , and Verena Wolf3 RWTH Aachen University1 , TU Munich2 , University of...
CAV
2007
Springer
14 years 7 months ago
2007
Springer
Abstract. Regular model checking is a form of symbolic model checking technique for systems whose states can be represented as finite words over a finite alphabet, where regular ...
CAV
2007
Springer
14 years 7 months ago
2007
Springer
stractions from Proofs Ranjit Jhala1 Kenneth L. McMillan2 1 UC San Diego 2 Cadence Berkeley Laboratories We present a technique for using infeasible program paths to automatically ...
CAV
2007
Springer
14 years 7 months ago
2007
Springer