Dagger

Dagger is a static analyzer for C programs. Dagger takes as input a C program along with its specification. The specification is given by assert statements embedded in the C program. Dagger uses Counter-Example Guided Abstraction Refinement (CEGAR) technology to either prove that the input program satisfies its specification or generate a counter-example demonstrating violation of the specification.

Publications

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

Benchmarks

Sendmail

p1-ok
p2-ok
p3-ok
p1-bad
p2-bad
p3-bad

Sting

seesaw
bkley
bk-nat
hsort
efm
lifo
lifnat
cars
barbr
swim
swim1
hsort1
barbr1
lifnat1

Miscellaneous

f1a
ex1
f2
ex2
JM06