CAV
2007
Springer
13 years 12 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
13 years 12 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
13 years 12 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
13 years 12 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
13 years 12 months ago
2007
Springer
CAV
2007
Springer
13 years 12 months ago
2007
Springer
CAV
2007
Springer
13 years 12 months ago
2007
Springer
CAV
2007
Springer
13 years 12 months ago
2007
Springer
C32SAT is a tool for checking C expressions. It can check whether a given C expression can be satisfied, is tautological, or always defined according to the ISO C99 standard. C32...
CAV
2007
Springer
13 years 12 months ago
2007
Springer
Bounded context switch reachability analysis is a useful and efficient approach for detecting bugs in multithreaded programs. In this paper, we address the application of this app...
CAV
2007
Springer
13 years 12 months ago
2007
Springer
In 2005 we proposed the first efficient on-the-fly algorithm for solving games based on timed game automata with respect to reachability and safety properties. The first prototy...