Between Dec 19, 2024 and Jan 2, 2025, datasets can be submitted to DRUM but will not be processed until after the break. Staff will not be available to answer email during this period, and will not be able to provide DOIs until after Jan 2. If you are in need of a DOI during this period, consider Dryad or OpenICPSR. Submission responses to the UDC may also be delayed during this time.

Browsing by Subject "Verification"

Now showing 1 - 2 of 2
  • Thumbnail Image
    Item
    The “Print o’Life”: Transitions of Text and the Early Modern Stage
    (2024) Biesel, Clara
    Although printing first came to England nearly a century before Shakespeare’s birth, within his lifetime, the use of print quadrupled. This project considers the affective responses visible in Shakespeare’s plays and a pair of contemporary texts (Helkiah Crooke’s anatomy textbook Mikrokosmographia and Martin Billingsley’s handwriting manual The Pen’s Excellencie) as individuals react to the cultural transition from texts produced primarily by hand to texts produced by machine. When read in parallel, these texts reveal a striking ambivalence present in their society as individuals come to grips with how a new technology is changing their understanding of themselves, evoking anxiety over an imagined future and nostalgia for an imagined past. In the context of this transition, richly embodied metaphors consider books imagined as bodies and bodies read as though they were books. The metaphors present bodies and books as though similar enough to be interchangeable, but those using these metaphors (in plays and elsewhere) fail to sustain the comparison. As books replace a physical, “in-person experience” with the printed word, the texts themselves reveal a sense of loss. Be it an anatomist unfolding the interior of a human cadaver which is missing, or direct instruction from a calligraphy teacher demonstrating the proper technique of the hand and the pen, or the living, collaborative, embodied performance of a play, these texts reveal the nostalgia and anxiety about the change towards the printed form. This project pulls together themes and methods from a variety of scholarly fields including print and book history, technology and medical humanities, studies of embodiment (including questions of race and gender), epistemology or knowledge studies, as well as performance, strengthening the connections and intersections between them.
  • Thumbnail Image
    Item
    Verification of Recursive Data Types using abstractions
    (2014-03) Pham, Hung Tuan
    Reasoning about functions that operate over algebraic data types is an important problem for a large variety of applications. One application of particular interest is network applications that manipulate or reason about complex message structures, such as XML messages. In this dissertation, we present a decision procedure for reasoning about algebraic data types using abstractions that are provided by catamorphisms: fold functions that map instances of algebraic data types into values in a decidable domain. We show that the procedure is sound and complete for a class of monotonic catamorphisms. Our work extends a previous decision procedure that unrolls catamorphism functions until a solution is found. We propose the categories of monotonic catamorphisms and associative-commutative catamorphisms, which we argue provide a better formal foundation than previous categorizations of catamorphisms. We use monotonic catamorphisms to address an incompleteness in the previous unrolling algorithm (and associated proof), and then use these notions to address two open problems from previous work: (1) we provide a bound on the number of unrollings necessary for completeness, showing that it is exponentially small with respect to formula size for associative-commutative catamorphisms, and (2) we demonstrate that associative-commutative catamorphisms can be combined within a formula whilst preserving completeness. Our combination results extend the set of problems that can be reasoned about using the catamorphism-based approach. In addition, we generalize certain kinds of catamorphism functions to support additional parameters. This extension, called parameterized associative-commutative catamorphisms subsumes the associative-commutative class, widens the set of functions that are known to be decidable, and makes several practically important functions (such as forall, exists, and member) over elements of algebraic data types straightforward to express. We also describe an implementation of the approach, called RADA, which accepts formulas in an extended version of the SMT-Lib2 syntax. The procedure is quite general and is central to the reasoning infrastructure for Guardol, a domain-specific language for reasoning about network guards.