-
Dirk Beyer.
Competition on Software Verification (SV-COMP).
In C. Flanagan and B. König, editors,
Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS 2012, Tallinn, Estonia, March 27-30),
LNCS 7214,
pages 504--524,
2012.
Springer-Verlag, Heidelberg.
[
WWW
] [
PDF
] Keyword(s): Software Model Checking.
@InProceedings{TACAS12,
author = {Dirk Beyer},
title = {Competition on Software Verification ({SV-COMP})},
booktitle = {Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS~2012, Tallinn, Estonia, March 27-30)},
publisher = {Springer-Verlag, Heidelberg},
editor = {C.~Flanagan and B.~K{\"o}nig},
series = {LNCS~7214},
pages = {504--524},
year = {2012},
isbn = {},
keyword = {Software Model Checking},
pdf = {http://www.sosy-lab.org/~dbeyer/Publications/2012-TACAS.Competition_on_Software_Verification.pdf},
url = {http://sv-comp.sosy-lab.org/},
abstract = { },
annote = {
},
}
-
Dirk Beyer,
Thomas A. Henzinger,
M. Erkan Keremoglu,
and Philipp Wendler.
Conditional Model Checking: A Technique to Pass Information between Verifiers.
In Tevfik Bultan and Martin Robillard, editors,
Proceedings of the 20th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE 2012, Cary, NC, November 10-17),
2012.
ACM.
[ PDF
] Keyword(s): Software Model Checking.
Abstract: |
Software model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself in a space-out, time-out, or one component of the verification tool giving up; in all of these failing cases, significant computation is performed by the verification tool before the failure, but no result is reported. We propose to reformulate the model-checking problem as follows, in order to have the verification tool report a summary of the performed work even in case of failure: given a program and a specification, the model checker returns a condition P ---usually a state predicate--- such that the program satisfies the specification under the condition P ---that is, as long as the program does not leave the states in which P is satisfied. In our experiments, we investigated as one major application of conditional model checking the sequential combination of model checkers with information passing. We give the condition that one model checker produces, as input to a second conditional model checker, such that the verification problem for the second is restricted to the part of the state space that is not covered by the condition, i.e., the second model checker works on the problems that the first model checker could not solve. Our experiments demonstrate that repeated application of conditional model checkers, passing information from one model checker to the next, can significantly improve the verification results and performance, i.e., we can now verify programs that we could not verify before. |
@InProceedings{FSE12,
author = {Dirk Beyer and Thomas A. Henzinger and M. Erkan Keremoglu and Philipp Wendler},
title = {Conditional Model Checking: {A} Technique to Pass Information between Verifiers},
booktitle = {Proceedings of the 20th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE~2012, Cary, NC, November 10-17)},
publisher = {ACM},
editor = {Tevfik Bultan and Martin Robillard},
pages = {},
year = {2012},
isbn = {978-1-4503-1614-9},
keyword = {Software Model Checking},
pdf = {http://www.sosy-lab.org/~dbeyer/Publications/2012-FSE.Conditional_Model_Checking.pdf},
url = {},
abstract = { Software model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself in a space-out, time-out, or one component of the verification tool giving up; in all of these failing cases, significant computation is performed by the verification tool before the failure, but no result is reported. We propose to reformulate the model-checking problem as follows, in order to have the verification tool report a summary of the performed work even in case of failure: given a program and a specification, the model checker returns a condition P ---usually a state predicate--- such that the program satisfies the specification under the condition P ---that is, as long as the program does not leave the states in which P is satisfied. In our experiments, we investigated as one major application of conditional model checking the sequential combination of model checkers with information passing. We give the condition that one model checker produces, as input to a second conditional model checker, such that the verification problem for the second is restricted to the part of the state space that is not covered by the condition, i.e., the second model checker works on the problems that the first model checker could not solve. Our experiments demonstrate that repeated application of conditional model checkers, passing information from one model checker to the next, can significantly improve the verification results and performance, i.e., we can now verify programs that we could not verify before. },
annote = {
},
}
-
Dirk Beyer and Alexander K. Petrenko.
Linux Driver Verification.
In T. Margaria and B. Steffen, editors,
Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA 2012, Part II, Heraklion, Crete, October 15-18),
LNCS 7610,
pages 1-6,
2012.
Springer-Verlag, Heidelberg.
[ PDF
] Keyword(s): Software Model Checking.
@InProceedings{LDV12,
author = {Dirk Beyer and Alexander K. Petrenko},
title = {{Linux} Driver Verification},
booktitle = {Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA~2012, Part II, Heraklion, Crete, October 15-18)},
publisher = {Springer-Verlag, Heidelberg},
editor = {T.~Margaria and B.~Steffen},
series = {LNCS~7610},
pages = {1-6},
year = {2012},
isbn = {},
keyword = {Software Model Checking},
pdf = {http://www.sosy-lab.org/~dbeyer/Publications/2012-ISOLA.Linux_Driver_Verification.pdf},
url = {},
abstract = { },
annote = {
},
}
-
Dirk Beyer and Philipp Wendler.
Algorithms for Software Model Checking: Predicate Abstraction vs. IMPACT.
In Gianpiero Cabodi and Satnam Singh, editors,
Proceedings of the 12th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2012, Cambrige, UK, October 22-25),
pages 106-113,
2012.
FMCAD.
[ PDF
] Keyword(s): Software Model Checking.
@InProceedings{FMCAD12,
author = {Dirk Beyer and Philipp Wendler},
title = {Algorithms for Software Model Checking: Predicate Abstraction vs. {IMPACT}},
booktitle = {Proceedings of the 12th International Conference on Formal Methods in Computer-Aided Design (FMCAD~2012, Cambrige, UK, October 22-25)},
publisher = {FMCAD},
editor = {Gianpiero Cabodi and Satnam Singh},
pages = {106-113},
year = {2012},
isbn = {978-1-4673-4831-7},
keyword = {Software Model Checking},
pdf = {http://www.sosy-lab.org/~dbeyer/Publications/2012-FMCAD.Algorithms_for_Software_Model_Checking.pdf},
url = {},
abstract = { },
annote = {
},
}
-
Falk Howar,
Malte Isberner,
Maik Merten,
Bernhard Steffen,
and Dirk Beyer.
The RERS Grey-Box Challenge 2012: Analysis of Event-Condition-Action Systems.
In T. Margaria and B. Steffen, editors,
Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA 2012, Part I, Heraklion, Crete, October 15-18),
LNCS 7609,
pages 608-614,
2012.
Springer-Verlag, Heidelberg.
[ PDF
] Keyword(s): Software Model Checking.
@InProceedings{RERS12,
author = {Falk Howar and Malte Isberner and Maik Merten and Bernhard Steffen and Dirk Beyer},
title = {The {RERS} Grey-Box Challenge 2012: Analysis of Event-Condition-Action Systems},
booktitle = {Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA~2012, Part I, Heraklion, Crete, October 15-18)},
publisher = {Springer-Verlag, Heidelberg},
editor = {T.~Margaria and B.~Steffen},
series = {LNCS~7609},
pages = {608-614},
year = {2012},
isbn = {},
keyword = {Software Model Checking},
pdf = {http://www.sosy-lab.org/~dbeyer/Publications/2012-ISOLA.The_RERS_Grey-Box_Challenge_2012_Analysis_of_Event-Condition-Action_Systems.pdf},
url = {},
abstract = { },
annote = {
},
}