CAV
2008
Springer
13 years 7 months ago
2008
Springer
A Tool: Causality-based Abstraction for Security Protocol Analysis (Tool Paper) Michael Backes1,2 , Stefan Lorenz1 , Matteo Maffei1 , and Kim Pecina1 1 Saarland University, Saarbr
CAV
2008
Springer
13 years 7 months ago
2008
Springer
Abstract. The use of Craig interpolants has enabled the development of powerful hardware and software model checking techniques. Efficient algorithms are known for computing interp...
CAV
2008
Springer
13 years 7 months ago
2008
Springer
We study the problem of monitoring concurrent program runs for atomicity violations. Unearthing fundamental results behind scheduling algorithms in database control, we build space...
CAV
2008
Springer
13 years 7 months ago
2008
Springer
Pointer safety faults in device drivers are one of the leading causes of crashes in operating systems code. In principle, shape analysis tools can be used to prove the absence of t...
CAV
2008
Springer
13 years 7 months ago
2008
Springer
Abstract. This paper presents a constraint-based technique for discovering a rich class of inductive invariants (boolean combinations of polynomial inequalities of bounded degree) ...
CAV
2008
Springer
13 years 7 months ago
2008
Springer
Program verification for relaxed memory models is hard. The high degree of nondeterminism in such models challenges standard verification techniques. This paper proposes a new veri...
CAV
2008
Springer
13 years 7 months ago
2008
Springer
In this paper we address the problem of shape analysis for concurrent programs. We present new algorithms, based on abstract interpretation, for automatically verifying properties ...
CAV
2008
Springer
13 years 7 months ago
2008
Springer
In this paper we present a word-level model checking method that attempts to speed up safety property checking of industrial netlists. Our aim is to construct an algorithm that all...
CAV
2008
Springer
13 years 7 months ago
2008
Springer
Ideally, a model checking tool should successfully tackle state space explosion for complete system validation, while providing short counterexamples when an error exists. Techniqu...
CAV
2008
Springer
13 years 7 months ago
2008
Springer