<?xml version="1.0" encoding="utf-8"?>
<export-example>
  <doc>
    <id>481</id>
    <completedYear>2017</completedYear>
    <publishedYear>2017</publishedYear>
    <thesisYearAccepted>2017</thesisYearAccepted>
    <language>eng</language>
    <pageFirst/>
    <pageLast/>
    <pageNumber>XXI, 155 S.</pageNumber>
    <edition/>
    <issue/>
    <volume/>
    <type>doctoralthesis</type>
    <publisherName/>
    <publisherPlace/>
    <creatingCorporation/>
    <contributingCorporation/>
    <belongsToBibliography>0</belongsToBibliography>
    <completedDate>2017-06-22</completedDate>
    <publishedDate>2017-06-22</publishedDate>
    <thesisDateAccepted>2017-03-24</thesisDateAccepted>
    <title language="eng">Effective Approaches to Abstraction Refinement for Automatic Software Verification</title>
    <abstract language="eng">This thesis presents various techniques that aim at enabling more effective and more&#13;
efficient approaches for automatic software verification.&#13;
After a brief motivation why automatic software verification is getting ever more&#13;
relevant, we continue with detailing the formalism used in this thesis and on the&#13;
concepts it is built on.&#13;
&#13;
We then describe the design and implementation of the value analysis, an analysis&#13;
for automatic software verification that tracks state information concretely. From&#13;
a thorough evaluation based on well over 4 000 verification tasks from the latest&#13;
edition of the International Competition on Software Verification (SV-COMP), we&#13;
learn that this plain value analysis leads to an efficient verification process for many&#13;
verification tasks, but at the same time, fails to solve other verification tasks due&#13;
to state-space explosion. From this insight we infer that some form of abstraction&#13;
technique must be added to the value analysis in order to also allow the successful&#13;
verification of large and complex verification tasks.&#13;
&#13;
As a solution, we propose to incorporate counterexample-guided abstraction refinement (CEGAR) and interpolation into the value domain. To this end, we design&#13;
a novel interpolation procedure, that extracts from infeasible counterexamples interpolants for the value domain, allowing to form a precision strong enough to exclude&#13;
these infeasible counterexamples, and to make progress in the CEGAR loop. We&#13;
then describe several optimizations and extensions to these concepts, such that the&#13;
value analysis with CEGAR becomes competitive for automatic software verification.&#13;
As the next step, we combine the value analysis with CEGAR with a predicate&#13;
analysis, to obtain a more precise and efficient composite analysis based on CEGAR.&#13;
This composite analysis is indeed on a par with the world’s leading software verification tools, as witnessed by the results of SV-COMP’13 where this approach achieved&#13;
the 2 nd place in the overall ranking.&#13;
&#13;
After having available competitive CEGAR-based analyses for the value domain,&#13;
the predicate domain, and the combination thereof, we then turn our attention to&#13;
techniques that have the goal to make all these CEGAR-based approaches more&#13;
successful. Our first novel idea in this regard is based on the concept of infeasible&#13;
sliced prefixes, which allow the computation of different precisions from a single&#13;
infeasible counterexample. This adds choice to the CEGAR loop, while without this&#13;
enhancement, no choice for a specific precision, i. e., a specific refinement, is possible.&#13;
In our evaluation we show, for both the value analysis and the predicate analysis,&#13;
that choosing different infeasible sliced prefixes during the refinement step leads to&#13;
major differences in verification effectiveness and verification efficiency.&#13;
Extending on the concept of infeasible sliced prefixes, we define several heuristics&#13;
in order to precisely select a single refinement from a set of possible refinements. We&#13;
make this new concept, which we refer to as guided refinement selection, available&#13;
to both the value and predicate analysis, and in a large-scale evaluation we try to&#13;
answer the question which selection technique leads to well suited abstractions and&#13;
thus, to a more effective verification process. Additionally, we present the idea of&#13;
inter-analysis refinement selection, where the refinement component of a composite&#13;
analysis may decide which of its component analyses is best to be refined, and in yet&#13;
another evaluation we highlight the positive effects of this technique.&#13;
&#13;
Finally, we present the results of SV-COMP’16, where the verifier we contributed&#13;
and which is based on the concepts and ideas presented in this thesis achieved the&#13;
1 st place in the category DeviceDriversLinux64.</abstract>
    <identifier type="urn">urn:nbn:de:bvb:739-opus4-4815</identifier>
    <author>Stefan Löwe</author>
    <subject>
      <language>eng</language>
      <type>uncontrolled</type>
      <value>software verification, model checking, counterexample guided abstraction refinement, CEGAR, interpolation, sliced prefixes, refinement selection, value analysis, predicate analysis, CPAchecker, automatic, automated</value>
    </subject>
    <subject>
      <language>deu</language>
      <type>swd</type>
      <value>Programmverifikation</value>
    </subject>
    <collection role="ddc" number="000">Informatik, Informationswissenschaft, allgemeine Werke</collection>
    <collection role="open_access" number="">open_access</collection>
    <collection role="institutes" number="">Fakultät für Informatik und Mathematik</collection>
    <thesisPublisher>Universität Passau</thesisPublisher>
    <thesisGrantor>Universität Passau</thesisGrantor>
    <file>https://opus4.kobv.de/opus4-uni-passau/files/481/Loewe_Stefan__Effective_Approaches_to_Abstraction_Refinement_for_Automatic_Software_Verification.pdf</file>
  </doc>
</export-example>
