James Caldwell, Ph.D. - US grants

Revascularization reverses chronic ventricular dysfunction, a major determinant of survival, in some patients with coronary disease. Identification of chronically underperfused but viable (hibernating) myocardium is an important diagnostic goal. We have developed a method for detecting chronically hypoxic but viable myocardium noninvasively using 18F-fluoromisonidazole (FMISO) and positron emission tomography (PET). In pilot PET studies we have demonstrated FMISO trapping in humans with chronic ischemic heart disease, and in animal studies, that FMISO is a more sensitive indicator of ischemia than 18F-fluorodeoxyglucose (FDG). The specific aims of this proposal are to: Aim 1: Compare 18F-FMISO images to 18F-FDG uptake/myocardial blood flow (15O-water) mismatch images in patients with regional ventricular dysfunction before and after revascularization to establish the relative sensitivity/specificity of the two methods for predicting functional recovery. We hypothesize that FMISO will prove to be a sensitive indicator of myocardial viability and that reversal of chronic hypoxia will correlate with contractile improvement. Aim 2. Develop and validate new positron labeled hypoxia tracers that exhibit more rapid oxygen-sensitive bioreduction and accelerated plasma clearance than FMISO, potentially allowing shorter imaging protocols and the detection of acute ischemia. We will synthesize and radiolabel new nitroimidazole analogues (among others, 4-methyl-2-nitroimidazole, 4- hydroxymethyl-2-nitroimidazole and 2-nitroimidazole-4-carboxylic acid) whose chemical characteristics appear favorable for hypoxia imaging. These compounds will be evaluated by biodistribution studies in rats and by oxygen-sensitivity studies in isolated adult rat myocytes. For analogues with the greatest oxygen-sensitivity and fastest blood clearance, PET studies will be performed in a canine model of prolonged ischemia with reversible regional dysfunction. The ultimate goal of this project is to validate and optimize the use of hypoxia markers and PET for the noninvasive evaluation of patients with regional ventricular dysfunction who may benefit from revascularization.

Revascularization reverses chronic ventricular dysfunction, a major determinant of survival, in some patients with coronary disease. Identification of chronically underperfused but viable (hibernating) myocardium is an important diagnostic goal. We have developed a method for detecting chronically hypoxic but viable myocardium noninvasively using 18F-fluoromisonidazole (FMISO) and positron emission tomography (PET). In pilot PET studies we have demonstrated FMISO trapping in humans with chronic ischemic heart disease, and in animal studies, that FMISO is a more sensitive indicator of ischemia than 18F-fluorodeoxyglucose (FDG). The specific aims of this proposal are to: Aim 1: Compare 18F-FMISO images to 18F-FDG uptake/myocardial blood flow (15O-water) mismatch images in patients with regional ventricular dysfunction before and after revascularization to establish the relative sensitivity/specificity of the two methods for predicting functional recovery. We hypothesize that FMISO will prove to be a sensitive indicator of myocardial viability and that reversal of chronic hypoxia will correlate with contractile improvement. Aim 2. Develop and validate new positron labeled hypoxia tracers that exhibit more rapid oxygen-sensitive bioreduction and accelerated plasma clearance than FMISO, potentially allowing shorter imaging protocols and the detection of acute ischemia. We will synthesize and radiolabel new nitroimidazole analogues (among others, 4-methyl-2-nitroimidazole, 4- hydroxymethyl-2-nitroimidazole and 2-nitroimidazole-4-carboxylic acid) whose chemical characteristics appear favorable for hypoxia imaging. These compounds will be evaluated by biodistribution studies in rats and by oxygen-sensitivity studies in isolated adult rat myocytes. For analogues with the greatest oxygen-sensitivity and fastest blood clearance, PET studies will be performed in a canine model of prolonged ischemia with reversible regional dysfunction. The ultimate goal of this project is to validate and optimize the use of hypoxia markers and PET for the noninvasive evaluation of patients with regional ventricular dysfunction who may benefit from revascularization.

technology /technique development; positron emission tomography; human tissue; cardiovascular system; biomedical resource; bioengineering /biomedical engineering; Mammalia;

We will test the hypothesis that in heart failure and sudden death, heterogeneity and/or mismatch of pre- and post-synaptic regional cardiac SNS function are specific indicators of the extent and mechanisms of the diseases. Specifically, we hypothesize that the role of the cardiac SNS can be tested by in vivo quantitative measures of regional pre- and post-synaptic function. There is substantial evidence to support the concept that aberrations in cardiac SNS function contribute to and may be primarily responsible for the morbidity and mortality associated with sudden cardiac death (SCD) and congestive heart failure (CHF), two illnesses that are major public health problems. Aim 1 will demonstrate that pre- and post-synaptic cardiac function can be quantified over a wide range of neuronal function using physiologically realistic blood-tissue exchange models that are directly applicable to PET imaging studies. These experiments will be performed in isolated perfused hearts and in vivo canine hearts. Aim 2a is a pilot human study to test the hypothesis that quantitation of regional SNS dysfunction, using physiologically realistic models, will differentiate patients with recurrent SCD from those experiencing only a single episode and that the new analysis methods for both pre-and post-synaptic function are more definitive than are qualitative methods for evaluating SNS function. Aim 2b is a pilot human study to test the hypothesis that modulation of cardiac sympathetic function by central inhibition of the SNS in patients with CHF can be demonstrated by quantitation of regional pre-and post synaptic function. When related to changes in regional myocardial flow and metabolism, this quantitative approach provides a tool for understanding mechanisms of CHF and for evaluating new therapeutic strategies.

We will test the hypothesis that in heart failure and sudden death, heterogeneity and/or mismatch of pre- and post-synaptic regional cardiac SNS function are specific indicators of the extent and mechanisms of the diseases. Specifically, we hypothesize that the role of the cardiac SNS can be tested by in vivo quantitative measures of regional pre- and post-synaptic function. There is substantial evidence to support the concept that aberrations in cardiac SNS function contribute to and may be primarily responsible for the morbidity and mortality associated with sudden cardiac death (SCD) and congestive heart failure (CHF), two illnesses that are major public health problems. Aim 1 will demonstrate that pre- and post-synaptic cardiac function can be quantified over a wide range of neuronal function using physiologically realistic blood-tissue exchange models that are directly applicable to PET imaging studies. These experiments will be performed in isolated perfused hearts and in the in vivo canine hearts. Aim 2a is a pilot human study to test the hypothesis that quantitation of regional SNS dysfunction, using physiologically realistic models, will differentiate patients with recurrent SCD from those experiencing only a single episode and that the new analysis methods for both pre- and post-synaptic function are more definitive than are qualitative methods for evaluating SNS function. Aim 2b is a pilot human study to test the hypothesis that modulation of cardiac sympathetic function by central inhibition of the SNS in patients with CHF can be demonstrated by quantitation of regional pre-and post synaptic function. When related to changes in regional myocardial flow and metabolism, this quantitative approach provides a tool for understanding mechanisms of CHF and for evaluating new therapeutic strategies. Aim 1 will demonstrate that pre- and post-synaptic cardiac function can be quantified over a wide range of neuronal function using physiologically realistic blood-tissue exchange models that are directly applicable to PET imaging studies. These experiments will be performed in isolated perfused hearts and in vivo canine hearts. Aim 2a is a pilot human study to test the hypothesis that quantitation of regional SNS dysfunction, using physiologically realistic models, will differentiate patients with recurrent SCD from those experiencing only a single episode and that the new analysis methods for both pre- and post-synaptic function are more definitive than are qualitative methods for evaluating SNS function. Aim 2b is a pilot human study to test the hypothesis that modulation of cardiac sympathetic function by central inhibition of the SNS in patients with CHF can be demonstrated by quantitation of regional pre-and post synaptic function. When related to changes in regional myocardial flow and metabolism, this quantitative approach provides a tool for understanding mechanisms of CHF and for evaluating new therapeutic strategies.

CCR-9985239
CAREER: A Formal Programming Methodology with Applications to
Developing Automated Verifiers
PI: James L. Caldwell

The goals of this research are (i) the development of new methods for
formal program development which combine existing approaches to
verification and synthesis; (ii) the application of those methods to
the development of correct-by-construction verification engines; and
(iii) integrating the formalized mathematics that supports these
methods into the undergraduate computer science curriculum. In
program development practice it is sometimes more expedient to verify
a known program, while at other times, synthesis is the better
approach. The research investigates methods of combining these
complementary modes of development within a single framework to
justify the correctness of complex software artifacts. The work
largely takes place within the framework of the constructive type
theory provided by the Nuprl system. This new method of program
development is applied and refined in the context of efforts to secure
correct implementations of automated verifiers; model checkers and
decision procedure based verification engines. The digital
representations of mathematical definitions, proofs, proof strategies,
and theorems that support this mode of program development formally
encode the applied mathematics of Computer Science. This research
explores new ways to incorporate this material in the undergraduate
classroom.

EIA-0216592
James L .Caldwell
Jeffrey Van Baalen
Gamboa Ruben

MRI: Acquisition of a Network of Workstations Serving as a Platform for Distributed Automated Reasoning

This proposal from an EPCoR state, adapting current parallel and distributed theorem
proving technology to a setting in which different computation servers become available in an unpredictable fashion, aims at building a network of workstations that can be used as a computational server for research. A cluster of high-performance workstations running Linux and the required networking infrastructure will be acquired. The effort will make available a large proportion of the computational facilities of the department for theorem proving efforts. In this setting, the search for the proof of a single theorem will be spread between all the idle workstations participating in the distributed proof effort.
In extending model checking to infinite state spaces, the research involves exploring two approaches for protocol verification: Development of,
1. On-the-fly model checker based on a 3-values logic and,
2. Theorem proving methods that can reduce a protocol's state space to a finite size.

Directorate for Computer and Information Science and Engineering (CISE)
Division Computer and Network Systems (CNS)
Science of Design (SoD) Program

Proposal Number: 0613919
P/I: Ruben Gamboa
Institution: University of Wyoming

Title: "SoD-HCER: Comprehensibility as a Design Criterion"

Award: $ 157,428
Duration: 24 months


The focus of this project is on software design comprehensibility where an objective measure of comprehensibility is proposed that can be determined by the use of automated techniques for detecting program constraints. Using comprehensibility as a criterion for evaluating designs poses a major intellectual challenge because comprehensibility is a subjective notion that complicates the task of detecting it automatically. The proposers' approach toward detecting comprehensibility is to modify two program analysis tools (Daikon and AbsInt) so that those tools can be used to comprehend "good" designs. The project has two main research goals: a) Determine if comprehensibility captures the informal notion of "good" design. This goal represents the empirical validation (or refutation) of the main thesis, that comprehensibility is the key quality shared by good designs; and, b) Identify design features that make designs more comprehensible. The intent here is to analyze different programs that are freely accessible on the Internet to identify designs that are easily comprehended by the tools, and then to see what design features they have in common. This is a highly speculative goal, but it is the main scientific question raised by the research. Moreover, it is one that can have a broad impact on the practice of programming. The thesis of this project, that comprehensibility can be used as a single criterion for evaluating design quality and that this criterion can be measured objectively by using automated tools that infer meaning from programs, provides a single and testable criterion to measure quality. This research brings the art of software design one step closer to a scientific footing. An early benefit of this project will be the identification of design features that lead to greater comprehensibility, hence to better design quality. Moreover, the integration of automated tools to measure design quality objectively is an aspect of this proposal that is unique and innovative. If successful, the project may contribute to the body of knowledge of the science of design by presenting "good" design precepts for practitioners to follow. In addition, the proposed research has the potential to make a significant impact both on computer science education and on the practice of programming in general. If this project is successful in establishing that comprehensibility is an adequate measure of design quality, students and professional designers will have a new and objective way to judge different designs.

Program Manager: Anita J. La Salle
Date: June 28, 2006