CAV
2005
Springer
14 years 5 months ago
2005
Springer
Abstract. We propose a new technique for the static analysis of concurrent programs comprised of multiple threads. In general, the problem is known to be undecidable even for progr...
CAV
2005
Springer
14 years 5 months ago
2005
Springer
Abstract. In predicate abstraction, exact image computation is problematic, requiring in the worst case an exponential number of calls to a decision procedure. For this reason, sof...
CAV
2005
Springer
14 years 5 months ago
2005
Springer
Bounded model checking is an efficient method for finding bugs in system designs. The major drawback of the basic method is that it cannot prove properties, only disprove them. R...
CAV
2005
Springer
14 years 5 months ago
2005
Springer
Abstract. The coverability problem is decidable for the class of wellstructured transition systems. Until recently, the only known algorithm to solve this problem was based on symb...
CAV
2005
Springer
14 years 5 months ago
2005
Springer
In this paper, we present the features of Romeo, a Time Petri Net (TPN) analyzer. The tool Romeo allows state space computation of TPN and on-the-fly model-checking of reachabilit...
CAV
2005
Springer
14 years 5 months ago
2005
Springer
Model checking has proven to be an effective technology for verification and debugging in hardware and more recently in software domains. We believe that recent trends in both th...
CAV
2005
Springer
14 years 5 months ago
2005
Springer
Automaton-based static program analysis has proved to be an effective tool for bug finding. Current tools generally re-analyze a program from scratch in response to a change in t...
CAV
2005
Springer
14 years 5 months ago
2005
Springer
CAV
2005
Springer
14 years 5 months ago
2005
Springer
Abstract. We address the issue of efficiently automating assume-guarantee reasoning for simulation conformance between finite state systems and specifications. We focus on a non...
CAV
2005
Springer
14 years 5 months ago
2005
Springer
We present a complete method for synthesizing lexicographic linear ranking functions supported by inductive linear invariants for loops with linear guards and transitions. Proving ...