# F-IDEs with Features and VCs Designed to Assist Human Reasoning When
Verification Fails

Yu-Shan Sun Clemson University
Clemson, SC, USA<EMAIL_ADDRESS>Pennsylvania State University
University Park, PA, USAClemson University
Clemson, SC, USA Daniel Welch Pennsylvania State University
University Park, PA, USA<EMAIL_ADDRESS>Clemson University
Clemson, SC, USA Murali Sitaraman Clemson University
Clemson, SC, USA<EMAIL_ADDRESS>
###### Abstract

This paper summarizes our efforts to aid human reasoning when verification
fails through the use of two distinct Formalization Integrated Development
Environments (F-IDEs) that we have developed. Both environments are modular
and facilitate reasoning about the full behavior of object-based code. The
first environment, referred to as the web-IDE, has been used for several years
to teach aspects of formal specification and verification, including why and
where verification conditions (VCs) arise and how to use them when
verification fails. The second F-IDE, RESOLVE Studio, remains experimental,
but is a more fully-fledged environment backed by a sequent-based VC generator
that produces VCs with fewer extraneous givens. While the environments and VC
generation techniques are necessarily language specific, the principles of
alternative VC generation methods, F-IDE features, and observations about
their impact on novices and experienced users are more generally applicable.

##  1 Introduction

As the importance of tools and environments with features for supporting
software verification is becoming better understood, a variety of systems have
been developed to fill this need. Indeed, the usability of auto-active [21]
specification and verification languages such as Why3 [8], Dafny [20], RESOLVE
[29], and AutoProof [32]—in which users indirectly interact with automated
provers through formal contracts such as loop invariants—hinge almost entirely
on the feedback provided to users through their respective front-end
environments.

Auto-active style feedback typically takes the form of a collection of
necessary and sufficient verification conditions (VCs) for proving correctness
of code w.r.t. some formal specification. Different tools report (failed) VC
details differently. For example, Dafny tends to report assertion failures
through Z3-generated counter examples [25], whereas AutoProof provides a
higher-level English explanation for each VC. While each tool has its distinct
characteristics, they share the common need of providing effective, non-
ambiguous support to users (preferably of all experience levels) when
verification fails.

The F-IDE contributions of this paper fall under the categorizations of
_usefulness_ and _ease of use_. We consider how VC usefulness is achieved and
how it can be effective. We detail how ease of understanding for a VC is
achieved, focusing, for example, on how reasoning complexity is simplified for
beginners by minimizing givens.

When necessary and sufficient VCs are generated and proved correct, their
details are understandably of little consequence to software engineers. So why
focus on VC generation at all? We consider two reasons. The first is
practical: when verification fails, VCs represent a first, crucial foothold
for novices and experts alike when attempting to identify which fixes are
needed at the source code or specification level. The second reason is
pedagogical: even when verification succeeds—students should be able to
examine the details of a VC, understand which line of code (or construct)
generated it, and why it was provable (e.g., making connections to concepts
learned in discrete math courses). Consequently, easing the human reasoning
process (through simpler, smaller VCs) and supporting student inquiry into
what happens when a program is verified are chief motivations for the
technical VC generation enhancements and tool features discussed in this
paper.

We highlight aspects of two F-IDEs that we have built as the primary means of
viewing VCs, proving, and debugging code that has failed to verify. The
language targeted by both environments is RESOLVE [29]—an integrated
specification and programming language that is imperative and object-based.
The language—with variants adapted to popular languages such as C++ and Java
[15]—has been used to teach modeling and reasoning principles (such as Design
by Contract) from beginning undergraduate CS education to graduate level
courses. Over 25,000 students across multiple institutions have benefited from
from these efforts over two decades [6, 15, 16].

Figure 1: RESOLVE’s web-based F-IDE (top), and RESOLVE Studio (bottom).

The older of the two environments is the web-IDE (Fig. 1, top), which has been
in use for over a decade as the primary development environment for
RESOLVE.111https://resolve.cs.clemson.edu/teaching The second, more recent
F-IDE is a desktop based environment named RESOLVE Studio (Fig. 1, bottom).
Built on top of the JetBrains IDE platform,222https://www.jetbrains.com/
RESOLVE Studio combines the usual modern IDE amenities with a version of the
RESOLVE compiler that includes the revised VC generation scheme detailed in
this paper. Additionally, in an effort to guide the design and application of
proof rules, RESOLVE Studio allows users to interactively derive VCs from
Hoare style triples. While this environment remains under development, it has
seen some usage (albeit limited) in a graduate programming languages course to
construct specifications using small, student-defined mathematical theories.
The contributions of this paper are twofold:

  * •

A general demonstration of how specification and auto-active verification of
software can be supported in the context of two F-IDEs.

  * •

A revised set of proof rules for generating sequent-based VCs in a
parsimonious manner that omits irrelevant givens with the intent of improving
human reasoning and VC comprehension.

The paper is organized as follows. Section 2 provides background on the
RESOLVE language. Section 3 illustrates the need for simpler VCs by examining
a failed VC in an older version of our web-IDE. Section 4 provides a high
level overview of RESOLVE’s VC generation process, while section 5 details the
proof rules that enable generation of parsimonious VCs. Section 6 shows VC
feedback and other features in RESOLVE Studio. Sections 7 \- 9 contain
respectively: an experimental evaluation of the revised proof rules, related
work, and conclusions with directions for future work.

##  2 RESOLVE Background

RESOLVE [29] is an imperative, object-based programming and specification
framework designed to support modular verification of sequential code. Every
RESOLVE component has a formal interface specification called a Concept. Below
is a snippet of one such concept for bounded queues.

⬇

Concept Queue_Template (type Entry; evaluates Max_Length : Integer);

requires Max_Length > 0;

uses String_Theory;

Type family Queue is modeled by Str(Entry);

exemplar Q;

constraints |Q| \leq Max_Length;

initialization ensures Q = $\Lambda$; // note: Q = \Lambda implies |Q| = 0

The concept shown is parameterized by a generic type Entry and an integer
Max_Length that places an upper bound on the number of entries that can be
stored. This bound must be positive (as per the module level requires clause)
and may be an arbitrary expression of type Integer (as per the evaluates
parameter mode). The imported module, String_Theory, gives the concept access
to a mathematical theory of strings—including operators for: string length
$|\bullet|$, concatenation $\circ$, the empty string $\Lambda$, and a
singleton string formation function $\langle\bullet\rangle$.

###  2.1 Abstract Specification

Specifications in RESOLVE are model-based: that is, each programmatic type is
conceptualized through the Type family construct, which, in this case,
declares that the (program) type Queue is mathematically modeled as a string
of generic entries, i.e.: Str(Entry). The exemplar queue, Q, that follows
gives specifiers a formal name to an example queue within the declaration. It
is used immediately thereafter in the constraints to assert that (1) not all
strings are models of valid queues, but only those of length Max_Length or
less, and (2) that queues are empty upon initialization.

Operations are declared after the model. Below is one such operation for
Enqueue.

⬇

Operation Enqueue (alters e : Entry; updates Q : Queue);

requires |Q| < Max_Length;

ensures Q = #Q $\circ$ $\langle$#e$\rangle$;

Formal contracts for Enqueue are communicated through requires and ensures
clauses (i.e.: pre- and post-conditions). The contract also encompasses
specification parameter modes. A mode of updates means that while the value of
the incoming queue (#Q) may be meaningful, its outgoing value (Q) is to be
updated in the manner specified in the ensures clause. The ensures clause can
be read as follows: “the outgoing value of Q is equal to the #-denoted
incoming queue concatenated with the singleton string containing the incoming
value of entry e.” The alters mode means that the incoming #e may contain a
meaningful value, but its outgoing value e is left unspecified. This gives
implementers of the Enqueue operation the most flexibility as to which value
is stored in the parameter e after a call to Enqueue completes.

To facilitate modular reasoning, the language enforces a strict separation
between the abstract state expressed in interface specifications and
executable, implementation level code. Thus, implementations must provide the
correspondence information (abstraction functions or relations) necessary to
connect the concrete state (in the implementation) to the abstract state (in
the interface). Readers interested in a more complete description of RESOLVE
should consult [12, 14, 29, 30] or one of the case studies [23, 31, 35]
carried out using the language.

##  3 The Need for Simpler VCs: Examining a Failed VC

While even modest enhancements made to our presentation of VCs (e.g.,
annotating the source of VCs next to the line(s) on which they arise) have
helped, the complexity of debugging VCs for beginners is considerably
increased when they include a large, obfuscating number of irrelevant givens.

Figure 2: A VC that fails to prove that stack S is restored; note: the version
of RESOLVE pictured does not accept non-ASCII notations—so Empty_String is
used instead of $\Lambda$, <..> instead of $\langle..\rangle$, etc.

For illustration purposes, Fig. 2 shows a buggy implementation of a Do_Nothing
operation on stacks333Stacks and queues are modeled the same—though their
operations (and specs.) differ which requires |S| >= 1, but fails to verify
since the last call to Push is commented out. In this case, the failed VC was
attempting to prove that S had been restored to its original state—as per the
restores parameter mode on S which automatically adds S = #S as a conjunct to
Do_Nothing’s ensures clause. After pressing the MP-Prove button, VCs are
generated for pre-conditions of invoked operations, in addition to the post-
condition of the operation being proved. Givens added to each VC arise from
module level requires clauses and external constraints from imported modules.

The process is completed when all VCs are verified or the system times out.
Since many initial student attempts contain errors and fail to verify, to
provide quicker feedback, the timeout has been set to be minimal on the web-
IDE at the risk of not being able to discharge some otherwise provable VCs.
Further, once at least three VCs fail to prove, the other VCs are not
attempted. Hovering over the orange VC badges on specific lines gives
information about the source of the VC(s) that arise from that line.

##  4 VC Generation Process

Generation of VCs that are both necessary and sufficient in order to prove
that an implementation is correct w.r.t. its specification is a syntax-
directed process. A more detailed description of RESOLVE’s VC-derivation
scheme and its proof rules can be found in [14, 30].

Prior to the application of any statement level proof rules is a pre-
processing step in which user code is logically grouped into assertive-code
blocks wherein all mathematical assertions are made explicit. The traditional
Hoare triple of the form $\\{P\\}\ c\ \\{Q\\}$ looks like the following in our
presentation, as assertive code may include any number of preceding statements
or assertions such as Assume $P$:

$\displaystyle\mathcal{C}\ \text{\textbackslash}\ \
\mathit{c};\quad\texttt{{Confirm}}\ Q;$

Here, $\mathcal{C}$ is a context containing a collection of typed symbols,
$\mathit{c}$ is a sequence of zero or more program statements, and $Q$ is an
assertion that must be confirmed to hold at the end.

Throughout the remainder of the paper, we employ a san-serif style font when
typesetting the names of proof rules, as well as any meta-operators we define
along the way.

###  4.1 Abstract Syntax

RESOLVE’s specification language is built on a many-sorted first order logic
organized into several constituent parts. First, we assume an initial set of
sort symbols $\mathsf{S}=\\{\mathtt{SSet},..\\}\cup\\{\mathbb{B}\\}$. Here,
SSet is the proper class of sets and the notation $T:\mathtt{SSet}$ introduces
a new user defined sort $T$ into context.

  * •

A set $\mathcal{T}$ of nullary constants
$c_{\\_}1,..,c_{\\_}n:T\in\mathcal{T}$ where $c_{\\_}1,c_{\\_}n$ could also
have any other sorts in $\mathsf{S}$.

  * •

A set $\mathcal{X}$ of variables $x,y,z:T\in\mathcal{X}$ representing
arbitrary elements which range over a domain $T$.

  * •

A set $\mathcal{F}$ of typed function symbols $f,g,..,h:T_{\\_}1\times..\times
T_{\\_}n\rightarrow T$ which range over $\mathcal{F}$. Here
$T_{\\_}1\times..\times T_{\\_}n$ represents the domain, while the (non-
subscripted) $T$ represents the co-domain.

  * •

Lastly, a set $\mathcal{P}$ of predicate symbols
$p,q,..,r:T_{\\_}1\times..\times T_{\\_}n\rightarrow\mathbb{B}$; which also
includes a reserved binary predicate for equality ($=$) as well as nullary
predicate symbols for true and false. We denote the arity of a given function
or predicate $o$ as $\mathsf{ar}(o)$.

These sets constitute the language’s vocabulary
$\mathcal{V}=\mathcal{T}\cup\mathcal{X}\cup\mathcal{F}\cup\mathcal{P}$; where
$\mathcal{V}$ can be enriched via the definition of new constants, functions,
and predicates in RESOLVE’s object theories. As a result, these sets are not
necessarily disjoint in practice. So determining whether a nullary “symbol”
denotes a variable (e.g, bound under a quantifier) or the name of a module
level definitional constant is dependent on the current context,
$\mathcal{C}$. With these categories fixed, we now define formulas (which
denote truth values) and terms (which serve as the fundamental building blocks
of formulas).

######  Definition 4.1.

The set of formulas and terms of our specification language over vocabulary
$\mathcal{V}$ is given by the following abstract syntax.

$\displaystyle\mathbf{Form}_{\\_}{\mathcal{V}}\ni\phi,\psi::=P(t_{\\_}1,..,t_{\\_}{\mathsf{ar}(P)})\
|\ \mathit{true}\ |\ \mathit{false}\ |\ \neg\phi\ |\ \phi\circ\psi|\
\mathcal{Q}\bar{x}_{\\_}n,\phi\ |\ t$
$\displaystyle\mathbf{Term}_{\\_}{\mathcal{V}}\ni t,y,\tau::=\
t_{\\_}0(t_{\\_}1,..,t_{\\_}{\mathsf{ar}(t_{\\_}0)})\ |\ t\rightarrow y\ |\
t_{\\_}0\times..\times t_{\\_}n\ |\ \lambda\bar{x}_{\\_}n,t\ |\ \cdots\ |\
(\psi)\ |\ \\#?\ s$

where $\circ\in\\{\wedge,\ \vee,\ \Rightarrow,\ \Leftrightarrow\\}$ and
$\mathcal{Q}\in\\{\forall,\ \exists,\ !\exists\\}$.

Formulas consist of the usual binary connectives and quantifiers while terms
permit (respectively) function application,444Outfix and infix style
applications are also accepted, though we omit these for brevity function
(arrow type) constructors, Cartesian products ($\times$), lambda abstraction,
parenthesized formulae, and terminal symbols $s$. We use the notation
$\bar{x}_{\\_}n$ as shorthand for a list of variable binders:
$x_{\\_}1,..,x_{\\_}n:\tau$ of term/type $\tau$.555Note that this effectively
makes the specification language higher order, as one can write, e.g.,
$\forall f:T\rightarrow T,f(x)$; we forego discussion of this and its
ramifications on proof automation—as this paper is primarily concerned with
tools and VC-generation

Next, we establish our syntax for assertive code fragments.

######  Definition 4.2.

A fragment of assertive code consists of zero or more program statements
interleaved with assertive statements of the form:

$\displaystyle\mathbf{Stmt}_{\\_}\mathcal{V}\ni s::=\textnormal{{{Assume}}}\
\phi;\ |\ \textnormal{{{Confirm}}}\ \phi;\ |\ \textnormal{{{Stipulate}}}\
\phi;\ |\ v:=t;\ |\ \cdots\ |\ \mathit{id}(y_{\\_}1,..,y_{\\_}n);$
$\displaystyle\qquad\quad\mathbf{AsrtCode}\ni a::=\ s^{*}\ \
\textnormal{{{Confirm}}}\ \bigwedge seq^{+};\qquad\mathbf{Seqnt}\ni
seq::=\Gamma\vdash\Delta$

where $\Gamma$ and $\Delta$ are sets of well-formed-formulas (wffs).

The statement production rule admits verification language specific statements
(including Assume and Confirm clauses—which we discuss in Sect. 5) as well as
strictly programmatic ones such as function assignment ($v:=t$) and procedure
calls ($\mathit{id}(y_{\\_}1,..,y_{\\_}n)$). We omit any remaining
programmatic statements for brevity.

Lastly, since our parsimonious rules rely on the ability to compute sets of
free variables from specifications, we employ a contexted “specification free
variable” function
$\mathsf{SFV}:\mathcal{C}\times\mathbf{Term}_{\\_}{\mathcal{V}}\rightarrow\wp(\mathbf{Term}_{\\_}{\mathcal{X}})$.
The following example demonstrates the function’s behavior.

######  Example 4.1 (SFV).

After processing theory modules for mathematical Booleans, Integers, and
Strings, suppose $\mathcal{C}$ contains the following constants and
predicates:

$\displaystyle\mathcal{C}=\\{\Lambda:\mathtt{SStr},\
\wedge:\mathbb{B}\times\mathbb{B}\rightarrow\mathbb{B},\
|\bullet|:\mathtt{SStr}\rightarrow\mathbb{N},\ \mathtt{0}:\mathbb{Z},\ \cdots\
\\}.$

The meaning of the types assigned to the constants should be reasonably
familiar with the exception of SStr—which is a user-defined sort representing
the proper class of all heterogeneously typed (math) strings. Next, we enrich
$\mathcal{C}$ with the following operation signature, where the programmatic
type Static_Array is mathematically modeled by \Int \rightarrow Entry.

⬇

$\mathcal{C}^{\prime}=\mathcal{C}\cup\\{\ $Oper Op (e : Entry; Q : Queue; A :
Static_Array);

ensures Q \neq \Lambda \and e = #A(0) \and

A = \lambdaj : \Int, if |Q| = j then #e else #A(j); $\\}$ \

Denoting the ensures clause as $\psi$, then $\mathcal{C}^{\prime}\
\text{\textbackslash}\ \mathsf{SFV}(\psi)$ yields: $\\{\texttt{Q},\
\texttt{\\#A},\ \texttt{A},\ \texttt{\\#e},\ \ \texttt{e}\\}$. Note that
constants like $\Lambda$, $|\bullet|$, etc. and bound variables j were
excluded, while specificational (program) variables (e.g. e, #e) were
included.

###  4.2 Sequent Calculus Review

Formally, the final Confirm assertion (which always terminates a fragment of
assertive code) is represented as a conjunction of Gentzen-style sequents
$\textbf{G}_{\\_}1,\cdots,\textbf{G}_{\\_}n$, each of which constitute the
final VCs produced by our goal-directed program proof process.

Each Gentzen sequent has the form
$\mathbf{G}\equiv\varphi_{\\_}1,\cdots,\varphi_{\\_}m\vdash\psi_{\\_}1,\cdots,\psi_{\\_}n$
where $m$ and $n$ are non-negative and $\varphi_{\\_}1,..,\varphi_{\\_}m$,
$\psi_{\\_}1,..,\psi_{\\_}n$ denote sets of wffs within a given sequent’s
antecedent ($\Gamma$) and succedent ($\Delta$), respectively. The wffs in
these sets are added from different specification contexts based on our proof
rules. Each sequent G semantically adheres to the usual interpretation:
$\bigwedge_{\\_}{i=1}^{m}\varphi_{\\_}i\vdash\bigvee_{\\_}{j=1}^{n}\psi_{\\_}j$.

$\mbox{ $\mathsf{NotLeft}$ }\ \frac{\textstyle\Gamma\vdash\phi,\
\Delta}{\textstyle\Gamma,\ \neg\phi\vdash\Delta}$ $\mbox{ $\mathsf{AndLeft}$
}\ \frac{\textstyle\Gamma,\ \phi,\psi\vdash\Delta}{\textstyle\Gamma,\
\phi\wedge\psi\vdash\Delta}$ $\mbox{ $\mathsf{OrLeft}$ }\
\frac{\textstyle\Gamma,\ \phi\vdash\Delta\quad\Gamma,\
\psi\vdash\Delta}{\textstyle\Gamma,\ \phi\vee\psi\vdash\Delta}$

$\mbox{ $\mathsf{NotRight}$ }\ \frac{\textstyle\Gamma,\
\phi\vdash\Delta}{\textstyle\Gamma\vdash\neg\phi,\ \Delta}$ $\mbox{
$\mathsf{AndRight}$ }\ \frac{\textstyle\Gamma\vdash\phi,\
\Delta\quad\Gamma\vdash\psi,\ \Delta}{\textstyle\Gamma\vdash\phi\wedge\psi,\
\Delta}$ $\mbox{ $\mathsf{OrRight}$ }\ \frac{\textstyle\Gamma\vdash\phi,\psi,\
\Delta}{\textstyle\Gamma\vdash\phi\vee\psi,\ \Delta}$

Figure 3: Standard sequent reduction rules for $\neg$, $\wedge$, and $\vee$.

To simplify the VCs, we apply the standard sequent reduction rules shown in
Fig. 3 to the antecedents and succedents of the sequents that make up the
final Confirm until they contain only atomic formulas.

We also fix convenience functions
$\mathsf{SFV}_{\\_}{\mathbf{set}}(\mathit{S})$ which extracts the sfv set from
the wffs in a given set $S$, and $\mathsf{SFV}_{\\_}{\vdash}(\mathit{seq})$
which extracts the sfv set from each side of a given sequent, seq.

###  4.3 Goal-Directed Proof Rule Application

Once assertive code has been constructed, the approach we use to generate VCs
is goal-directed and is illustrated at a high level in Fig. 4.

Figure 4: RESOLVE’s VC generation scheme.

Starting with the penultimate statement (prior to the final Confirm
conjunction), each statement is eliminated one at a time via the application
of its corresponding proof rule. After each statement rule is applied, sequent
reduction rules and others (such as rules for handling equality or theory-
specific rewrite rules) are then applied to further simplify the formulae in
each sequent.

After all statements have been eliminated via application of their
corresponding rules, the conjuncted sequents in the final Confirm are broken
apart and sent off to RESOLVE’s in-house congruence closure prover for
verification [12, 16]. The particulars of the prover are not directly relevant
to this paper. Prover backends with which we have experimented include
specialized decision procedures [2] as well as SMT solvers [31] based on Z3
[25].

##  5 Proof Rules for Forming Parsimonious VCs

In this section, proof rules for generating parsimonious VCs are formalized
and illustrated on a fragment of example assertive code. As with the sequent
reduction rules, in the proof rules that follow, it is necessary and
sufficient to prove what is above the line in order to prove what follows
below the line.

### Confirm Rule

Confirm clauses add a sequent with a single goal to the final sequent
conjunction. This, and the “assume” rule that follows in the next section,
represent an intermediate type of assertion which generally arise from the
application of other (larger) proof rules. For example, applying RESOLVE’s
call rule generates (within the assertive code) a Confirm clause asserting
that the called operation’s argument-specialized precondition $\varphi$ holds.
The confirm rule is given below:

$\displaystyle\mbox{ $\mathsf{Confirm}$ }\
\frac{\textstyle\mathcal{C}\backslash\ \mathit{c};\quad\texttt{{Confirm}}\
\bigwedge\Psi\cup\\{\vdash\varphi\\};}{\textstyle\mathcal{C}\backslash\
\mathit{c};\quad\texttt{{Confirm}}\ \varphi;\quad\texttt{{Confirm}}\
\bigwedge\Psi;}$

Here and in subsequent rules we employ the turnstile $\vdash$ as a shorthand
sequent constructor. For example, $\vdash\varphi$ denotes a fresh sequent with
no antecedents and a single wff $\varphi$ in its succedent. In cases where we
wish to add $\varphi$ to the antecedent of some non-empty sequent $s$, we will
write $\Gamma_{\\_}s,\varphi\vdash\Delta_{\\_}s$ where $\Gamma_{\\_}s$ and
$\Delta_{\\_}s$ refer to sets of existing wffs in the antecedent and succedent
of $s$, respectively.

######  Example 5.1.

Recalling the math string notation outlined in section 2, suppose the system
generated the following assertive code fragment:

⬇

Assume |S| \leq 2 $\wedge$ |T| \leq 2 $\wedge$ S = \Lambda $\wedge$ T =
\langle1\rangle \circ \langle2\rangle;

Confirm (S = \Lambda $\vee$ T = \Lambda) $\wedge$ (|S| + |T| = 2);

Confirm $\bigwedge$ $\Psi$;

Application of the Confirm rule yields:

⬇

Assume |S| \leq 2 $\wedge$ |T| \leq 2 $\wedge$ S = \Lambda $\wedge$ T =
\langle1\rangle \circ \langle2\rangle;

Confirm $\bigwedge$ $\Psi\ \cup$ $\\{$ {} $\vdash$ {(S = \Lambda $\vee$ T =
\Lambda) $\wedge$ (|S| + |T| = 2)} $\\}$;

The VC Generator then simplifies the final confirm with an application of
AndRight then OrRight to the first (and only) sequent’s succedent in the set
$\Psi$, yielding:

⬇

Assume |S| \leq 2 $\wedge$ |T| \leq 2 $\wedge$ S = \Lambda $\wedge$ T =
\langle1\rangle \circ \langle2\rangle;

Confirm $\bigwedge$ $\Psi\ \cup\ \\{$ {} $\vdash$ {S = \Lambda, T = \Lambda}
$\\}\ \cup\ \\{$ {} $\vdash$ {|S| + |T| = 2} $\\}$;

In future assertive code listings, we omit the set $\Psi$ for brevity.

### Parsimonious Assume Rule

Assume clauses add antecedents to sequents in the final Confirm. The key to
the new parsimonious rule, however, is to only add givens that are “relevant”
to a given sequent. Conservative variants of our VC generator simply added
each conjunct of an encountered assume clause to the list of givens for each
VC—resulting in VCs with many redundant givens (e.g., Sect. 3). Below is our
parsimonious variant of the original rule.

$\displaystyle\mbox{ $\mathsf{ParsimoniousAssume}$ }\
\frac{\textstyle\mathcal{C}\backslash\ \mathit{c};\quad\texttt{{Confirm}}\
\bigwedge\sigma(\Psi,\varphi)}{\textstyle\mathcal{C}\backslash\
\mathit{c};\quad\texttt{{Assume}}\ \varphi;\quad\texttt{{Confirm}}\
\bigwedge\Psi;}$

The core addition to our revised rule (aside from the usage of sequents) is
the addition of a parsimonious “selection” function $\sigma$ that is applied
to the set of existing sequents $\Psi$ in the final Confirm and the formula
$\varphi$ that is being assumed—i.e., $\sigma(\Psi,\varphi)$. We define this
selection function as follows:

$\displaystyle\sigma:((S:\wp(\mathbf{Sqnt}_{\\_}\mathcal{V}))\times(\psi:\mathbf{Form}_{\\_}\mathcal{V}))\rightarrow\wp(\mathbf{Sqnt}_{\\_}\mathcal{V})\
\triangleq$
$\displaystyle\qquad\\{s:S\mid\forall\phi:\langle\langle\psi\rangle\rangle,$
$\displaystyle\qquad\qquad\mathbf{if}\
\mathsf{FVC}(\phi,\langle\langle\psi\rangle\rangle)\cap\mathsf{SFV}_{\\_}\vdash(s)\neq\emptyset\
\textbf{ then }\ s=\Gamma_{\\_}s,\phi\vdash\Delta_{\\_}s\ \mathbf{else}\
s=\Gamma_{\\_}s\vdash\Delta_{\\_}s\\}.$

Specifically, $\sigma$ takes a set of existing sequents $S$ along with a
formula $\psi$ and produces a set of (potentially modified) sequents. Here,
the $\langle\langle\bullet\rangle\rangle$ operator is used to split $\psi$
into a list of conjuncts. The comprehension in the body of $\sigma$ tests
whether or not the transitive closure of all free variables of $\phi$
appearing across of the collection of any conjuncted clauses in $\psi$
(computed via a free-var closure function
$\mathsf{FVC}(\phi,\langle\langle\psi\rangle\rangle)$ intersects with the free
variables obtained from the existing sequent $s$. If the intersection is non-
empty, $\phi$ is added to the antecedent of $s$, otherwise $s$ remains
unchanged.

While the benefits of the parsimonious assume rule will not be immediately
evident from example 5.1, its impact on the number of givens in VCs generated
by larger programs and algorithms will be examined further in Sect. 7.

######  Example 5.2.

To illustrate why the $\mathsf{FVC}$ function is needed, we consider the
following assertive code (where each specificational free variable is
subscripted by a $v$):

⬇

Assume p(cv) $\wedge$ cv = bv $\wedge$ sv = xv

Confirm $\bigwedge$ {} $\vdash$ {p(bv)}

Suppose we break apart the Assume clause (i.e., using
$\langle\langle\bullet\rangle\rangle$) and consider each conjunct isolation,
one at a time, from left to right. The sfv set from the first clause,
p(c${}_{\\_}v$) (i.e.: $\\{\mathtt{c}_{\\_}v\\}$), does not overlap with the
sfv set from the sequent in the final confirm ($\\{\mathtt{b}_{\\_}v\\}$),
thus it would not be added as an antecedent. However, the second clause would
be added to the antecedent (since b${}_{\\_}v$ overlaps). But the first
clause—which has been since discarded—is needed along with the second in order
to prove the goal (the third is rightfully excluded as it has no overlaps).
The FVC closure function solves this problem by combining the sfv set of a
given source clause (in this case $\mathtt{p}(\mathtt{b}_{\\_}v)$), with any
other clauses in the provided list with overlapping specificational free
variables. For example:

$\displaystyle\mathsf{FVC}(\ \mathtt{p}(\mathtt{b}_{\\_}v),\
\langle\langle\mathtt{p}(\mathtt{c}_{\\_}v),\ \
\mathtt{c}_{\\_}v=\mathtt{b}_{\\_}v,\ \ ...\ \rangle\rangle\
)=\\{\mathtt{c}_{\\_}v,\mathtt{b}_{\\_}v\\}$

which enables us to add required clauses while still filtering unrelated ones.

### Postprocessing Rule: Folding Top Level Equalities

We also introduce a separate assertive code postprocessing/simplification rule
that performs substitutions for equalities appearing as top level formulas in
a given sequent’s antecedent. Here, such equalities must be of the general
form $v=t$, where
$v\in\mathsf{SFV}_{\\_}{\mathbf{set}}(\Gamma-\\{v=t\\})$666The notation
$\varphi[v\rightsquigarrow t]$ in the rule denotes the substitution of a
variable $v$ for a term $t$ in clause $\varphi$.

$\displaystyle\mbox{ $\mathsf{ApplyEqLeft}$ }\ \frac{\textstyle\mathcal{C}\
\text{\textbackslash}\ \ \textbf{{Confirm}}\
\bigwedge\varphi_{\\_}i[v\rightsquigarrow
t]\vdash\delta_{\\_}j[v\rightsquigarrow t]}{\textstyle\mathcal{C}\
\text{\textbackslash}\ \ \textbf{{Confirm}}\
\bigwedge\varphi_{\\_}1,\cdots,\varphi_{\\_}n,\
v=t\vdash\delta_{\\_}1,\cdots,\delta_{\\_}m}\textnormal{ where
}\varphi_{\\_}i\in\Gamma,\delta_{\\_}j\in\Delta\textnormal{ and
}i\leq|\Gamma|,j\leq|\Delta|$

Returning to example 5.1, since ApplyEqLeft requires $v=t$ to appear as a top-
level formula in the antecedent (both of which are currently empty) and that
all assertive statements prior to the final confirm clause are eliminated, the
rule cannot yet be applied. Thus, we must first apply the ParsimoniousAssume
rule which yields:

⬇

Confirm $\bigwedge$

{|S| \leq 2, |T| \leq 2, S = \Lambda, T = \langle1\rangle \circ
\langle2\rangle} $\vdash$ {S = \Lambda, T = \Lambda}

{|S| \leq 2, |T| \leq 2, S = \Lambda, T = \langle1\rangle \circ
\langle2\rangle} $\vdash$ {|S| + |T| = 2};

Following this, the VC generator’s simplifier then applies any applicable
sequent based reduction rules,777Beyond the traditional statement rules, we
broadly categorize any rule involving the $\vdash$ meta operator as a sequent
rule which, in this case, consists of four back-to-back applications of
ApplyEqLeft (two for each sequent), resulting in:

⬇

Confirm $\bigwedge$

{|\Lambda| \leq 2, |\langle1\rangle \circ \langle2\rangle| \leq 2} $\vdash$
{\Lambda = \Lambda, (\langle1\rangle \circ \langle2\rangle) = \Lambda}

{|\Lambda| \leq 2, |\langle1\rangle \circ \langle2\rangle| \leq 2} $\vdash$
{|\Lambda| + |\langle1\rangle \circ \langle2\rangle| = 2};

The first sequent is provable via the trivially true equality:
$\Lambda=\Lambda$ (recall that since each wff in the succeedent is disjuncted,
this trivial equality makes the entire succeedent true). The second follows
from application of various corollaries available in our theory of strings
including, e.g.:

⬇

Corollary Len1: \forall \alpha, \beta : SStr, |\alpha $\circ$ \beta| =
|\alpha| + |\beta|;

as well as results involving natural numbers, +, and the base case of our
string theory’s inductively defined length $|\bullet|$ function (which
establishes |$\Lambda$| = 0).

Note that while one could conceivably apply additional rules (such as
reflexivity) to “close/prove” sequents on the fly during VC generation, we
instead choose dispatch each VC only at the proving stage for consistency and
reporting purposes—e.g.: displaying results after a “prove” button is pressed.
Otherwise, a proved, missing VC may be surprising or misleading to a learner.

### Improving Verifier Feedback for Contradictory Code

The process of removing irrelevant givens requires care, as it can lead to
incompleteness that negatively impacts verifier feedback. Consider, e.g, the
contradictory fragment of code starting with (A) in Fig. 5.

Figure 5: Deriving a vacuously true sequent from contradictory nested if-
statements using a variant of the Assume rule called Stipulate

While the VC generator sets up assertive code for all nominal paths through
the body, Fig. 5 focuses on the derivation where the innermost if-statement’s
body is presumed to execute. Note that each if-statement’s condition is
translated by the system into a Stipulate statement—meaning any control
predicates resulting from the application of proof rules to If, While, etc.
statements always get included as antecedents in the final confirm’s sequents
(regardless of variable overlap). To see why Stipulate is needed, consider
step (E) in Fig. 5 and replace each Stipulate keyword with Assume and proceed
with the derivation. Since there are no overlaps between the assumed clauses
and the final confirm, each would be discarded, leaving the unprovable sequent
$\vdash\\{1=2\\}$ to timeout during a proof attempt. This is not advantageous
from a feedback perspective, as student code often contains similar
contradictions and unreachable logic (though perhaps less obvious ones). Under
this approach, vacuously true VCs can be flagged and reported to the
user—identifying suspect code.

##  6 Sequent-Based VC Generation in RESOLVE Studio

In this section, using a sorting example, we provide an overview of the VC
reporting, simplification, and derivation tracing features included in our
second environment, RESOLVE Studio.

###  6.1 Example: Fully Generic Sorting

For a more complex example, we consider the specification and implementation
of a generic sorting algorithm for queues. However, rather than adding a sort
operation to the Queue_Template concept (which would require updating each
existing implementation) we instead use an enhancement module—which allow
users to write layered code for secondary operations using the primary
operations of the base concept (in this case, Queue_Template). The queue
Sorting_Capability enhancement is below.

⬇

Enhancement Sorting_Capability (Def $\trianglelefteq$: Entry \times Entry
\longrightarrow $\mathbb{B}$) for Queue_Template;

uses Basic_Ordering_Theory, String_Theory with Occ_Tly_Permute_Ext;

requires Is_Total_Preordering($\trianglelefteq$);

Operation Sort (updates Q : Queue);

ensures Q Is_Permutation #Q $\wedge$ Is_Cfml_w(Q, $\trianglelefteq$);

end Sorting_Capability;

The enhancement is parameterized by an (abstract) binary predicate
$\trianglelefteq$ that determines ordering of the queue’s entries. The module
level pre-condition subsequently requires that the relation passed is a total
preordering—i.e.: it must be both total and transitive:

$\displaystyle\textnormal{($\trianglelefteq$-total)}\ \ \forall
x,y:\mathtt{Entry},\ x\trianglelefteq y\ \vee\ y\trianglelefteq
x\quad\quad\textnormal{($\trianglelefteq$-trans)}\ \ \forall
x,y,z:\mathtt{Entry},\ x\trianglelefteq y\Rightarrow y\trianglelefteq
z\Rightarrow x\trianglelefteq z.$

The Sort operation takes a single queue, Q, and ensures two properties: (1)
that the resulting queue is a permutation of (exactly) the incoming queue’s
entries, and (2) that the ordering of all entries in the outgoing queue is
conformal with (Is_Cfml_w) the $\trianglelefteq$ ordering predicate. Both the
permutation and conformality predicates were imported from String_Theory,
augmented with a string occurrence tallying and permutation theory extension
containing the required predicates.

For more information on the predicates that make up the sorting
specification—and the way in which we define them in RESOLVE theories
(including aspects of the math type system)—please consult [34].

###  6.2 An Annotated Implementation

Fig. 6 shows a selection sorting implementation of Sorting_Capability loaded
(with VCs already generated) in RESOLVE Studio.

Figure 6: Selection sorting impl. in RESOLVE Studio; viewing the VC for the
loop invariant’s base case

Note that enhancement implementations are oblivious to any one particular
implementation of the base concept, and must be written in terms of either
local operations and/or by calling the primary operations of the base concept.
The implementation iterates over the input queue, extracts the minimum entry
in each iteration via the local procedure Remove_Min, then enqueues it onto a
temporary queue, Sorted_Q (which holds the entries ordered thus far). The loop
is annotated in several different parts: a changing clause indicates the
variables being updated in the loop (which can help simplify certain styles of
invariants), a decreasing clause (a progress metric for proving termination),
and a loop invariant communicated through the maintaining clause. The
invariant, shown in Fig. 6, is summarized below:

  * •

The first conjunct states that the concatenation of elements in the
(temporary) Sorted_Q and Q constitute the entirety of the elements being
sorted.

  * •

The second conjunct states that the Sorted_Q’s elements are ordered w.r.t. the
$\trianglelefteq$ relation.

  * •

The last conjunct states that every element in Sorted_Q is related by
$\trianglelefteq$ to every element in Q. In other words: that all entries in
Sorted_Q “precede” the remaining entries in Q.

###  6.3 Verification

The verification process is started by invoking the “Generate VCs” action.
Once VCs are generated, clicking any of the  buttons opens a tool menu wherein
users can select any VCs arising from that particular construct or line of
code (Fig. 7, leftmost).

Figure 7: VC selection process in RESOLVE Studio

Once a VC is selected, the IDE automatically navigates to the VC in question
in the tool window, displaying the goal and givens. Selecting any particular
VC in the “Final VCs” window also highlights the assertion, statement, or
construct that generated it within the code. Pressing the prove button invokes
the verifier, updating the badges with a checkmark, warning, or a
timeout/failure icon.

Advanced Feature: VC Derivation Tracing. RESOLVE Studio also allows
experienced users and researchers the ability to trace interactively through
the derivation of VCs, starting from initial assertive code, to final VCs
(Fig. 8) below.

Figure 8: Interactive VC derivation tracing and rule application from example
5.1

We anticipate this being of use to math specialists such as theory developers
who seek to add theory-specific simplification rules (e.g., simplifying
$S\circ\Lambda$ to $S$) and observe their affect when applied during
derivations to further ‘clean’ resulting VCs and ease their comprehension.

##  7 Experimental Evaluation

We have tested our revised VC generation technique on a modest battery of
extension operations888Recursive implementations are labeled with an $(R)$ for
a variety of concepts drawn from RESOLVE’s current component library including
typical operations for lists, stacks, and queues.

Component |  | Non-Parsimonious |  | Parsimonious
---|---|---|---|---
|  | #VCs | #VCs${}_{\\_}{A\geq 5}$ | #VCs${}_{\\_}{A\geq 10}$ |  | #VCs | #VCs${}_{\\_}{A\geq 5}$ | #VCs${}_{\\_}{A\geq 10}$
List Search |  | 35 | 35 | 35 |  | 35 | 16 | 0
List Reverse (R) |  | 8 | 8 | 8 |  | 8 | 0 | 0
Queue Append (R) |  | 8 | 8 | 8 |  | 8 | 0 | 0
Queue Selection Sort |  | 36 | 36 | 36 |  | 36 | 16 | 0
Stack Copy |  | 24 | 24 | 24 |  | 24 | 5 | 0
Table 1: Comparison of VC generation schemes: non-parsimonious vs
parsimonious.

Table 1 compares VCs generated without and with the parsimonious scheme. For
each, the first column contains the total number of VCs generated
($\\#\mathit{VCs}$), the number of VCs generated with five or more antecedents
($\\#\mathit{VCs_{\\_}{A\geq 5}}$), and the number of VCs generated with ten
or more antecedents ($\\#\mathit{VCs_{\\_}{A\geq 10}}$).

Note that with the non-parsimonious scheme, all VCs contain ten or more
antecedents, while under the parsimonious scheme none contain more than ten.
Since this paper has been written, the parsimonious scheme detailed has also
been incorporated into the compiler backing the web-IDE, meaning students have
already benefited from the reduced size of each VC. For a sense of how much
shorter the VCs are, consider the (unprovable) VC from our initial example in
Fig. 2: $\\{1\leq|\langle e^{\prime\prime\prime}\rangle\ \circ\
S^{\prime}|\\}\vdash\\{S^{\prime}=\langle e^{\prime\prime\prime}\rangle\
\circ\ S^{\prime}\\}$.

These experimental results indicate that the parsimonious scheme produces
fewer givens for humans to consider when debugging failed VCs. This can be
viewed as a measure of usefulness for VC comprehension overall, as well as a
means of improving ease of use when combined with our existing F-IDEs.

##  8 Related Work

Since VC generation and auto-active program verification are vast topics, this
section focuses primarily on work in generating simpler, debuggable VCs
presented in an IDE or otherwise. A direct comparison of our work with other
efforts is somewhat hindered by the simple fact that others typically
“outsource” the process of generating VCs to Intermediate Verification
Languages (IVLs) such as Boogie [19]. Outsourcing has its benefits, namely:
shifting the burden of VC generation (which can be non-trivial to implement in
general) to a separate, reusable tool that multiple languages can target.
Notable disadvantages however include high potential for “impedance
mismatches” when translating between IVLs [4], or (more commonly) when
translating the constructs of the rich ‘high level’ specification language
into the ‘lower level’ representation employed by a particular IVL [33]—or
vice versa [11]. These mismatches in turn can complicate error reporting
efforts, including VC feedback on failed verification attempts. Some related
systems are summarized below.

Dafny [20] integrates its toolchain into an IDE for Visual Studio including
the Boogie Verification Debugger [19], which translates Z3 generated counter
examples into a form suitable for human consumption. AutoProof [32], which
also uses Boogie and Z3 for the verification of Eiffel programs, employs “two
step" verification to broadly interpret (as opposed to on a per-VC basis) the
reasons for verification failures using a combination of traditional modular
verification and approximation (such as unrolling). For IDE support, push-
button verification and a host of other functionality is provided in the
Eiffel Verification Environment.

Why3 [8] is another popular autoactive tool that employs its own IVL (WhyML),
to target a number of SMT solvers for automated proof as well as some
traditionally interactive systems (such as Coq) for proofs requiring manual
steps. The language comes with a verification environment (called WhyIDE) that
gives users the ability to browse goals in the current session and perform
common transformations such as, for example, splitting a goal into separate
conjuncts (which can then be sent to different provers).

The KeY framework [3], which targets full functional verification of Java
programs, perhaps gives users the most control over how VCs are structured and
ultimately dispatched. As opposed to being reliant on any particular IVL, the
language instead employs its own in-house prover that attempts to
automatically verify a VC via repeated application of first order sequent
reduction rules (among others). In cases where automation fails, the system
can also serve as an interactive proof assistant that allows users to
systematically apply ‘taclets’ (i.e., tactics) to the current proof
state—manually guiding the system towards the goal.

##  9 Conclusions and Future Work

We have discussed the design of two F-IDEs that aim to provide users with
feedback suitable for reasoning about code correctness when verification
fails. Following a technical overview of our revised proof system, including
rules for deriving “parsimonious” VCs, we have demonstrated our presentation
of VCs in both the context of the web-IDE (in use for several years) and a
newer F-IDE named RESOLVE Studio. A critical avenue for future work remains
the ability to efficiently persist verification results to ease usability and
to support scalable development of larger, more intricate case studies. Though
we have extensive positive feedback from students who have used our online
reasoning tools for which the VC generator detailed in this paper now forms
the backbone [9, 10, 26], we anticipate additional studies on student usage
and debugging of VCs in our second experimental environment, RESOLVE Studio.

### Acknowledgments

We thank the RSRG research groups at Clemson and Ohio State who have
contributed to this work. Particular thanks are due to Bill Ogden and Joan
Krone for their insights on the proof rules detailed.

## References

  * [1]
  * [2] Bruce Adcock (2010): _Working Towards the Verified Software Process_.  PhD thesis, The Ohio State University.
  * [3] Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt & Mattias Ulbrich (2016): _Deductive Software Verification \- The KeY Book - From Theory to Practice_.  LNCS 10001, Springer, Cham, 10.1007/978-3-319-49812-6.
  * [4] Michael Ameri & Carlo A. Furia (2016): _Why Just Boogie?_ In Erika Ábrahám & Marieke Huisman, editors: IFM 2016, Springer International Publishing, Cham, pp. 79–95, 10.1007/978-3-319-33693-0_6.
  * [5] Charles T. Cook, Svetlana Drachova-Strang, Yu-Shan Sun, Murali Sitaraman, Jeffrey C. Carver & Joseph E. Hollingsworth (2013): _Specification and reasoning in SE projects using a Web IDE_.  In: 26th International Conference on Software Engineering Education and Training, CSEE&T 2013, San Francisco, CA, USA, May 19-21, 2013, pp. 229–238, 10.1109/CSEET.2013.6595254.
  * [6] Charles T. Cook, Heather Harton, Hampton Smith & Murali Sitaraman (2012): _Specification Engineering and Modular Verification Using a Web-integrated Verifying Compiler_.  In: ICSE, ACM, pp. 1379–1382, 10.1109/ICSE.2012.6227243.
  * [7] Charles T. Cook, Heather K. Harton, Hampton Smith & Murali Sitaraman (2012): _Specification engineering and modular verification using a web-integrated verifying compiler_.  In Martin Glinz, Gail C. Murphy & Mauro Pezzè, editors: ICSE 2012, IEEE Computer Society, pp. 1379–1382, 10.1109/ICSE.2012.6227243.
  * [8] Jean-Christophe Filliâtre & Andrei Paskevich (2013): _Why3 - Where Programs Meet Provers_.  In Matthias Felleisen & Philippa Gardner, editors: ESOP 2013, LNCS 7792, Springer, pp. 125–128, 10.1007/978-3-642-37036-68.
  * [9] Megan Fowler, Eileen T. Kraemer, Murali Sitaraman & Joseph E. Hollingsworth (2021): _Tool-Aided Loop Invariant Development: Insights into Student Conceptions and Difficulties_.  In Carsten Schulte, Brett A. Becker, Monica Divitini & Erik Barendsen, editors: ITiCSE 2021, ACM, pp. 387–393, 10.1145/3430665.3456351.
  * [10] Megan Fowler, Eileen T. Kraemer, Yu-Shan Sun, Murali Sitaraman, Jason O. Hallstrom & Joseph E. Hollingsworth (2020): _Tool-Aided Assessment of Difficulties in Learning Formal Design-by-Contract Assertions_.  In Jürgen Mottok, editor: ECSEE 2020, ACM, pp. 52–60, 10.1145/3396802.3396807.
  * [11] Carlo A. Furia, Christopher M. Poskitt & Julian Tschannen (2015): _The AutoProof Verifier: Usability by Non-Experts and on Standard Code_.  In Catherine Dubois, Paolo Masci & Dominique Méry, editors: F-IDE 2015, pp. 42–55, 10.4204/EPTCS.187.4.
  * [12] Smith Hampton (2013): _Engineering Specifications and Mathematics for Verified Software_.  PhD Dissertation, Clemson University.
  * [13] Douglas E. Harms & Bruce W. Weide (1991): _Copying and Swapping: Influences on the Design of Reusable Software Components_.  IEEE Trans. Softw. Eng. 17(5), pp. 424–435, 10.1109/32.90445.
  * [14] Heather Harton (2011): _Mechanical and Modular Verification Condition Generation for Object-Based Software_.  PhD Dissertation, Clemson University.
  * [15] Wayne D. Heym, Paolo A. G. Sivilotti, Paolo Bucci, Murali Sitaraman, Kevin Plis, Joseph E. Hollingsworth, Joan Krone & Nigamanth Sridhar (2017): _Integrating Components, Contracts, and Reasoning in CS Curricula with RESOLVE: Experiences at Multiple Institutions_.  In Hironori Washizaki & Nancy Mead, editors: CSEE&T, IEEE, pp. 202–211, 10.1109/CSEET.2017.40.
  * [16] Nabil M. Kabbani, Daniel Welch, Caleb Priester, Stephen Schaub, Blair Durkee, Yu-Shan Sun & Murali Sitaraman (2015): _Formal Reasoning Using an Iterative Approach with an Integrated Web IDE_.  In: F-IDE 2015, pp. 56–71, 10.4204/EPTCS.187.5.
  * [17] Jason Kirschenbaum, Bruce M. Adcock, Derek Bronish, Hampton Smith, Heather K. Harton, Murali Sitaraman & Bruce W. Weide (2009): _Verifying Component-Based Software: Deep Mathematics or Simple Bookkeeping?_ In Stephen H. Edwards & Gregory Kulczycki, editors: ICSR 2009, LNCS 5791, Springer, Berlin, Heidelberg, pp. 31–40, 10.1007/978-3-642-04211-94.
  * [18] Eileen T. Kraemer, Murali Sitaraman & Joseph E. Hollingsworth (2018): _An Activity-Based Undergraduate Software Engineering Course to Engage Students and Encourage Learning_.  In: Proceedings of the 3rd European Conference of Software Engineering Education, ECSEE 2018, Seeon Monastery, Bavaria, Germany, June 14-15, 2018, pp. 18–25, 10.1145/3209087.3209100.
  * [19] Claire Le Goues, K. Rustan M. Leino & Michał Moskal (2011): _The Boogie Verification Debugger (Tool Paper)_.  In Gilles Barthe, Alberto Pardo & Gerardo Schneider, editors: SEFM 2011, LNCS, Springer, Berlin, Heidelberg, pp. 407–414, 10.1007/978-3-642-24690-628.
  * [20] K. Rustan M. Leino (2013): _Developing verified programs with Dafny_.  In David Notkin, Betty H. C. Cheng & Klaus Pohl, editors: ICSE 2013, IEEE, pp. 1488–1490, 10.1109/ICSE.2013.6606754.
  * [21] K. Rustan M. Leino & Michal Moskał (2010): _Usable Auto-Active Verification_.  In Tom Ball, Lenore Zuck & Natarajan Shankar, editors: UV 2010.  Available at http://fm.csl.sri.com/UV10/.
  * [22] K. Rustan M. Leino & Clément Pit-Claudel (2016): _Trigger Selection Strategies to Stabilize Program Verifiers_.  In Swarat Chaudhuri & Azadeh Farzan, editors: CAV 2016, LNCS 9779, Springer, pp. 361–381, 10.1007/978-3-319-41528-420.
  * [23] Nicodemus M. J. Mbwambo (2017): _A Well-Designed, Tree-Based, Generic Map Component to Challenge the Process Towards Automated Verification_.  Master’s Thesis, Clemson University.
  * [24] Bertrand Meyer (1992): _Applying “Design by Contract"_.  Computer 25(10), pp. 40–51, 10.1109/2.161279.
  * [25] Leonardo de Moura & Nikolaj Bjørner (2008): _Z3: An Efficient SMT Solver_.  In C. R. Ramakrishnan & Jakob Rehof, editors: TACAS 2008, LNCS 4963, Springer, Berlin, Heidelberg, pp. 337–340, 10.1007/978-3-540-78800-324.
  * [26] C. Priester, Y. S. Sun & M. Sitaraman (2016): _Tool-Assisted Loop Invariant Development and Analysis_.  In: 2016 IEEE 29th International Conference on Software Engineering Education and Training (CSEET), pp. 66–70, 10.1109/CSEET.2016.28.
  * [27] Kalyan C. Regula, Hampton Smith, Heather Keown, Jason O. Hallstrom, Nigamanth Sridhar & Murali Sitaraman (2012): _A Case Study in Verification of Embedded Network Software_.  In Alwyn Goodloe & Suzette Person, editors: NFM 2012, LNCS 7226, Springer, pp. 433–448, 10.1007/978-3-642-28891-3_38.
  * [28] Iman Saleh (2015): _Formalizing Data-Centric Web Services_.  Web-Scale Workflow and Analytics, Springer, 10.1007/978-3-319-24678-9.
  * [29] Murali Sitaraman, Bruce M. Adcock, Jeremy Avigad, Derek Bronish, Paolo Bucci, David Frazier, Harvey M. Friedman, Heather K. Harton, Wayne D. Heym, Jason Kirschenbaum, Joan Krone, Hampton Smith & Bruce W. Weide (2011): _Building a Push-Button RESOLVE Verifier: Progress and Challenges_.  Formal Aspects of Computing 23(5), pp. 607–626, 10.1007/s00165-010-0154-3.
  * [30] Yu-Shan Sun (2018): _Towards Automated Verification of Object-Based Software with Reference Behavior_.  PhD Dissertation, Clemson University.
  * [31] Aditi Tagore, Diego Zaccai & Bruce W. Weide (2012): _Automatically Proving Thousands of Verification Conditions Using an SMT Solver: An Empirical Study_.  In: NFM 2012, pp. 195–209, 10.1007/978-3-642-28891-320.
  * [32] Julian Tschannen, Carlo A. Furia, Martin Nordio & Nadia Polikarpova (2015): _AutoProof: Auto-Active Functional Verification of Object-Oriented Programs_.  In Christel Baier & Cesare Tinelli, editors: TACAS 2015, LNCS 9035, Springer, Berlin, Heidelberg, pp. 566–580, 10.1007/978-3-662-46681-053.
  * [33] Mark Utting, David J. Pearce & Lindsay Groves (2017): _Making Whiley Boogie!_ In Nadia Polikarpova & Steve Schneider, editors: IFM 2017, LNCS 10510, Springer, pp. 69–84, 10.1007/978-3-319-66845-15.
  * [34] Daniel Welch (2019): _Scaling Up Automated Verification: A Case Study and a Formalization IDE for Building High Integrity Software_.  PhD Dissertation, Clemson University.
  * [35] Daniel Welch & Murali Sitaraman (2017): _Engineering and Employing Reusable Software Components for Modular Verification_.  In Goetz Botterweck & Claudia Werner, editors: ICSR 2017, LNCS 10221, Springer, pp. 139–154, 10.1007/978-3-319-56856-010.