Floyd-Hoare Verifiers "Considered Harmful"

The Floyd-Hoare methodology completely dominates the field of program verification and has contributed much to our understanding of how programs might be analyzed. Useful but limited verifiers have been developed using Floyd-Hoare techniques. However, it has long been known that it is difficult to handle side effects on shared data structures within the Floyd-Hoare framework. Most examples of successful Floyd-Hoare axioms for assignment to complex data structures, similar statements have been used by London. This paper demonstrates an error in these formalizations and suggests a different style of verification.

Inspection Methods in Programming

The work reported here lies in the area of overlap between artificial intelligence software engineering. As research in artificial intelligence, it is a step towards a model of problem solving in the domain of programming. In particular, this work focuses on the routine aspects of programming which involve the application of previous experience with similar programs. I call this programming by inspection. Programming is viewed here as a kind of engineering activity. Analysis and synthesis by inspection area prominent part of expert problem solving in many other engineering disciplines, such as electrical and mechanical engineering. The notion of inspections methods in programming developed in this work is motivated by similar notions in other areas of engineering. This work is also motivated by current practical concerns in the area of software engineering. The inadequacy of current programming technology is universally recognized. Part of the solution to this problem will be to increase the level of automation in programming. I believe that the next major step in the evolution of more automated programming will be interactive systems which provide a mixture of partially automated program analysis, synthesis and verification. One such system being developed at MIT, called the programmer's apprentice, is the immediate intended application of this work. This report concentrates on the knowledge are of the programmer's apprentice, which is the form of a taxonomy of commonly used algorithms and data structures. To the extent that a programmer is able to construct and manipulate programs in terms of the forms in such a taxonomy, he may relieve himself of many details and generally raise the conceptual level of his interaction with the system, as compared with present day programming environments. Also, since it is practical to expand a great deal of effort pre-analyzing the entries in a library, the difficulty of verifying the correctness of programs constructed this way is correspondingly reduced. The feasibility of this approach is demonstrated by the design of an initial library of common techniques for manipulating symbolic data. This document also reports on the further development of a formalism called the plan calculus for specifying computations in a programming language independent manner. This formalism combines both data and control abstraction in a uniform framework that has facilities for representing multiple points of view and side effects.

Targeted Stimuli-Responsive Dextran Conjugates for Doxorubicin Delivery to Hepatocytes

A targeted, stimuli-responsive, polymeric drug delivery vehicle is being developed in our lab to help alleviate severe side-effects caused by narrow therapeutic window drugs. Targeting specific cell types or organs via proteins, specifically, lectin-mediated targeting holds potential due to the high specificity and affinity of receptor-ligand interactions, rapid internalization, and relative ease of processing. Dextran, a commercially available, biodegradable polymer has been conjugated to doxorubicin and galactosamine to target hepatocytes in a three-step, one-pot synthesis. The loading of doxorubicin and galactose on the conjugates was determined by absorbance at 485 nm and elemental analysis, respectively. Conjugation efficiency based on the amount loaded of each reactant varies from 20% to 50% for doxorubicin and from 2% to 20% for galactosamine. Doxorubicin has also been attached to dextran through an acid-labile hydrazide bond. Doxorubicin acts by intercalating with DNA in the nuclei of cells. The fluorescence of doxorubicin is quenched when it binds to DNA. This allows a fluorescence-based cell-free assay to evaluate the efficacy of the polymer conjugates where we measure the fluorescence of doxorubicin and the conjugates in increasing concentrations of calf thymus DNA. Fluorescence quenching indicates that our conjugates can bind to DNA. The degree of binding increases with polymer molecular weight and substitution of doxorubicin. In cell culture experiments with hepatocytes, the relative uptake of polymer conjugates was evaluated using flow cytometry, and the killing efficiency was determined using the MTT cell proliferation assay. We have found that conjugate uptake is much lower than that of free doxorubicin. Lower uptake of conjugates may increase the maximum dose of drug tolerated by the body. Also, non-galactosylated conjugate uptake is lower than that of the galactosylated conjugate. Microscopy indicates that doxorubicin localizes almost exclusively at the nucleus, whereas the conjugates are present throughout the cell. Doxorubicin linked to dextran through a hydrazide bond was used to achieve improved killing efficiency. Following uptake, the doxorubicin dissociates from the polymer in an endosomal compartment and diffuses to the nucleus. The LC₅₀ of covalently linked doxorubicin is 7.4 μg/mL, whereas that of hydrazide linked doxorubicin is 4.4 μg/mL.