Bug hunting with false negatives

J.R. Calamé, N. Ioustinova, J.C. Pol, van de, N. Sidorova

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

91 Downloads (Pure)


Safe data abstractions are widely used for verification purposes. Positive verification results can be transferred from the abstract to the concrete system. When a property is violated in the abstract system, one still has to check whether a concrete violation scenario exists. However, even when the violation scenario is not reproducible in the concrete system (a false negative), it may still contain information on possible sources of bugs. Here, we propose a bug hunting framework based on abstract violation scenarios. We first extract a violation pattern from one abstract violation scenario. The violation pattern represents multiple abstract violation scenarios, increasing the chance that a corresponding concrete violation exists. Then, we look for a concrete violation that corresponds to the violation pattern by using constraint solving techniques. Finally, we define the class of counterexamples that we can handle and argue correctness of the proposed framework. Our method combines two formal techniques, model checking and constraint solving. Through an analysis of contracting and precise abstractions, we are able to integrate overapproximation by abstraction with concrete counterexample generation.
Originele taal-2Engels
TitelProceedings of the 6th International Conference on Integrated Formal Methods (IFM 2007) 2-5 July 2007, Oxford, United Kingdom
RedacteurenJ. Davies, J. Gibbons
Plaats van productieBerlin, Germany
ISBN van geprinte versie978-3-540-73209-9
StatusGepubliceerd - 2007
Evenementconference; IFM 2007, Oxford, United Kingdom; 2007-07-02; 2007-07-05 -
Duur: 2 jul. 20075 jul. 2007

Publicatie series

NaamLecture Notes in Computer Science
ISSN van geprinte versie0302-9743


Congresconference; IFM 2007, Oxford, United Kingdom; 2007-07-02; 2007-07-05
AnderIFM 2007, Oxford, United Kingdom


Duik in de onderzoeksthema's van 'Bug hunting with false negatives'. Samen vormen ze een unieke vingerafdruk.

Citeer dit