Bug Hunting with False Negatives

Jens Calamé, Natalia Ioustinova, Jan Cornelis van de Pol, Natalia Sidorova

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    Abstract

    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.
    Original languageUndefined
    Title of host publicationIntegrated Formal Methods
    EditorsJ. Davies, J. Gibbons
    Place of PublicationBerlin
    PublisherSpringer
    Pages98-117
    Number of pages20
    ISBN (Print)978-3-540-73209-9
    DOIs
    Publication statusPublished - Jul 2007

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    NumberLNCS4549
    Volume4591
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Keywords

    • FMT-MC: MODEL CHECKING
    • EWI-11288
    • METIS-242020
    • IR-61979
    • CR-D.2.5

    Cite this

    Calamé, J., Ioustinova, N., van de Pol, J. C., & Sidorova, N. (2007). Bug Hunting with False Negatives. In J. Davies, & J. Gibbons (Eds.), Integrated Formal Methods (pp. 98-117). (Lecture Notes in Computer Science; Vol. 4591, No. LNCS4549). Berlin: Springer. https://doi.org/10.1007/978-3-540-73210-5_6
    Calamé, Jens ; Ioustinova, Natalia ; van de Pol, Jan Cornelis ; Sidorova, Natalia. / Bug Hunting with False Negatives. Integrated Formal Methods. editor / J. Davies ; J. Gibbons. Berlin : Springer, 2007. pp. 98-117 (Lecture Notes in Computer Science; LNCS4549).
    @inproceedings{1fb343c6ee134494ba60bbc72f742efa,
    title = "Bug Hunting with False Negatives",
    abstract = "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.",
    keywords = "FMT-MC: MODEL CHECKING, EWI-11288, METIS-242020, IR-61979, CR-D.2.5",
    author = "Jens Calam{\'e} and Natalia Ioustinova and {van de Pol}, {Jan Cornelis} and Natalia Sidorova",
    note = "10.1007/978-3-540-73210-5_6",
    year = "2007",
    month = "7",
    doi = "10.1007/978-3-540-73210-5_6",
    language = "Undefined",
    isbn = "978-3-540-73209-9",
    series = "Lecture Notes in Computer Science",
    publisher = "Springer",
    number = "LNCS4549",
    pages = "98--117",
    editor = "J. Davies and J. Gibbons",
    booktitle = "Integrated Formal Methods",

    }

    Calamé, J, Ioustinova, N, van de Pol, JC & Sidorova, N 2007, Bug Hunting with False Negatives. in J Davies & J Gibbons (eds), Integrated Formal Methods. Lecture Notes in Computer Science, no. LNCS4549, vol. 4591, Springer, Berlin, pp. 98-117. https://doi.org/10.1007/978-3-540-73210-5_6

    Bug Hunting with False Negatives. / Calamé, Jens; Ioustinova, Natalia; van de Pol, Jan Cornelis; Sidorova, Natalia.

    Integrated Formal Methods. ed. / J. Davies; J. Gibbons. Berlin : Springer, 2007. p. 98-117 (Lecture Notes in Computer Science; Vol. 4591, No. LNCS4549).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    TY - GEN

    T1 - Bug Hunting with False Negatives

    AU - Calamé, Jens

    AU - Ioustinova, Natalia

    AU - van de Pol, Jan Cornelis

    AU - Sidorova, Natalia

    N1 - 10.1007/978-3-540-73210-5_6

    PY - 2007/7

    Y1 - 2007/7

    N2 - 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.

    AB - 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.

    KW - FMT-MC: MODEL CHECKING

    KW - EWI-11288

    KW - METIS-242020

    KW - IR-61979

    KW - CR-D.2.5

    U2 - 10.1007/978-3-540-73210-5_6

    DO - 10.1007/978-3-540-73210-5_6

    M3 - Conference contribution

    SN - 978-3-540-73209-9

    T3 - Lecture Notes in Computer Science

    SP - 98

    EP - 117

    BT - Integrated Formal Methods

    A2 - Davies, J.

    A2 - Gibbons, J.

    PB - Springer

    CY - Berlin

    ER -

    Calamé J, Ioustinova N, van de Pol JC, Sidorova N. Bug Hunting with False Negatives. In Davies J, Gibbons J, editors, Integrated Formal Methods. Berlin: Springer. 2007. p. 98-117. (Lecture Notes in Computer Science; LNCS4549). https://doi.org/10.1007/978-3-540-73210-5_6