Typescript (photocopy). / Digitized by Kansas Correctional Industries

Operating systems software is fundamental to modern computer systems: all other applications are dependent upon the correct and timely provision of basic system services. At the same time, advances in programming languages and type theory have lead to the creation of functional programming languages with type systems that are designed to combine theorem proving with practical systems programming. The Terrier operating system project focuses on low-level systems programming in the context of a multi-core, real-time, embedded system, while taking advantage of a dependently typed programming language named ATS to improve reliability. Terrier is a new point in the design space for an operating system, one that leans heavily on an associated programming language, ATS, to provide safety that has traditionally been in the scope of hardware protection and kernel privilege. Terrier tries to have far fewer abstractions between program and hardware. The purpose of Terrier is to put programs as much in contact with the real hardware, real memory, and real timing constraints as possible, while still retaining the ability to multiplex programs and provide for a reasonable level of safety through static analysis.

A linguagem C não provê segurança espacial de memória: não garante que a memória acessada através de um ponteiro para um objeto, tal como um vetor, de fato pertence ao objeto em questão. Em vez disso, o programador é responsável por gerenciar informações de alocações e limites, e garantir que apenas acessos válidos à memória são realizados pelo programa. Por um lado, isso provê flexibilidade: o programador tem controle total sobre o layout dos dados em memória, e sobre o momento em que verificações são realizadas. Por outro lado, essa é uma fonte frequente de erros e vulnerabilidades de segurança em programas C. Diversas técnicas já foram propostas para prover segurança de memória em C. Tipicamente tais sistemas mantêm suas próprias informações de limites e instrumentam o programa para garantir que a segurança de memória não seja violada. Isso causa uma série de inconvenientes, tais como mudanças no layout de memória de estruturas de dados, quebrando assim a compatibilidade binária com bibliotecas externas, e/ou um aumento no consumo de memória. Uma abordagem diferente consiste em usar tipos dependentes para descrever a informação de limites já latente em programas C e assim permitir que o compilador use essa informação para garantir a segurança espacial de memória. Embora tais sistemas tenham sido propostos no passado, eles estão atrelados especificamente à linguagem C. Outras linguagens, como C++, sofrem de problemas similares de segurança de memória, e portanto poderiam se beneficiar de uma abordagem mais independente de linguagem. Este trabalho propõe Týr, uma transformação de código baseada em tipos dependentes para garantir a segurança espacial de memória de programas C ao nível LLVM IR. O sistema permite que o programador descreva no nível dos tipos as relações entre pointeiros e informação de limites já presente em programas C. Dessa maneira, Týr provê segurança espacial de memória verificando o uso consistente desses metadados pré-existentes, através de verificações em tempo de execução inseridas no programa guiadas pela informação de tipos dependentes. Ao trabalhar no nível mais baixo do LLVM IR, Týr tem por objetivo ser usável como uma fundação para segurança espacial de memória que possa ser facilmente estendida no futuro para outras linguagens compiláveis para LLVM IR, tais como C++ e Objective C. Demonstramos que Týr é eficaz na proteção contra violações de segurança espacial de memória, com um overhead de tempo de execução relativamente baixo e de consumo de memória próximo de zero, atingindo assim um desempenho competitivo com outros sistemas para segurança espacial de memória de uma maneira mais independente de linguagem. / The C programming language does not enforce spatial memory safety: it does not ensure that memory accessed through a pointer to an object, such as an array, actually belongs to that object. Rather, the programmer is responsible for keeping track of allocations and bounds information and ensuring that only valid memory accesses are performed by the program. On the one hand, this provides flexibility: the programmer has full control over the layout of data in memory, and when checks are performed. On the other hand, this is a frequent source of bugs and security vulnerabilities in C programs. A number of techniques have been proposed to provide memory safety in C. Typically such systems keep their own bounds information and instrument the program to ensure that memory safety is not violated. This has a number of drawbacks, such as changing the memory layout of data structures and thus breaking binary compatibility with external libraries and/or increased memory usage. A different approach is to use dependent types to describe the bounds information already latent in C programs and thus allow the compiler to use that information to enforce spatial memory safety. Although such systems have been proposed before, they are tied specifically to the C programming language. Other languages such as C++ suffer from similar memory safety problems, and thus could benefit from a more language-agnostic approach. This work proposes Týr, a program transformation based on dependent types for ensuring spatial memory safety of C programs at the LLVM IR level. It allows programmers to describe at the type level the relationships between pointers and bounds information already present in C programs. In this way, Týr ensures spatial memory safety by checking the consistent usage of this pre-existing metadata, through run-time checks inserted in the program guided by the dependent type information. By targeting the lower LLVM IR level, Týr aims to be usable as a foundation for spatial memory which could be easily extended in the future to other languages that can be compiled to LLVM IR, such as C++ and Objective C. We show that Týr is effective at protecting against spatial memory safety violations, with a reasonably low execution time overhead and nearly zero memory consumption overhead, thus achieving performance competitive with other systems for spatial memory safety, in a more language-agnostic way.

Comme les syst`emes mat´eriels et logiciels grandissent de fa¸con continue en ´echelle et fonctionnalit´es, la probabilit´e d’erreurs subtiles de- vient toujours plus grande. Les techniques d’abstraction, souvent bas´ees sur l’interpr´etation abstraite de Cousot, fournissent une m´ethode pour ex´ecuter symboliquement les syst`emes en utilisant le domaine abstrait `a la place du domaine concret. Dans cette th`ese, on introduit des techniques d’abstraction pour les logiques sous des interpr´etations multi-valu´ees. Beaucoup d’applications des logiques multi-valu´ees ont ´et´e trouv´ees dans la v´erification du mat´eriel et du logiciel. Pour la v´erification du mat´eriel, des outils de simulation et des r´ealisations des circuits multi-valu´es v´eritables ont ´et´e propos´es, les risques dynamiques ont ´et´e model´es en introduisant des ´etats faux pour trouver des r´egions chevauchantes des signaux en concurrence, etc. Pour la v´erification du logiciel on a besoin d’incertitude parce qu’on ne peut savoir si certains comportements devraient ˆetre possibles et on a besoin du d´esaccord parce que l’on peut avoir des acteurs diff´erents qui sont en d´esaccord pour la mani`ere dont les syst`emes devraient se comporter. Les abstractions sont obtenues en appliquant des relations d’´equivalence et apr`es, les symboles pr´edicatifs de la logique sont red´efinis `a s’appliquer cor- rectement aux classes d’´equivalence `a l’aide des politiques d’interpr´etation. On fournit des r´esultats de pr´eservation pour la logique de premier ordre, pour la logique temporelle et pour la logique temporelle de la connaissance. Avant de discuter les abstractions multi-valu´ees pour la logique temporelle, nous pr´esentons une ´etude de cas pour utiliser l’abstraction dans le contexte des mod`eles du contrˆole d’acc`es. Nous fournirons aussi une technique d’abstraction pour les types de do- nn´ees. Cette technique d’abstraction peut ˆetre ´elargie pour les types abstraits de donn´ees. Ici, les abstractions sont appliqu´ees aux sp´ecifications initiales au moyen des ´equations et ils sont appel´es des abstractions ´equationnelles. De plus, la technique d’abstraction pr´esent´ee g´en´eralise et clarifie la nature de beaucoup de techniques d’abstraction trouv´ees dans la litt´erature, telles: la technique de dupliquer les symboles pr´edicatifs, shape analysis, l’abstraction par pr´edicats, l’approche de McMillan, etc. Pour raisonner au sujet des syst`emes dynamiques, on introduit les types de donn´ees dynamiques et on ´etend la m´ethode d’abstraction ant´erieure `a ce cas. Le probl`eme principal qui survient quand on utilise les abstractions est de trouver l’abstraction convenable ou de raffiner une abstraction d´ej`a existante pour en obtenir une meilleure. On prouve que les techniques d’abstraction que nous avons introduites pour les types de donn´ees sous l’interpr´etation 3- valu´ee Kleene, peuvent ˆetre utilis´ees dans une proc´edure de raffinement. De plus, on montre que la proc´edure de raffinement guid´e par contre-exemple est plus efficace quand on l’utilise sous les abstractions ´equationnelles / As the hardware and software systems are growing continuously in scale and functionality, the likelihood of subtle errors becomes greater. Abstraction techniques, often based on abstract interpretation, provide a method for symbolically executing systems using the abstract instead of the concrete domain. In this thesis, we are concerned with abstractions for logics under multi-valued interpretations. Many applications of multi-valued logics have been found in hardware and software verification. For hardware verification, simulation tools and imple- mentations of genuinely multi-valued circuits have been proposed, dynamic hazards have been modeled by introducing pseudo states to find overlapping regions of competing signals, implementation of gates have been verified on the basis of switch level models, etc. For software verification, we need uncer- tainty because we may not know whether some behaviors should be possible, we need disagreement because we may have different stakeholders that dis- agree about how the systems should behave and we need to represent relative importance because some behaviors are essential and others may or may not be implemented. The abstractions are obtained by applying equivalence relations and then, the predicate symbols of the logic are re-defined to work properly on equiva- lence classes by using interpretation policies. We provide preservation results for first-order logic, temporal logic, and temporal logic of knowledge. As a case study, we show how abstraction can be used to solve the safety problem for protection systems which model access control policies. The use of abstraction in the context of data types, is also investigated. This technique scales well from data types to abstract data types. Here, abstractions are applied to initial specifications by means of equations and they are called equationally specified abstractions. Moreover, the abstraction technique we propose generalizes and clarifies the nature of many abstraction techniques found in the literature, such as the technique of duplicating pred- icate symbols, shape analysis, predicate abstraction, McMillan’s approach, etc. To reason about dynamic systems, we introduce dynamic data types and extend the previous abstraction technique to this case. The main problem that arises when using abstraction techniques is to find the suitable abstraction or to refine an already existing abstraction in order to obtain a better one. In this thesis, we prove that the abstraction techniques for data types, under Kleene’s three-valued interpretation, can be used in a refinement procedure. Moreover, we show that the counterexample guided abstraction refinement procedure (CEGAR) works better when used with equationally specified abstractions

This thesis describes research into the role of various factors in novice program comprehension, including the underlying programming paradigm, the representational features of the programming language, and the various types of information which can be derived from the program. The main postulate of the thesis is that there is no unique method for understanding programs, and that program comprehension will be influenced by, among other things, the way in which programs are represented, both semantically and syntactically. This idea has implications for the learning of programming, particularly in terms of how theses concepts should be embodied. The thesis is focused around three empirical studies. The first study, based on th so-called "information types" studies, challenged the idea that program comprehension is an invariant process over languages, and suggested that programming language will have a differential effect on comprehension, as evidenced by the types of information which novices are able to extract from a program. Despite the use of a markedly different language from earliier studies, the results were broadly similar. However, it was suggested that there are other factors additional to programming notation which intervene in the comprehension process, and which cannot be discounted. Furthermore, the study highlighted the need to tie the hypotheses about information extraction more closely to the programming paradigm. The second study introduced a graphical component into the investigation, and looked at the way in which visual representations of programs combine with programming paradigm to influence comprehension. The mis-match conjecture, which suggests that tasks requiring information which is highlighted by a notation will be facilitated relative to tasks where the information must be inferred, was applied to programming paradigm. The study showed that the mis-match effect can be overridden by other factors, most notably subjects' prior experience and the programming culture in which they are taught. The third study combined the methodologies of the first two studies to look at the mis-match conjecture within the wider context of information types. Using graphical representations of the control flow and data flow paradigms, it showed that, despite a bias toward one paradigm based on prior experience and culture, programming paradigm does influence the way in which the program is understood, resulting in improved performance on tasks requiring information which the paradigm is hypothesised to highlight. Furthermore, this effect extends to groups of information which could be said to be theoretically related to the information being highlighted. The thesis also proposes a new and more precise methodology for the analysis of students' accounts of their comprehension of a program, a form a data which is typically derived from the information types studies. It then shows how an analysis of this qualitative data can be used to provide further support for the quantitative results. Finally, the thesis suggests how the core results could be used to develop computer based support environments for novice visual programming, and provides other suggestions for further work.

Children who have developmental disorders that involve memorial deficits and impairments in social interaction and communication, such as Autism Spectrum Disorders (ASD), can present challenges to professionals seeking their testimony when they are victims or witnesses of a crime. Most forensic interviews involve long delays after an event, underscoring the importance of conducting experimental studies which consider the effect of delay on children's memory. In this research, fifty-nine children (age 6-15 years) with ASD (N=27) and without disabilities (N=32) were questioned about their participation in a set of activities after a two-week delay and again after a two-month delay, using the Revised National Institute of Child Health and Human Development (NICHD) Investigative Interview Protocol. A detailed coding scheme was designed to code and analyse the interviewers' utterances and the children's responses in 118 interviews. Transcripts were coded for completeness (with respect to the gist of the event), amount of narrative details, and accuracy. Results indicated that autistic children did not differ from typically developing (TD) peers on any dimensions of memory after both delays. Specifically, both groups of children provided equivalently complete accounts on both occasions. However, children in both groups provided significantly fewer narrative details about the event in the second interview, and the accuracy rates were lower. Recall prompts elicited more detailed and more accurate responses from children in both groups than recognition prompts. Although autistic children recalled fewer correct narrative details than TD peers when questioned using open-ended recall prompts, they were as accurate as TD peers in response to recognition prompts. The informativeness and accuracy of children's reports remained unchanged over time. Finally, social support was beneficial when children were interviewed for the first time but not after a longer delay. The findings indicate that autistic children can provide meaningful and reliable testimony about an event they personally experienced, but several aspects of their memory reports deteriorate over time.

Studies have shown an increase in student achievement when educational partnerships between families and schools exist. At the elementary school that was the focus of this study, there had once been a thriving family involvement program; however, the number of family-school partnerships had declined in recent years. Students, families, and teachers needed improved knowledge of the types of family involvement programs that everyone would be willing to participate in to increase student learning and achievement. The purpose of this case study was to determine whether the types of involvement currently offered to families at the elementary school matched the types of involvement in which families would be willing to participate. The study also determined which types of involvement teachers were currently providing and which they would be willing to provide. Epstein's 6 types of family involvement were used as a conceptual foundation for this case study. The study used questionnaires, focus groups, and interviews to collect data from 14 teachers and 25 families. The key research question involved determining what teachers and families were willing to participate in to increase partnerships and involvement. Surveys, focus group transcripts, and interview transcripts were analyzed for themes. A data spiral was used to analyze the data, and triangulation and peer review were used to ensure trustworthiness of the findings. By implementing the suggestions from this study, including more communication and family input, the elementary school may form more partnerships with families and the community, which may help to increase involvement and ultimately improve student achievement. This study offers implications for social change by helping create an atmosphere where the school, families, and community work together to help students succeed.

Conformal antennas have widespread applications in communication systems for vehicular bodies, aircrafts, and spacecrafts etc. They are non-protruding and can arbitrarily take any shape on the surface where they are etched. This thesis is a summary of two main projects. The first project employs a conformal array of four S-band and four GPS-band antennas for sub-payload of a sounding rocket. The sub-payload is a small cylinder and therefore the eight conformal antennas are based on curved patch geometry. The second project employs a conformal antenna for a CubeSat. The antenna is based on a cavitybacked slot and therefore can be conveniently integrated around the surface-mount solar cells of the CubeSat. Such an integration has enormous merits for CubeSat because there is no competition between the antennas and solar cells for the limited surface real estate. The antenna design operates UHF band with circular polarization, making it the first UHF nondeployed antenna for CubeSats. For both projects, problems such as isolation, impedance bandwidth, axial ratio bandwidth, and EMI shielding have been analyzed and resolved. This thesis work yields a prototype-ready design for the first project, and a final prototype and measurements for the second project.

Land-cover identification and mapping are an integral part of natural resource planning and management. Satellite imagery provides a way to obtain land cover information, particularly for large tracts of land such as those administered by federal and state agencies. This study assesses the usefulness of the Brightness/Greenness Transformation of Landsat Thematic Mapper data for differentiating conifer forest types in northern Utah. Satellite data for the Logan Ranger District of the Wasatch-Cache National Forest were classified into 27 vegetation classes. Of these, nine were determined to be conifer classes and were used in subsequent analyses. Ten sites of each conifer class type were field checked and vegetation and physical site characteristics recorded. The Brightness/Greenness Transformation was able to distinguish conifer areas from other vegetation types. High-density conifer classes were classified at 94 percent accuracy. Low-density conifer classes were classified correctly 65 percent of the time. The Brightness/Greenness Transformation alone met with limited success in distinguish ing between conifer species. Each class showed great variability with respect to major overstory species. Analysis of variance indicated that none of the site factors measured consistently corresponded with the spectrally designated classes. While several factors differed significantly among classes, no factor was significantly different for all c l ass-pair combinations. Correlation analysis revealed that brightness, greenness, and wetness values related more to environmental values than to conifer species. Brightness was highly correlated with percent of exposed soil on the site. Greenness was highly correlated to the presence of deciduous and herbaceous vegetation. Wetness was highly correlated to total tree and conifer cover values. Adding slope and aspect data to the Brightness/Greenness Transformation classes with the highest percentages of canopy cover did allow separation of lodgepole pine and Douglas fir. High percentagecanopy cover sites on slopes less than 35 percent were classified as lodgepole pine with 89 percent accuracy. On slopes greater than or equal to 35 percent, Douglas fir was found with 79 percent accuracy.

Some highway agencies in the United States are experiencing frequent distresses in asphalt pavements on bridge approaches/departures. Commonly observed distresses include alligator cracking and rutting, which reduce roadway smoothness and safety. To lessen the distresses in pavements it is needed to investigate the extent and root causes of the problem. Based on Florida highway conditions, this research study mainly focused on1. Literature review and identification of the extent of the problem; 2. Collection of relevant pavement condition data and descriptive analysis; 3. Development of statistical models to determine factors influencing the distresses in asphalt pavements on bridge approaches/departures. To the best of my knowledge, this is the first study that uses a statistical model to determine the factors that are responsible for causing asphalt pavement distresses on bridge approaches/departures. As part of the literature review, a nationwide questionnaire survey was targeted towards U.S state DOTs. The data collection and analysis specific to the Florida highways found that in 2015 on Florida Interstate highways, about 27% bridges with asphalt pavements on their approaches/departures showed signs of cracking, and about 20% bridges have noticeable rutting in their approach or departure pavements. A random parameter linear regression model was applied to examine the factors that may influence distresses in asphalt pavements in Florida. Pavement condition was evaluated based on the Florida Department of Transportation (FDOT) 2015 pavement condition data and video log images, and other relevant data were collected from various sources such as FDOT Roadway Characteristics Inventory (RCI) database, FDOT pavement management reports, and FDOT Ground Penetrating Radar (GPR) survey reports. A constraint existed in the availability of the GPR data that can give pavement layer thickness, which limited the number of bridge approach pavement sections included in the statistical modeling. Based on the limited data, the estimated results from the random parameter linear regression model showed that the variables influencing distresses in asphalt pavements on bridge approaches/departures, in terms of rutting and roughness, may include pavement age, annual average daily truck traffic, and surface friction course.