Report describing an efficient data structure for supporting common relations in an application capable of assisting and verifying formal arguments.

In work that involves mathematical rigor, there are numerous benefits to adopting a representation of models and arguments that can be supplied to a formal reasoning or verification system: reusability, automatic evaluation of examples, and verification of consistency and correctness. However, accessibility has not been a priority in the design of formal verification tools that can provide these benefits. In earlier work \cite{BUCS-TR-2009-015}, we attempt to address this broad problem by proposing several specific design criteria organized around the notion of a \emph{natural context}: the sphere of awareness a working human user maintains of the relevant constructs, arguments, experiences, and background materials necessary to accomplish the task at hand. This work expands one aspect of the earlier work by considering more extensively an essential capability for any formal reasoning system whose design is oriented around simulating the natural context: native support for a collection of mathematical relations that deal with common constructs in arithmetic and set theory. We provide a formal definition for a context of relations that can be used to both validate and assist formal reasoning activities. We provide a proof that any algorithm that implements this formal structure faithfully will necessary converge. Finally, we present and prove the efficiency of an implementation of this formal structure that leverages modular implementations of well-known data structures: balanced search trees and transitive closures of hypergraphs.

In college courses dealing with material that requires mathematical rigor, there are numerous benefits to adopting a machine-readable representation for formal arguments: students can focus on a consistent and specific collection of constructs, examples and counterexamples can be evaluated, and assignments can be assembled and checked with the help of automated system for assistance and verification of formal reasoning. However, the usability and accessibility of such machine-readable representations (and the corresponding systems) has not been a priority in the design of formal verification tools that can provide these benefits. In related work \cite{BUCS-TR-2009-015}, we attempt to address this broad problem by proposing several specific design criteria organized around the notion of a \emph{natural context}: the sphere of awareness a working human user maintains of the relevant constructs, arguments, experiences, and background materials necessary to accomplish the task at hand. We evaluate our proposed design criteria by deploying within the classroom a formal lightweight verification system designed according to our criteria. We present all of the formal reasoning examples and assignments considered during this deployment, most of which are drawn directly from an introductory text on functional programming. We demonstrate how the design of the system improves the effectiveness and understandability of the examples, and how it aids in the instruction of formal basic formal reasoning techniques. We make brief remarks about the practical and administrative implications of the system's design from the perspectives of the student, the instructor, and the grader.

In research areas involving mathematical rigor, there are numerous benefits to adopting a formal representation of models and arguments: reusability, automatic evaluation of examples, and verification of consistency and correctness. However, accessibility has not been a priority in the design of formal verification tools that can provide these benefits. In earlier work \cite{BUCS-TR-2009-015}, we attempt to address this broad problem by proposing several specific design criteria organized around the notion of a \emph{natural context}: the sphere of awareness a working human user maintains of the relevant constructs, arguments, experiences, and background materials necessary to accomplish the task at hand. We evaluate our proposed design criteria by utilizing within the context of novel research a formal reasoning system that is designed according to these criteria. In particular, we consider how the design and capabilities of the formal reasoning system that we employ influence, aid, or hinder our ability to accomplish a formal reasoning task -- the assembly of a machine-verifiable proof pertaining to the NetSketch formalism.

NetSketch is a tool for the specification of constrained-flow applications and the certification of desirable safety properties imposed thereon. NetSketch is conceived to assist system integrators in two types of activities: modeling and design. It provides capabilities for compositional analysis based on a strongly-typed Domain-Specific Language (DSL) for describing and reasoning about constrained-flow networks and invariants that need to be enforced thereupon. In a companion paper \cite{BUCS-TR-2009-028}, we overview NetSketch, highlight its salient features, and illustrate how it could be used in actual applications. In this paper, we define using a machine-readable syntax major parts of the formal system underlying the operation of NetSketch, along with its semantics and a corresponding notion of validity. We then provide a proof of soundness for the formalism that can be partially verified using a lightweight formal reasoning system that simulates natural contexts. A traditional version of these definitions and arguments can be found in a related paper \cite{BUCS-TR-2009-029}.

NetSketch is a tool for the specification of constrained-flow applications and the certification of desirable safety properties imposed thereon. NetSketch is conceived to assist system integrators in two types of activities: modeling and design. As a modeling tool, it enables the abstraction of an existing system while retaining sufficient information about it to carry out future analysis of safety properties. As a design tool, NetSketch enables the exploration of alternative safe designs as well as the identification of minimal requirements for outsourced subsystems. NetSketch embodies a lightweight formal verification philosophy, whereby the power (but not the heavy machinery) of a rigorous formalism is made accessible to users via a friendly interface. NetSketch does so by exposing tradeoffs between exactness of analysis and scalability, and by combining traditional whole-system analysis with a more flexible compositional analysis. The compositional analysis is based on a strongly-typed Domain-Specific Language (DSL) for describing and reasoning about constrained-flow networks at various levels of sketchiness along with invariants that need to be enforced thereupon. In this paper, we define the formal system underlying the operation of NetSketch, in particular the DSL behind NetSketch's user-interface when used in ``sketch mode'', and prove its soundness relative to appropriately-defined notions of validity. In a companion paper \cite{BUCS-TR-2009-028}, we overview NetSketch, highlight its salient features, and illustrate how it could be used in two applications: the management/shaping of traffic flows in a vehicular network (as a proxy for CPS applications) and in a streaming media network (as a proxy for Internet applications).

"NetSketch is a tool that enables the specification of network-flow applications and the certification of desirable safety properties imposed thereon. NetSketch is conceived to assist system integrators in two types of activities: modeling and design. As a modeling tool, it enables the abstraction of an existing system while retaining sufficient information about it to enable future analysis of safety properties. As a design tool, NetSketch enables the exploration of alternative safe designs as well as the identification of minimal requirements for outsourced subsystems. NetSketch embodies a lightweight formal verification philosophy, whereby the power (but not the heavy machinery) of a rigorous formalism is made accessible to users via a friendly interface. NetSketch does so by exposing tradeoffs between exactness of analysis and scalability, and by combining traditional whole-system analysis with a more flexible compositional analysis. The compositional analysis is based on a strongly-typed Domain-Specific Language (DSL) for describing network configurations at various levels of sketchiness along with invariants that need to be enforced thereupon. In this paper, we overview NetSketch, highlight its salient features, and illustrate how it could be used in two applications: the management/shaping of traffic flows in a vehicular network (as a proxy for CPS applications) and in a streaming media network (as a proxy for Internet applications). In a companion paper, we define the formal system underlying the operation of NetSketch, in particular the DSL behind NetSketch's user-interface when used in ``sketch mode'', and prove its soundness relative to appropriately-defined notions of validity.

In research areas involving mathematical rigor, there are numerous benefits to adopting a formal representation of models and arguments: reusability, automatic evaluation of examples, and verification of consistency and correctness. However, broad accessibility has not been a priority in the design of formal verification tools that can provide these benefits. We propose a few design criteria to address these issues by drawing on our own reasoning as well as that of existing work: (1) a simple, familiar, and conventional concrete syntax that is independent of any environment, application, or veri- fication strategy; (2) extensive native support for at least basic constructions and practices related to logical reasoning, arithmetic, naive set theory, algebraic manipulation, and evaluation of simple functions; and (3) a lightweight underlying structure that reduces workload and entry costs by allowing users to employ features selectively and by automatically managing multiple logical systems without requiring a user's involvement or technical knowledge.

We demonstrate the feasibility of satisfying these criteria by presenting our own formal representation and verification system. Our system's simple concrete syntax overlaps with English, LATEX and MediaWiki markup. The system's underlying verifier demonstrates our main contributions. It relies on heuristic search techniques, data structures, syntactic analyses, and normal forms to make the proof authoring process more manageable and consistent with prevailing practices. Furthermore, its underlying logic consists of a symbolic template that enables lightweight verification but can also be used to automatically manage multiple logical systems through straightforward syntactic restrictions.

We first introduce a very simple typed language for expressing allocation algorithms that allows automatic verification that an algorithm is monotonic and therefore truthful. The analysis of truthfulness is accomplished using a syntax-directed transformation which constructs a proof of monotonicity based on an exhaustive critical-value analysis of the algorithm. We then define a more high-level, general-purpose programming language with typical constructs, such as those for defining recursive functions, along with primitives that match allocation algorithm combinators found in the work of Mu'alem and Nisan. We demonstrate how this language can be used to combine both primitive and user-defined combinators, allowing it to capture a collection of basic truthful allocation algorithms. In addition to demonstrating the value of programming language design techniques in application to a specific domain, this work suggests a blueprint for interactive tools that can be used to teach the simple principles of truthful mechanism design.