CAV
2010
Springer
13 years 7 months ago
2010
Springer
Gist is a tool that (a) solves the qualitative analysis problem of turn-based probabilistic games with -regular objectives; and (b) synthesizes reasonable environment assumptions f...
CAV
2010
Springer
13 years 7 months ago
2010
Springer
Systems ought to behave reasonably even in circumstances that are not anticipated in their specifications. We propose a definition of robustness for liveness specifications which p...
CAV
2010
Springer
13 years 7 months ago
2010
Springer
We present a graphical toolset for verifying AADL models, which are gaining widespread acceptance in aerospace, automobile and avionics industries for comprehensively specifying sa...
CAV
2010
Springer
13 years 7 months ago
2010
Springer
Analysis of Symbolic Executions Aws Albarghouthi1 , Arie Gurfinkel2 , Ou Wei1,3 , and Marsha Chechik1 1 Department of Computer Science, University of Toronto, Canada 2 Software Eng...
CAV
2010
Springer
13 years 7 months ago
2010
Springer
We show a new and constructive proof of the following language-theoretic result: for every context-free language L, there is a bounded context-free language L L which has the same...
CAV
2010
Springer
13 years 7 months ago
2010
Springer
We describe a practical method for reasoning about realistic concurrent programs. Our method allows global two-state invariants that restrict update of shared state. We provide sim...
CAV
2010
Springer
13 years 7 months ago
2010
Springer
Often one has a preference order among the different systems that satisfy a given specification. Under a probabilistic assumption about the possible inputs, such a preference order...
CAV
2010
Springer
13 years 7 months ago
2010
Springer
We consider the class of finite-state programs executed by an unbounded number of replicated threads communicating via shared variables. The thread-state reachability problem for t...
CAV
2010
Springer
13 years 7 months ago
2010
Springer
CAV
2010
Springer
13 years 8 months ago
2010
Springer
Graded-CTL is an extension of CTL with graded quantifiers which allow to reason about either at least or all but any number of possible futures. In this paper we show an extension...