Skip to main content

Collaborative Verification and Testing with Explicit Assumptions

Christakis, Maria, Müller, Peter, Wüstholz, Valentin (2012) Collaborative Verification and Testing with Explicit Assumptions. In: 18th International Symposium on Formal Methods, August 27-31, 2012, Paris, France. (doi:10.1007/978-3-642-32759-9_13)

PDF - Author's Accepted Manuscript
Download (405kB) Preview
[img]
Preview
Official URL
http://doi.org/10.1007/978-3-642-32759-9_13

Abstract

Many mainstream static code checkers make a number of compromises to improve automation, performance, and accuracy. These compromises include not checking certain program properties as well as making implicit, unsound assumptions. Consequently, the results of such static checkers do not provide definite guarantees about program correctness, which makes it unclear which properties remain to be tested. We propose a technique for collaborative verification and testing that makes compromises of static checkers explicit such that they can be compensated for by complementary checkers or testing. Our experiments suggest that our technique finds more errors and proves more properties than static checking alone, testing alone, and combinations that do not explicitly document the compromises made by static checkers. Our technique is also useful to obtain small test suites for partially-verified programs.

Item Type: Conference or workshop item (Paper)
DOI/Identification number: 10.1007/978-3-642-32759-9_13
Subjects: Q Science > QA Mathematics (inc Computing science)
Divisions: Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: M. Christaki
Date Deposited: 23 Nov 2016 14:41 UTC
Last Modified: 29 May 2019 18:17 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/58948 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year