Skip to main content
Kent Academic Repository

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) (KAR id:58948)


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: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: M. Christaki
Date Deposited: 23 Nov 2016 14:41 UTC
Last Modified: 16 Nov 2021 10:23 UTC
Resource URI: (The current URI for this page, for reference purposes)

University of Kent Author Information

Christakis, Maria.

Creator's ORCID:
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.