obustness Testing of Intermediate Verifier



Introduction {#sec:intro}
============

Automated program verifiers have become complex pieces of software; inevitably, they contain bugs that make them misbehave in certain conditions. *Verification tools need verification too.*

In order to apply verification techniques to program verifiers, we have to settle on the kind of (correctness) properties to be verified. If we simply want to look for basic *programming errors*—such as memory allocation errors, or parsing failures—the usual verification[^1] techniques designed for generic software—from random testing to static analysis—will work as well on program verifiers. Alternatively, we may treat a program verifier as a *translator* that encodes the semantics of a program and specification language into purely logic constraints—which can be fed to a generic theorem prover. In this case, we may pursue a correct-by-construction approach that checks that the translation preserves the intended semantics—as it has been done in few milestone research achievements @compcert [@VeryAnalyzer]@compcert.

There is a third kind of analysis, however, which is peculiar to automated program verifiers that aim at being sound. Such tools input a program complete with specification and other auxiliary annotations, and output either " <span style="font-variant:small-caps;">success</span>" or " <span style="font-variant:small-caps;">failure</span>". Success means that the verifier proved that the input program is correct; but failure may mean that the program is incorrect or, more commonly, that the verifier needs more information to verify the program—such as more detailed annotations. This asymmetry between "verified" and "don't know" is a form of incompleteness, which is inevitable for sound verifiers that target expressive, undecidable program logics. Indeed, using such tools often requires users to become acquainted with the tools' idiosyncrasies, developing an intuition for what kind of information, and in what form, is required for verification to succeed. To put it in another way, program verifiers may exhibit *brittle, or unstable, behavior*: tiny changes of the input program that ought to be inconsequential have a major impact on the effectiveness achieved by the program verifier. For instance, details the example of a small program that passes or fails verification just according to the relative order of two unrelated declarations. Brittle behavior of this kind compromises the usability of verification tools. In this work, we target this kind of *robustness (stability) analysis* of program verifiers. We call an automated verifier *robust* if its behavior is not significantly affected by small changes in the input that should be immaterial. A verifier that is not robust is *brittle* (unstable): it depends on idiosyncratic features of the input. Using brittle verifiers can be extremely frustrating: the feedback we get as we try to develop a verified program incrementally is inconsistent, and we end up running in circles—trying to fix nonexistent errors or adding unnecessary annotations. Besides being a novel research direction for the verification of verifiers, identifying brittle behavior has the potential of helping develop more robust tools that are ultimately more usable.

More precisely, we apply *lightweight verification techniques* based on *testing*. Testing is a widely used technique that cannot establish correctness but is quite effective at findings bugs.

The goal of our work is to automatically generate tests that reveal brittleness. Using the approach described in detail in , we start from a *seed*: a program that is correct and can be verified by an automated verifier. We *mutate* the seed by applying random sequences of predefined mutation operators. Each mutation operator captures a simple variation of the way a program is written that *does not change its semantics*; for example, it changes the order of independent declarations. Thus, every mutant is a *metamorphic transformation* @metamorphic of the seed—and equivalent to it. If the verifier *fails* to verify a mutant we found a bug that exposes brittle behavior: seed and mutant differ only by small syntactic details that should be immaterial, but such tiny details impact the verifier's effectiveness in checking a correct program.

While our approach to *robustness testing* is applicable in principle to any automated program verifier, the mutation operators depend to some extent on the semantics of the verifier's input language, as they have to be semantic preserving. To demonstrate robustness testing in practice, we focus on the Boogie language @TIB2. Boogie is a so-called *intermediate verification language*, combining an expressive program logic and a simple procedural programming language, which is commonly used as an intermediate layer in many verification tools. Boogie's popularity makes our technique (and our implementation) immediately useful to a variety of researchers and practitioners.

As we describe in , we implemented robustness testing for Boogie in a tool called <span>`\mugie`</span>. In experiments described in , we ran <span>`\mugie`</span>on 135 seed Boogie programs, generating and verifying over mutants. The mutants triggered brittle behavior in 16 of the seed programs; large, feature-rich programs turned out to be particularly brittle, to the point where several different mutations were capable of making Boogie misbehave. As we reflect in , our technique for robustness testing can be a useful complement to traditional testing techniques, and it can help buttress the construction of more robust, and thus ultimately more effective and usable, program verifiers.

<span> ***Tool availability.***</span> The tool <span><span>`\mugie`</span></span>, as well as all the artifacts related to its experimental evaluation, are publicly available @toolSite. A few additional details about the experiments are available in a longer version of this paper @RobustnessIVL-TR-20180509.

Motivating Example {#sec:example}
==================

Let's see a concrete example of how verifiers can behave brittlely. shows a simple Boogie program consisting of five declarations, each listed on a separate numbered line.

\[numbers=left,xleftmargin=20mm\] function h(int) returns (int);\#\[ln:hdecl\]\# axiom (forall x, y: int a67d:ce30:8b00:4856:c02f:75af:3b8:dfd7 x &gt; y ==&gt; h(x) &gt; y);\#\[ln:hdef\]\# const a: \[int\] int;\#\[ln:adecl\]\# axiom (forall i: int a67d:ce30:8b00:4856:c02f:75af:3b8:dfd7 0 &lt;= i ==&gt; a\[i\] &lt; a \[i +$\,$1\]);\#\[ln:adef\]\# procedure p(i: int) returns (o: int) \#\# $\quad$requires i &gt;=$\,$0; ensures o &gt; $\,$a\[i\]; <span> o := $\,$h(a\[i +$\,$1\]); </span>\#\[ln:pdef\]\#

The program introduces an integer function (), whose semantics is partially axiomatized (); a constant integer map (), whose elements at nonnegative indexes are sorted (); and a procedure (, spanning two physical lines in the figure)—complete with signature, specification, and implementation—which returns the result of applying to an element of . Never mind about the specific nature of the program; we can see that procedure is correct with respect to its specification: from the axiom about and 's precondition, and thus from the axiom about . Indeed, Boogie successfully checks that is correct.

There is nothing special about the order of declarations in —after all, "the order of the declarations in a \[Boogie\] program is immaterial" @TIB2 [Sec. 1]. A different programmer may, for example, put 's declarations before 's. In this case, surprisingly, Boogie fails verification warning the user that 's postcondition may not hold.[^2]

A few more experiments show that there's a fair chance of running into this kind of brittle behavior. Out of the $5! = 120$ possible permutations of the 5 declarations in —each an equivalent version of the program—Boogie verifies exactly half, and fails verification of the other half. We could not find any simple pattern in the order of declarations (such as "line $x$ before line $y$") that predicts whether a permutation corresponds to a program Boogie can verify.

The <span><span style="font-variant:small-caps;">smt</span>-<span style="font-variant:small-caps;">lib</span></span> @SMTlib2 files generated by Boogie (encoding the program's correctness conditions in a format understood by SMT solvers) also only differ by the order of declarations and assertions—with additional complications due to the fact that declarations have to come before usage in <span><span style="font-variant:small-caps;">smt</span>-<span style="font-variant:small-caps;">lib</span></span>, and the VCs also include auxiliary functions generated by Boogie. The interplay of Boogie and Z3 determines the brittle behavior we observe in this example: even if it uses a generic format, Boogie's <span><span style="font-variant:small-caps;">smt</span>-<span style="font-variant:small-caps;">lib</span></span>encoding uses plenty of Z3-specific options, but is not always robust in the way it interacts with the solver. To better understand whether other tools' SMT encodings may be less brittle than Boogie's, we used <span>`b2w`</span> @b2w to translate all 120 permutations of to WhyML—the input language of the Why3 intermediate verifier @FilliatreP13. Why3 successfully verified all of them—using Z3 as SMT solver, like Boogie does—which suggests that some features of Boogie's encoding (as opposed to Z3's capabilities) are responsible for the brittle behavior on the example.

Such kinds of brittleness—a program switching from verified to unverified based on changes that should be inconsequential—can greatly frustrate users, and in particular novices who are learning the ropes and may get stuck looking for an error in a program that is actually correct—and could be proved so if definitions were arranged in a slightly different way. Since brittleness hinders scalability to projects of realistic size, it can also be a significant problem for advanced users; for example, the developers behind the Ironclad Apps @Ironclad and IronFleet @IronFleet projects reported[^3] that "solvers' instability was a major issue" in their verification efforts.

<span>-30mm</span><span>-30mm</span>

\[ toolbox/.style=<span>rectangle,minimum width=20mm,minimum height=5mm, very thick,rounded corners=2mm,font=,draw=boogieKW,fill=boogieKW,text=white</span>, databox/.style=<span>font=,minimum width=16mm</span>, outbox/.style=<span>font=,minimum width=6mm</span>, align=center \] ;

\[color=arrowcol,line width=1pt,round cap-latex',shorten &gt;=3pt,shorten &lt;= 4pt,every node/.style=<span>font=</span>\] (seed) – (morph); in <span>1, 2, 22, k, k2, n</span> <span> (morph) – (m.west); (m.east) – (v); (v) – (o.west); </span> (ok) – (found);

How Robustness Testing Works {#sec:how}
============================

Robustness testing is a technique that "perturbs" a correct and verified program by introducing small changes, and observes whether the changes affect the program's verifiability. The changes should be inconsequential, because they are designed not to alter the program's behavior or specification; if they do change the verifier's outcome, we found lack of robustness.

While robustness testing is applicable to any automated program verifier, we focus the presentation on the popular Boogie intermediate verification language. Henceforth, a "program" is a program (complete with specification and other annotations) written in the Boogie language. illustrates how robustness testing works at a high level; the rest of the section provides details.

In general terms, testing requires to build a valid *input*, feed it to the system under test, and compare the system's output with the *expected* output—given by a testing *oracle*. Testing the behavior of a verifier according to this paradigm brings challenges that go beyond those involved in generating tests for general programs. First, a verifier's input is a whole *program*, complete with specification and other annotations (such as lemmas and auxiliary functions) for verification. Second, robustness testing aims at exposing subtle inconsistencies in a verifier's output, and not basic programming errors—such as memory access errors, parsing errors, or input/output errors—that every piece of software might be subject to. Therefore, we need to devise suitable strategies for *input generation* and *oracle generation*.

Mutation Operators
------------------

<span>**Input generation.**</span> In order to expose brittleness of verifiers, we need to build complex input programs of significant size, complete with rich specifications and all the annotations that are necessary to perform automated verification. While we may use grammar-based generation techniques @csmith to automatically build syntactically correct Boogie programs, the generated programs would either have trivial specifications or not be semantically correct—that is, they would not pass verification. Instead, robustness testing starts from a collection of *verified programs*—the *seeds*—and automatically generates simple, semantically equivalent variants of those programs.[^4] This way, we can seed robustness testing with a variety of sophisticated verification benchmarks, and assess robustness on realistic programs of considerable complexity.

<span>**Mutation operators.**</span> Given a seed $s$, robustness testing generates many variants $M(s)$ of $s$ by "perturbing" $s$. Building on the basic concepts and terminology of mutation testing @mutation [@mutationSurvey]@mutationSurvey,[^5] we call *mutant* each variant $m$ of a seed $s$ obtained by applying a random sequence of *mutation operators*.

A mutation operator captures a simple syntactic transformation of a Boogie program; crucially, mutation operators should *not change a program's semantics* but only introduce equivalent or redundant information. Under this fundamental condition, every mutant $m$ of a seed $s$ is equivalent to $s$ in the sense that $s$ and $m$ should both pass (or both fail) verification. This is an instance of *metamorphic testing*, where we transform between equivalent inputs so that the seed serves as an oracle to check the expected verifier output on all of the seed's mutants.

<span>\*<span>3</span><span>p<span>0.32</span></span></span> & &\

1.  \[m:S1\] Swap any two declarations

2.  \[m:S5\] Split a procedure definition into declaration and implementation

3.  \[m:S6\] Move any declaration into a separate file (and call Boogie on both files)

&

1.  \[m:L1\] Swap any two local variable declarations

2.  \[m:L2\] Split a declaration of multiple variables into multiple declarations

3.  \[m:L4\] Join any two preconditions into a conjunctive one

4.  \[m:L5\] Join any two postconditions into a conjunctive one

5.  \[m:L6\] Swap any two pre-/postcondition, intermediate assertion, or loop invariant clauses

6.  \[m:L8\] Complement an condition and switch its and branches

&

1.  \[m:G1\] Add as pre-/postcondition, intermediate assertion, or loop invariant clause

2.  \[m:G2\] Remove a trigger annotation

Based on our experience using Boogie and working around its brittle behavior, we designed the mutation operators in , which exercise different language features:

Structural

:   mutation operators change the overall structure of top-level declarations—by changing their relative order (\[m:S1\]), separating declarations and implementations (\[m:S5\]), and splitting into multiple files (\[m:S6\]).

Local

:   mutation operators work at the level of procedure bodies—by changing the relative order of or splitting on multiple lines local variable declarations (\[m:L1\] and \[m:L2\]), merging two pre- or postcondition clauses and into a conjunctive clause (\[m:L4\] and \[m:L5\]), changing the relative order of assertions of the same program element (\[m:L6\]), and permuting the and branches of a conditional (\[m:L8\]).

Generative

:   mutation operators alter redundant information—by adding trivial assertions (\[m:G1\]), and removing quantifier instantiation suggestions ("triggers" in \[m:G2\]).

We stress that our mutation operators do not alter the semantics of a Boogie program according to the language's specification @TIB2: in Boogie, the order of declarations is immaterial (\[m:S1\], \[m:L1\], \[m:L2\]); a procedure's implementation may be with its declaration or be separate from it (\[m:S5\]); multiple input files are processed as if they were one (\[m:S6\]); multiple specification elements are implicitly conjoined, and their relative order does not matter (\[m:L4\], \[m:L5\], \[m:L6\]); a conditional's branches are mutually exclusive (\[m:L8\]); and assertions are irrelevant since Boogie only checks partial correctness (\[m:G1\]).

<span>**Triggers.**</span> \[m:G2\] is the only mutation operator that may alter the semantics of a Boogie program in practice: while triggers are suggestions on how to instantiate quantifiers, they are crucial to guide SMT solvers and increase stability in practice @triggerSelection [@blt]. Therefore, **we do not consider \[m:G2\] semantics-preserving**; our experiments only apply \[m:G2\] in a separate experimental run to give an idea of its impact in isolation.

More mutation operators are possible, but the selection in should strike a good balance between effectiveness in setting off brittle behavior and feasibility of studying the effect of each individual operator in isolation.

<span>**Example.**</span> In the example of , the program in is a possible seed—a correct Boogie program that verifies. Applying mutation operator \[m:S1\] twice—first to lines , , and then to lines , —generates a mutant where 's declarations come before . As discussed in , this mutant fails verification even if it is equivalent to the seed.

\[!bt\]

$M \gets \{ s \}$ attempts $\gets 0$

()<span>$|M| < N_M$</span><span> attempts $\gets$ attempts $+$ 1 </span>

Mutation Generation
-------------------

Given a seed $s$, the generation of mutants repeatedly draws random mutation operators and applies them to $s$, or to a previously generated mutant of $s$, until the desired number $N_M$ of mutants is reached.

Alg. \[alg:mugen\] shows the algorithm to generate mutants. The algorithm maintains a pool $M$ of mutants, which initially only includes the seed $s$. Each iteration of the main generation loop proceeds as follows:

pick a random program $p$ in the pool $M$;

select a random mutation operator $o$;

apply $o$ to $p$, giving mutant $m$;

add $m$ to pool $M$ (if it is not already there).

Users can bias the random selection of mutation operators by assigning a weight $w(o)$ to each mutation operator $o$ in : the algorithm draws an operator with probability proportional to its weight, and operators with zero weight are never drawn.

Besides the mutation operator selection, there are two other passages of the algorithm where random selection is involved: a program $p$ is drawn uniformly at random from $M$; and applying an operator $o$ selects uniformly at random program locations where $o$ can be applied. For example, if $o$ is \[m:S1\] (swap two top-level declarations), applying $o$ to $p$ involves randomly selecting two top level declarations in $p$ to be swapped.

Any mutation operator can generate only finitely many mutants; since the generation is random, it is possible that a newly generated mutant is identical to one that is already in the pool. In practice, this is not a problem as long as the seed $s$ is not too small or the enabled operators too restrictive (for example, \[m:S5\] can only generate $2^D$ mutants, where $D$ is the number of procedure definitions in $s$). The generation loop has an alternative stopping conditions that gives up after MAX\_ATTEMPTS iterations that have failed to generate enough distinct mutants.

<span>**Robustness testing.**</span> After generating a set $M(s)$ of mutants of a seed $s$, robustness testing runs the Boogie tool on each mutant in $M(s)$. If Boogie can verify $s$ but fails to verify any mutant $m \in M(s)$, we have found an instance of *brittle behavior*: $s$ and $m$ are equivalent by construction, but the different form in which $m$ is expressed trips up Boogie and makes verification fail on an otherwise correct program.

Implementation {#sec:implementation}
--------------

We implemented robustness testing as a commandline tool <span>`\mugie`</span>(pronounced "moogie"). <span>`\mugie`</span>implements in Haskell the mutation generation Alg. \[alg:mugen\], and extends parts of Boogaloo's front-end @boogaloo for parsing and typechecking Boogie programs.

Each mutation operator is implemented—using the `lens` Haskell package @haskellLens—as function from Boogie programs to Boogie programs;[^6] With this design, adding new mutation operators or changing their order of application is straightforward as it just uses Haskell's function composition. Upon terminating, <span><span>`\mugie`</span></span>outputs each mutant as a separate file (or files, if \[m:S6\] is applied), and annotates each file with a comment header indicating the seed and the sequence of mutation operators that were applied to generate the mutant from the seed.

<span>**Pretty printing.**</span> <span>`\mugie`</span>represents programs by their abstract syntax trees, which are then rendered using concrete syntax when all mutants have been generated. Such a pretty printing may introduce small syntactic changes—when the same abstract syntax can be rendered using different syntactic forms. Besides obvious changes in white spaces, line breaks, and comments (which are removed), <span><span>`\mugie`</span></span>'s pretty printer may introduce one normalizing change: functions and procedures without return clause in their signature get an explicit clause. To further ensure no implicit transformation is added during pretty printing, we also checked that pretty printing has no effect on the behavior of Boogie programs (that is, a pretty-printed seed verifies iff the original seed also verifies).

Experimental Evaluation {#sec:experiments}
=======================

Robustness testing was initially motivated by our anecdotal experience using intermediate verifiers. To rigorously assess to what extent they are indeed brittle, and whether robustness testing can expose their brittleness, we conducted an experimental evaluation using <span><span>`\mugie`</span></span>. This section describes design and results of these experiments.

Experimental Design
-------------------

A run of <span><span>`\mugie`</span></span>inputs a *seed* program $s$ and outputs a number of metamorphic mutants of $s$, which are then verified with some tool $t$ (see ).

<span>**Seed selection.**</span> We prepared a curated collection of seeds by selecting Boogie programs from several different sources, with the goal of having a diverse representation of how Boogie may be used in practice. Each example belongs to one of six groups according to its origin and characteristics; displays basic statistics about them. Group **A** contains basic **A**lgorithms (search in an array, binary search trees, etc.) implemented directly in Boogie in our previous work @FMV-CSUR14; these are relatively simple, but non-trivial, verification benchmarks. Group **T** is a different selection of mainly algorithmic problems (bubble sort, Dutch flag, etc.) included in Boogie's distribution **T**ests. Group **E** consists of small **E**xamples from our previous work @blt that target the impact of different trigger annotations in Boogie. Group **S** collects large Boogie programs that we generated automatically from fixed, repetitive structures (for example, nested conditionals); in previous work @blt we used these programs to evaluate **S**calability. Groups **D** and **P** contain Boogie programs automatically generated by the **D**afny @dafny and Auto**P**roof @FNPT-STTT16 verifiers (which use Boogie as intermediate representation). The Dafny and Eiffel programs they translate come from the tools' galleries of verification benchmarks @dafnyGallery [@autoproofGallery]. As we see from the substantial size of the Boogie programs they generate, Dafny and AutoProof introduce a significant overhead as they include axiomatic definitions of heap memory and complex types. In all, we collected 135 seeds of size ranging from just 6 to over lines of Boogie code for a total of nearly lines of programs and specifications.

\[c\]<span>0.5</span>

\[c\]<span>0.4</span>

  <span style="font-variant:small-caps;">tool</span>             <span style="font-variant:small-caps;">commit</span>   <span style="font-variant:small-caps;">date</span>   <span style="font-variant:small-caps;">z3</span>
  ------------------------------------------------------------ ------------------------------------------------------ ---------------------------------------------------- --------------------------------------------------
  <span style="font-variant:small-caps;">boogie</span> 4.1.1                                                 `b2d448`                                           2012-09-18                                              4.1.1
  <span style="font-variant:small-caps;">boogie</span> 4.3.2                                                 `97fde1`                                           2015-03-10                                              4.3.2
  <span style="font-variant:small-caps;">boogie</span> 4.4.1                                                 `75b5be`                                           2015-11-19                                              4.4.1
  <span style="font-variant:small-caps;">boogie</span> 4.5.0                                                 `63b360`                                           2017-07-06                                              4.5.0

  : Boogie programs ("seeds") and Boogie tool versions used in the experiments.<span data-label="tab:basic-stats"></span>

<span>**Tool selection.**</span> In principle, <span><span>`\mugie`</span></span>can be used to test the robustness of any verifier that can input Boogie programs: besides Boogie, tools such as Boogaloo @boogaloo, Symbooglix @symbooglix, and `blt` @blt. However, different tools target different kinds of analyses, and thus typically require different kinds of seeds to be tested properly and meaningfully compared. To our knowledge, no tools other than Boogie itself support the full Boogie language, or are as mature and as effective as Boogie for sound verification (as opposed to other analyses, such as the symbolic execution performed by Boogaloo and Symbooglix) on the kinds of examples we selected. We intend to perform a different evaluation of these tools using <span><span>`\mugie`</span></span>in the future, but for consistency and clarity we focus on the Boogie tool in this paper.

In order to understand whether Boogie's robustness has changed over its development history, our experiments include different versions of Boogie. The Boogie repository is not very consistent in assigning new version numbers, nor does it tag specific commits to this effect. As a proxy for that, we searched through the logs of Boogie's repository for commit messages that indicate updates to accommodate new features of the Z3 SMT solver—Boogie's standard and main backend. For each of four major versions of Z3 (4.1.1, 4.3.2, 4.4.1, and 4.5.0), we identified the most recent commit that refers explicitly to that version (see ); for example, commit `63b360` says "Calibrated test output to Z3 version 4.5.0". Then, we call "Boogie $v$" the version of Boogie at the commit mentioning Z3 version $v$, running Z3 version $v$ as backend.

To better assess whether brittle behavior is attributable to Boogie's encoding or to Z3's behavior, we included two other tools in our experiments: CVC4 refers to the SMT solver CVC4 v. 1.5 inputting Boogie's SMT2 encoding of verification condition (the same input that is normally fed to Z3); Why3 refers to the intermediate verifier Why3 v. 0.86.3 using Z3 4.3.2 as backend, and inputting WhyML translations of Boogie programs automatically generated by <span>`b2w`</span> @b2w.

<span>-10mm</span><span>5mm</span>

                                                                                <span style="font-variant:small-caps;">definition</span>                                                                                                      <span style="font-variant:small-caps;">description</span>
  ----------------------------------------------------------------------------- ------------------------------------------------------------------------------------------------------------------------------------------------------------- -----------------------------------------------------------------------------------
                                                                            $S$                                                                                                                                                               set of all seeds
                                                                     $M_{O}(s)$                                                                                                                                                               set of all mutants of seed $s$ (generated with mutation operators $O$)
                                         $S_t^{{\text{\color{green}\faCheck}}}$ $\{ s \in S \mid t(s) \}$                                                                                                                                     seeds that pass verification with tool $t$
                                      $M_O(s)^{{\text{\color{red}\faClose}}}_t$ $\{ m \in M_O(s) \mid \neg t(m) \}$                                                                                                                           mutants of seed $s$ that fail verification with tool $t$
    $S_t^{{\text{\color{green}\faCheck}}\leadsto {\text{\color{red}\faClose}}}$ $\{ s \in S_t^{{\text{\color{green}\faCheck}}} \mid |M_O(s)^{{\text{\color{red}\faClose}}}_t| > 0 \}$                                                         passing seeds with at least one mutant failing with tool $t$
                                                            $M_O(s)^{\infty}_t$ $\{ m \in M_O(s)^{{\text{\color{red}\faClose}}}_t \mid t(m) \text{ times out} \}$                                                                             failing mutants of seed $s$ that time out with tool $t$
                          <span style="font-variant:small-caps;">\# pass</span> $|S_t^{{\text{\color{green}\faCheck}}}|$                                                                                                                      number of seeds that pass verification with tool $t$
                 <span style="font-variant:small-caps;">\# $\exists$fail</span> $|S_t^{{\text{\color{green}\faCheck}}\leadsto {\text{\color{red}\faClose}}}|$                                                                                 number of verified seeds with at least one failing mutant with tool $t$
                  <span style="font-variant:small-caps;">% $\exists$fail</span> $100\cdot|S_t^{{\text{\color{green}\faCheck}}\leadsto {\text{\color{red}\faClose}}}|/|S_t^{{\text{\color{green}\faCheck}}}|$                                  percentage of verified seeds with at least one failing mutant with tool $t$
                                                  $\overline{\textsc{\% fail}}$ $100\cdot \textit{mean}_{s \in S_t^{{\text{\color{green}\faCheck}}}} |M_O(s)^{{\text{\color{red}\faClose}}}_t|/|M_O(s)|$                                      average percentage of failing mutants per verified seed with tool $t$
                                               $\overline{\textsc{\% timeout}}$ $100\cdot\textit{mean}_{s \in S_t^{{\text{\color{green}\faCheck}}}}|M_O(s)^{\infty}_t|/|M_O(s)|$                                                              average percentage of timed out mutants per verified seed with tool $t$
                                  $\overline{\textsc{\% }\exists\textsc{fail}}$ $100\cdot\textit{mean}_{s \in S_t^{{\text{\color{green}\faCheck}}\leadsto {\text{\color{red}\faClose}}}}|M_O(s)^{{\text{\color{red}\faClose}}}_t|/|M_O(s)|$   average percentage of failing mutants per verified seed with some failing mutants

  : Definitions and descriptions of the experimental measures reported in .<span data-label="tab:notation"></span>

<span>**Experimental setup.**</span> Each experiment has two phases: first, *generate mutants* for every seed; then, *run Boogie* on the mutants and check which mutants still verify.

For every seed $s \in S$ (where $S$ includes all 135 programs summarized in ), we generate different *batches* $M_O(s)$ of mutants of $s$ by enabling specific mutation operators $O$ in <span><span>`\mugie`</span></span>. Precisely, we generate 12 different batches for every seed:

$M_{*}(s)$

:   consists of 100 different mutants of $s$, generated by picking uniformly at random among all mutation operators in **except** (that is, each mutation operator gets the same positive weight, and gets weight zero);

$M_J(s)$<span>,</span>

:   for $J$ one of the 11 operators in , consists of 50 different mutants of $s$ generated by only applying mutation operator $J$ (that is, $J$ gets a positive weight, and all other operators get weight zero).

Batch $M_*$ demonstrates the effectiveness of robustness testing with general settings; then, the smaller batches $M_J$ focus on the individual effectiveness of one mutation operator at a time. Operator \[m:G2\] is only used in isolation (and not at all in $M_*$) since it may change the semantics of programs indirectly by guiding quantifier instantiation.

Let $t$ be a tool (a Boogie version in , or another verifier). For every seed $s \in S$, we run $t$ on $s$ and on all mutants $M_O(s)$ in each batch. For a run of $t$ on program $p$ (seed or mutant), we write $t(p)$ if $t$ verifies $p$ successfully; and $\neg t(p)$ if $t$ fails to verify $p$ (because it times out, or returns with failure). Based on this basic data, we measure robustness by counting the number of verified seeds whose mutants fail verification: see the measures defined in and the results described in detail in . As an additional check that the mutation operators do not change the semantics of programs, we ascertained that all mutants pass parsing and other syntactic checks.

To reduce the running time in practical usage scenarios, one may stop verification of a seed's mutants as soon as one of them fails verification, or even alternate seed mutation and verification steps to avoid generating mutants after the first failure. In this paper's experiments, however, we decided to run verification exhaustively on every mutant in order to collect detailed information about the effectiveness of robustness testing.

<span>**Running times.**</span> The experiments ran on a Ubuntu 16.04 LTS GNU/Linux box with Intel 8-core i7-4790 timlee@example.com GHz and 16 GB of RAM. Generating the mutants took about 15 minutes for the batch $M_*$ and 10 minutes for each batch $M_J$. Each verification run was given a timeout of 20 seconds, after which it was forcefully terminated by the scheduler of GNU `parallel` @gnuParallel. For replicability, seeds and summary output of the experimental runs are available online @toolSite.

Experimental Results {#sec:results}
--------------------

<span>**Overall results: batch $M_*$.**</span> Our experiments, whose detailed results are in , show that robustness testing is *effective* in exposing *brittle behavior*, which is *recurrent* in Boogie: for 12% of the seeds that pass verification,[^7] there is at least one mutant in batch $M_*$ that fails verification.

Not all seeds are equally prone to brittleness: while on average only 3% of one seed's mutants fail verification, it is considerably easier to trip up seeds that are *susceptible* to brittle behavior (that is such that at least one mutant fails verification): 27% of mutants per such seeds fail verification.

When the verifier times out on a mutant, it may be because:

\[label=*)*\]

\[to:spurious\] the timeout is itself unstable and due to random noise in the runtime environment;

\[to:longer\] the mutant takes longer to verify than the seed, but may still be verified given longer time;

\[to:infinity\] verification time diverges.

We ruled out \[to:spurious\] by repeating experiments 10 times, and reporting a timeout only if all 10 repetitions time out. Thus, we can generally consider the timeouts in indicative of a genuine degrading of performance in verification—which affected 3% of one seed's mutants on average.

<span>**Boogie versions.**</span> There is little difference between Boogie versions, with the exception of Boogie 4.1.1. This older version does not support some language features used extensively in many larger examples that also tend to be more brittle (groups D and P). As a result, the percentage of verified seeds with mutants that fail verification is spuriously lower (4%) but only because the experiments with Boogie 4.1.1 dodged the harder problems and performed similarly to the other Boogie versions on the simpler ones. Leaving the older Boogie version 4.1.1 aside, our experiments leave open the question of whether robustness has significantly improved in recent versions of Boogie.

<span>**Intermediate verifier vs. backend.**</span> Is the brittleness we observed in our experiments imputable to Boogie or really to Z3? To shed light on this question, we tried to verify every seed and mutant using CVC4 instead of Z3 with Boogie's encoding; and using Why3 on a translation @b2w of Boogie's input. Since the seeds are programs optimized for Boogie verification, CVC4 and Why3 can correctly process only about half of the seeds that Boogie can. This gives us too little evidence to answer the question conclusively: while both CVC4 and Why3 seem to be more robust than Boogie, they can verify none of the brittle seeds (that is, verified seeds with at least one failing mutant), and thus behave as robustly as Boogie on the programs that both tools can process.[^8] As suggested by the simple example of (where Why3 was indeed more robust than Boogie), it is really the interplay of Boogie and Z3 that determines brittle behavior. While SMT solvers have their own quirks, Boogie is meant to provide a stable intermediate layer; in all, it seems fair to say that Boogie is at least partly responsible for the brittleness.

<span>**Program groups.**</span> Robustness varies greatly across groups, according to features and complexity of the seeds that are mutated. Groups D and P are the most brittle: about 1/3 of passing seeds in D, and about 2/5 of passing seeds in P, have at least one mutant that fails verification. Seeds in D and P are large and complex programs generated by Dafny and AutoProof; they include extensive definitions with plenty of generic types, complex axioms, and instantiations. The brittleness of these programs reflects the hardness of verifying strong specifications and feature-rich programming languages: the Boogie encoding must be optimized in every aspect if it has to be automatically verifiable; even a modicum of clutter—introduced by <span><span>`\mugie`</span></span>—may jeopardize successful verification.

By the same token, groups A, E, and T's programs are more robust because they have a smaller impact surface in terms of features and size. Group S's programs are uniformly robust because they have simple, repetitive structure and weak specifications despite their significant size.

<span>**Mutation operators and batches $M_J$.**</span> and the rightmost columns of explore the relative effectiveness of each mutation operator. , , , and could not generate any failing mutant—suggesting that Boogie's encoding of procedure declarations, of local variables, and of conditionals is fairly robust. In contrast, all other operators could generate at least one failing mutant; indicates that and generated failing mutants for respectively 2 seeds and 1 seed that were robust in batch $M_*$ (using all mutation operators with the same frequency)—indicating that mutation operators are complementary to a certain extent in the kind of brittleness they can expose. Since every seed that $M_*$ trips up can also be tripped up by a single operator, combining multiple mutation operators does not seem to be necessary for successful robustness testing (although predicting which operators will be effective may be hard).

gives information about the frequency of different mutation operators in failing mutants of batch $M_*$. Differences are consistent with the results of batches $M_J$—which provide more direct evidence. As usual, the numbers for Boogie 4.1.1 are different because of a much smaller number of passing seeds on which the statistics are computed, which in turn is a result of Boogie 4.1.1's more limited supported features.

<span>**Failures.**</span> Overall, 13 brittle seeds are revealed by 350 failing mutants in $M_*$ with Boogie 4.5.0. Failures are of three kinds:

\[label=*)*\]

timeouts (6 seeds, 252 mutants);

type errors (5 seeds, 10 mutants);

explicit verification failures (2 seeds, 88 mutants).

*Timeouts*

:   *Timeouts* mainly occur in group D (5 seeds), where size and complexity of the code are such that any mutation that slows down verification may hit the timeout limit; verification of some mutants seems to be non-terminating, whereas others are just slowed down by some tens of seconds. One exception is in group T, whose implementation of a queue in the style of dynamic frames is not particularly large (322 lines) but includes many assertions that take time to verify. Some mutants verify if given longer time; in fact, group T's programs are otherwise very robust, probably because they are part of Boogie's test suite, and thus any change in Boogie is checked against the same examples to ensure they still verify.

*Type errors*

:   *Type errors* all occur in group P and only when mutation \[m:S6\] splits the seed in a way that procedure (part of AutoProof's heap axiomatization) ends up being declared after its first usage; in this case, Boogie cannot correctly instantiate the procedure's generic type, which triggers a type error even before Z3 is involved. Even though AutoProof's heap encoding is based on Dafny's and hence somewhat similar to it, Dafny is immune to such faulty behavior.

*Verification failures*

:   *Verification failures* occur in seeds of group A and D. In particular, a binary search tree implementation in group A fails verification when the relative order of two postconditions is swapped by \[m:L6\]; while Why3 cannot prove the whole example, it can prove the brittle procedure alone regardless of the postcondition order. Group D's solution to problem 3 in the VerifyThis 2015 competition @VT15 fails verification when two preconditions are merged into a conjunctive one by \[m:L4\].

In all, it is clear that Boogie's encoding is quite sensitive to the order of declarations and assertions even when it should not matter.

<span>**Triggers.**</span> Remember that mutation operator \[m:G2\] is the only one that modifies triggers, and was only applied in isolation in a separate set of experiments. As we expected from previous work @triggerSelection, altering triggers is likely to make verification fail (30 seeds and 276 mutants overall; 20 seeds are only brittle if triggers are modified); most of these failures (26 seeds and 250 mutants) are timeouts, since removing triggers is likely to at least slow down verification—if not make it diverge. Operator \[m:G2\] is very effective at exposing brittleness mainly with the complex examples in groups D and P, which include numerous axioms and extensive quantification patterns. Group E's programs are a bit special because they are brittle—they are designed to be so—but are only affected by mutation operators that remove the trigger annotations on which they strongly depend; in contrast, they are robust against all other mutation operators.

<span>**Failing seeds.**</span> is the counterpart of , showing if random mutations may change a seed that fails verification into one that passes it. Unsurprisingly, this does not happen very often: there are only 2 seeds that go from failing to passing with random mutations. One in group E is similar to the example of but where the seed's order of declarations fails verification, and swapping two of them restores verifiability; one in group P is , which robustly verifies with Boogie 4.3.2 but times out with more recent Boogie versions. AutoProof's encoding was fine-tuned based on Boogie 4.3.2, which explains why it may be sensitive to using newer Boogie versions.

Related Work {#sec:related}
============

<span>**Robustness.**</span> This paper's robustness testing aims at detecting so-called *butterfly effects* @triggerSelection—macroscopic changes in a verifier's output in response to minor modifications of its input. Program provers often incur volatile behavior because they use automated theorem provers—such as SMT solvers—which in turn rely on heuristics to handle efficiently, in many practical cases, complex proofs in undecidable logics. Matching triggers—heuristics to guide quantifier instantiation—are especially prone to misfire in response to tiny changes in the input, as observed in previous work @triggerSelection [@blt] and confirmed by our experiments in .

The notion of robustness originates from dynamical systems theory @FMMR-TimeBook-12 [@Kha95]. While robustness is well understood for linear systems, *nonlinear* systems may manifest unpredictable loss of robustness that are hard to analyze and prevent. In this context, real time temporal logics have been proposed as a way of formalizing and analyzing behavioral properties that are satisfied robustly @FainekosP09.

<span>**Random testing.**</span> Our approach uses *testing* to expose brittle behavior of verifiers. While testing can only try out finitely many inputs—and thus can only prove the presence of errors, as remarked in one of Dijkstra's most memorable quotes @dijkstra1970notes—it is an invaluable analysis techniques, which requires relatively little effort to be applied. By automatically generating test inputs, *random testing* has proved to be extremely effective at detecting subtle errors in programs completely automatically. Random testing can generate instances of complex data types by recursively building them according to their inductive structure—as it has been done for functional @QuickCheck [@FetscherCPHF15]@QuickCheckand object-oriented @Randoop [@AutoTest]@Randoopprogramming languages. Random testing has also been successfully applied to security testing—where it is normally called "fuzzing" @GodefroidLM12—as well as to compiler testing @csmith [@LeAS14]@csmith—where well-formed programs are randomly generated according to the input language's grammar.

<span>**Mutation testing.**</span> This paper's robustness testing is a form of random testing, in that it applies random mutation operators to transform a program into an equivalent one. The terminology and the idea of applying mutation operators to transform between variants of a program come from *mutation testing* @mutationSurvey. However, the goals of traditional mutation testing and of this paper's robustness testing are specular. Mutation testing is normally used to assess the robustness of a test suite—by applying error-inducing mutations to correct programs, and ascertaining whether the tests fail on the mutated programs. In contrast, we use mutation testing to assess the *robustness of a verifier*—by applying semantic-preserving mutations to correct (verified) programs, and ascertaining whether the mutated programs still verify. Therefore, the mutation operators of standard mutation testing introduce bugs in a way that is representative of common programming mistakes; the mutation operators of robustness testing (see ) do not alter correctness but merely represent alternative syntax expressing the same behavior in a way that is representative of different styles of programming.

<span>**Metamorphic testing.**</span> In testing, generating inputs is only half of the work; one also has to compare the system's output with the *expected output* to determine whether a test is passing or failing. The definition of correct expected output is given by an *oracle* @BarrHMSY15. The more complex the properties we are testing for, the more complex the oracle: a crash oracle (did the program crash?) is sufficient to test for simple errors such as out-of-bound memory access; finding more complex errors requires some form of *specification* @HieronsBBCDDGHKKLSVWZ09 of expected behavior—for example in the form of assertions @Korat [@PFPWM-ICSE13].

Even when directly building an oracle is as complex as writing a correct program, there are still indirect ways of extrapolating whether an output is correct. In *differential testing* @differentialTesting, there are variants of the program under test; under the assumption that not all variants have the same bugs, one can feed the same input to every variant, and stipulate that the output returned by the majority is the expected one—and any outlier is likely buggy. Differential testing has been applied to testing compilers @csmith, looking for the compiler that generates the executable that behaves differently from the others on the same input. In *metamorphic testing* @metamorphic [@metamorphicSurvey]@metamorphicSurvey, an input is transformed into an equivalent one according to *metamorphic relations* (for example, the inputs $x$ and $-x$ should be equivalent inputs to a function computing the absolute value); equivalent inputs that determine different outputs are indicative of error. Our robustness testing applies mutation operators that determine identity metamorphic relations between Boogie programs, since they only change syntactic details and not the semantics of programs.

Discussion and Future Work {#sec:discussion}
==========================

Our experiments with <span><span>`\mugie`</span></span>confirm the intuition—bred by frequently using it in our work—that Boogie is prone to brittle behaviour. How can we shield users from this brittle behavior, thus improving the usability of verification technology?

Program verifiers that use Boogie as an intermediate representation achieve this goal to some extent: the researchers who built the verifiers have developed an intuitive understanding of Boogie's idiosyncrasies, and have encoded this informal knowledge into their tools. End users do not have to worry about Boogie's brittleness but can count on the tools to provide an encoding of their input programs that has a good chance of being effective. In contrast, developers of program verifiers still have to know how to interact with Boogie and be aware of its peculiarities.

Robustness testing may play a role not only in exposing brittle behavior—the focus of this paper—but in precisely tracking down the sources of brittleness, thus helping to debug them. To this end, we plan to address *minimization* and *equivalency detection* of mutants in future work. The idea is that the number of failing mutants that we get by running <span><span>`\mugie`</span></span>are not directly effective as debugging aids, because it takes a good deal of manual analysis to pinpoint the precise sources of failure in large programs with several mutations. Instead, we will apply techniques such as delta debugging @deltaDebug to reduce the size of a failing mutant as much as possible while still triggering failing behavior in Boogie. Failing mutants of minimal size will be easier to inspect by hand, and thus will point to concrete aspects of the Boogie translation that could be made more robust.

To further investigate to what extent it is Z3 that is brittle, and to what extent it is Boogie's encoding of verification condition—an aspect only partially addressed by this paper's experiments—we will apply robustness testing directly to SMT problems, also to understand how Boogie's encoding can be made more robust.

Robustness testing could become a useful technique for developers working on different layers of verification infrastructure, to help them track down sources of brittleness during development and ultimately making verification technology easier to use and more broadly applicable.

[^1]: In this paper, the term "verification" also designates *validation* techniques such as testing.

[^2]: The first author found out this at the most inappropriate of times—during a live demo!

[^3]: By an anonymous reviewer of FM 2018.

[^4]: @RobustnessIVL-TR-20180509 describes some experiments with seeds that *fail* verification. Unsurprisingly, random mutations are unlikely to turn an unverified program into a verified one—therefore, the main paper focuses on using verified programs as seeds.

[^5]: See for a discussion of how robustness testing differs from traditional mutation testing.

[^6]: Precisely, the input domain also includes a random seed to select the program elements to which the operator is applied.

[^7]: For clarity, we initially focus on Boogie 4.5.0, and later discuss differences with other versions.

[^8]: Additionally, Why3 times out on 51 mutants of 2 seeds in group S; this seems to reflect an ineffective translation performed by <span>`b2w`</span> @b2w rather than brittleness of Why3.

{'source': 'arXiv_out/1805'}