Defining the undefinedness of C11 : practical semantics-based program analysis

2017 ◽  
Author(s):  
◽  
Chris Hathhorn
Keyword(s):  
Program Analysis ◽  
Third Party ◽  
Test Suite ◽  
University Of Missouri ◽  
C Language ◽  
C Programs ◽  
Semantic Treatment ◽  
Practical Analysis ◽  
Core Language ◽  
The University

[ACCESS RESTRICTED TO THE UNIVERSITY OF MISSOURI AT AUTHOR'S REQUEST.] This thesis extends the work of Ellison and Ros,u [13, 12] but focuses on the "negative" semantics of the C11 language--the semantics required to not just give meaning to correct programs, but also to reject undefined programs. We investigate undefined behavior in C and discuss the techniques and special considerations needed to formally specify it. Using these techniques, we have modified and extended a semantics of C into one that captures undefined behavior. The amount of semantic infrastructure and effort required to achieve this was unexpectedly high, in the end more than tripling the size of the original semantics. From our semantics, we automatically extract kcc, a tool for checking realworld C programs for undefined behavior and other common programmer mistakes. Previous versions of this tool were used primarily for testing the correctness of the semantics, but we have improved it into a tool for doing practical analysis of real C programs. It beats many similar tools in its ability to catch a broad range of undesirable behaviors. We demonstrate this with comparisons based on our own test suite in addition to third-party benchmarks. Our checker is capable of detecting examples of all 77 categories of core language undefinedness appearing in the C11 standard, more than any other tool we considered. Based on this evaluation, we argue that our work is the most comprehensive and complete semantic treatment of undefined behavior in C, and thus of the C language itself.

scholarly journals Program refactoring in the presence of preprocessor directives

2005 ◽  
Author(s):  
◽  
Alejandra Garrido
Keyword(s):  
Program Analysis ◽  
Single Unit ◽  
Source Code ◽  
C Language ◽  
C Programs ◽  
Novel Approach ◽  
C Preprocessor ◽  
Single Configuration

The C preprocessor is heavily used in C programs because it provides useful and even necessary additions to the C language. Since preprocessor directives are not part of C, they are removed before parsing and program analysis take place, during the phase called preprocessing. In the context of refactoring, it is inappropriate to remove preprocessor directives: if changes are applied on the preprocessed version of a program, it may not be possible to recover the un-preprocessed version. This means that after refactoring, all the source code would be contained in a single unit, targeted to a single configuration and without preprocessor macros. This thesis describes a novel approach to preserve preprocessor directives during parsing and program analysis, and integrate them in the program representations. Furthermore, it illustrates how the program representations are used during refactor ing and how transformations preserve preprocessor directives. Additionally, the semantics of the C preprocessor are formally specified, and the results of implementing this approach in a refactoring tool for C, CRefactory, are presented.

Information, incentives, markets and policy

2016 ◽  
Author(s):  
◽  
Fan Yang
Keyword(s):  
Intellectual Property ◽  
Third Party ◽  
Computer Gaming ◽  
University Of Missouri ◽  
Healthy Behaviors ◽  
Potential Employer ◽  
Strategic Bombing ◽  
Pooling Equilibrium ◽  
Competitive Labor Market ◽  
The University

[ACCESS RESTRICTED TO THE UNIVERSITY OF MISSOURI AT AUTHOR'S REQUEST.] Chapter One: How low might be the resource costliness of making signals credible? Using a job market as an example, I build a signaling model to determine the extent to which a transfer from an applicant might replace a resource cost as an equilibrium method of achieving signal credibility. As long as a firm's claim to be hiring for an open position is credible, and profitability of the hiring process per se is limited to an application fee, the firm has an incentive to use the properly calibrated fee to implement a separating equilibrium. Applicant risk aversion does not necessarily discourage a monopsonist potential employer from using an application fee, but a firm hiring in a competitive labor market with risk-averse applicants may prefer a pooling equilibrium, hiring all applicants at their average productivity. Partial extension to a model with third-party assistance (a headhunter or a job board) is possible. Chapter Two: How costly is it to keep civilians from danger in a war? Issues previously unrelated are exposed by a new model. A government in a possibly protracted war provides health insurance to conscripts and civilians, possibly different plans. Incentives to engage in healthy behaviors before knowing whether one will be conscripted, as a conscript, and as an unconscripted civilian, are analyzed in relation to aspects of the government's conduct of the war. Surprisingly, killing random civilians can be welfareimproving relative to policies that limit likely lethal actions to cases when civilians face no danger. This may demonstrate reasonable arguments against strategic bombing, which rather than forcing an enemy out of a war, may lead to them battling longer. Chapter Three: Software producers, and possibly a broader range of firms possessing intellectual property, may have an option to rely on a community of volunteers to produce products and variants of products that utilizing the firm's intellectual property, rather than pay employees to do so. A model focusing on the computer gaming industry illustrates this new range of distribution options. In the base model, a company with a developed "game 1" may [a] sell game 1 and allow mods (i.e., a community of volunteer gamers/programmers will develop game 2 based on game 1), [b] develop game 2 itself and sell 2 separately, or [c] develop game 2 itself and sell it as a DLC to game 1 (a special case of mixed bundling). Conditions for each to be the preferred option are explored. An extension to endogenize level of modularity, by considering both a game 2 and a game 3 as mods, is considered.

TEM study of boron additions to cobalt aluminide

1988 ◽  
Vol 46 ◽  
pp. 546-547
Author(s):  
Gerald B. Feldewerth
Keyword(s):  
High Temperature ◽  
Turbine Engines ◽  
Major Drawback ◽  
University Of Missouri ◽  
Specific Strength ◽  
Aerospace Applications ◽  
Wide Range ◽  
Ordered Alloys ◽  
The University ◽  
Very High

In recent years an increasing emphasis has been placed on the study of high temperature intermetallic compounds for possible aerospace applications. One group of interest is the B2 aiuminides. This group of intermetaliics has a very high melting temperature, good high temperature, and excellent specific strength. These qualities make it a candidate for applications such as turbine engines. The B2 aiuminides exist over a wide range of compositions and also have a large solubility for third element substitutional additions, which may allow alloying additions to overcome their major drawback, their brittle nature.One B2 aluminide currently being studied is cobalt aluminide. Optical microscopy of CoAl alloys produced at the University of Missouri-Rolla showed a dramatic decrease in the grain size which affects the yield strength and flow stress of long range ordered alloys, and a change in the grain shape with the addition of 0.5 % boron.

MARS — Its Tenth Anniversary of Operation and its Future

1980 ◽  
Vol 19 (03) ◽  
pp. 125-132
Author(s):  
G. S. Lodwick ◽  
C. R. Wickizer ◽  
E. Dickhaus
Keyword(s):  
Conceptual Development ◽  
Administrative Support ◽  
Final Section ◽  
Economic Benefits ◽  
Hospital Environment ◽  
Computer Scientist ◽  
University Of Missouri ◽  
Complete Bibliography ◽  
The University ◽  
Economic Considerations

The Missouri Automated Radiology System recently passed its tenth year of clinical operation at the University of Missouri. This article presents the views of a radiologist who has been instrumental in the conceptual development and administrative support of MARS for most of this period, an economist who evaluated MARS from 1972 to 1974 as part of her doctoral dissertation, and a computer scientist who has worked for two years in the development of a Standard MUMPS version of MARS. The first section provides a historical perspective. The second deals with economic considerations of the present MARS system, and suggests those improvements which offer the greatest economic benefits. The final section discusses the new approaches employed in the latest version of MARS, as well as areas for further application in the overall radiology and hospital environment. A complete bibliography on MARS is provided for further reading.

scholarly journals Shape Neutral Analysis of Graph-based Data-structures

2018 ◽  
Vol 18 (3-4) ◽  
pp. 470-483 ◽  
Author(s):  
GREGORY J. DUCK ◽  
JOXAN JAFFAR ◽  
ROLAND H. C. YAP
Keyword(s):  
Data Structure ◽  
Data Structures ◽  
Program Analysis ◽  
Constraint Handling ◽  
C Programs ◽  
Wide Range ◽  
Target Program ◽  
Target Data ◽  
Structure Graph ◽  
Structure Properties

AbstractMalformed data-structures can lead to runtime errors such as arbitrary memory access or corruption. Despite this, reasoning over data-structure properties for low-level heap manipulating programs remains challenging. In this paper we present a constraint-based program analysis that checks data-structure integrity, w.r.t. given target data-structure properties, as the heap is manipulated by the program. Our approach is to automatically generate a solver for properties using the type definitions from the target program. The generated solver is implemented using a Constraint Handling Rules (CHR) extension of built-in heap, integer and equality solvers. A key property of our program analysis is that the target data-structure properties are shape neutral, i.e., the analysis does not check for properties relating to a given data-structure graph shape, such as doubly-linked-lists versus trees. Nevertheless, the analysis can detect errors in a wide range of data-structure manipulating programs, including those that use lists, trees, DAGs, graphs, etc. We present an implementation that uses the Satisfiability Modulo Constraint Handling Rules (SMCHR) system. Experimental results show that our approach works well for real-world C programs.

An Interactive Morphological Matrix Computational Design Tool: A Hybrid of Two Methods

2007 ◽  
Author(s):  
Cari R. Bryant ◽  
Matt Bohm ◽  
Robert B. Stone ◽  
Daniel A. McAdams
Keyword(s):  
Computational Design ◽  
Design Tool ◽  
Design Tools ◽  
Concept Generation ◽  
University Of Missouri ◽  
Generation Algorithm ◽  
Design Theories ◽  
The University ◽  
Matrix Generator

This paper builds on previous concept generation techniques explored at the University of Missouri - Rolla and presents an interactive concept generation tool aimed specifically at the early concept generation phase of the design process. Research into automated concept generation design theories led to the creation of two distinct design tools: an automated morphological search that presents a designer with a static matrix of solutions that solve the desired input functionality and a computational concept generation algorithm that presents a designer with a static list of compatible component chains that solve the desired input functionality. The merger of both the automated morphological matrix and concept generation algorithm yields an interactive concept generator that allows the user to select specific solution components while receiving instantaneous feedback on component compatibility. The research presented evaluates the conceptual results from the hybrid morphological matrix approach and compares interactively constructed solutions to those returned by the non-interactive automated morphological matrix generator using a dog food sample packet counter as a case study.

Beyond the border war : student civil rights activism at the University of Kansas and the University of Missouri, 1946-1954

2020 ◽  
Author(s):  
◽  
Mary Beth Brown
Keyword(s):  
World War Ii ◽  
Civil Rights ◽  
Race Relations ◽  
Student Activism ◽  
University Of Kansas ◽  
University Of Missouri ◽  
Effect Change ◽  
Student Activists ◽  
The University ◽  
The 19Th Century

[ACCESS RESTRICTED TO THE UNIVERSITY OF MISSOURI-COLUMBIA AT REQUEST OF AUTHOR.] This dissertation examines post-World War II student civil rights activism at two Midwestern college campuses, the University of Missouri (MU) and the University of Kansas (KU). Missouri and Kansas have conflicting histories concerning race dating back to Bleeding Kansas and the history of race relations on the campuses of KU and MU. This history is especially complicated during the period between 1946 and 1954 because of heightened student activism that challenged racial injustices. Race relations on campus largely mirrored that of the state's political environment, with KU having integrated in the 19th century, whereas MU did not desegregate until 1950. However, the same did not apply to the success of student activists at each school where MU students found success fighting against discriminatory practices in Columbia, whereas local business leaders and the university administration stymied KU students. The dissertation examines the exchange of ideas and strategy among students, which occurred through athletics, debates, guest speakers, and various regional and national groups. In particular, the study argues that campus spaces, such as residential co-ops and student organizations, were deeply significant because they served as incubators of activism by offering students a place to talk about racial and social injustice and plan ways to challenge these inequalities and effect change on campus and in the broader community.

Sharp things, or the silver lines are not scars

2019 ◽  
Author(s):  
◽  
Teresa Milbrodt
Keyword(s):  
Financial Stability ◽  
Romantic Relationship ◽  
Insurance Coverage ◽  
Health Insurance Coverage ◽  
Stained Glass ◽  
University Of Missouri ◽  
Adjunct Instructor ◽  
Constant Change ◽  
Part Time ◽  
The University

[ACCESS RESTRICTED TO THE UNIVERSITY OF MISSOURI AT REQUEST OF AUTHOR.] This novel is the story of Tianne, a twenty-eight-year-old stained glass artist. She works two part-time jobs as a clerk at a stained glass supply store, and as an adjunct instructor at a community college. Her boyfriend Jeremiah is an academic adviser at the same college, but wants a career performing in comedy clubs. He uses a wheelchair due to spina bifida, and is cheerfully blunt that he could die from an undetected kidney infection. Tianne wrangles her own invisible disability, since endometriosis causes her to have awful cramps during her period that can keep her home from work. Tianne loves her jobs but worries about bills after her car breaks down. She envies Jeremiah's financial stability until he's fired for speaking his mind too many times to administration. Tianne fears for his health insurance coverage, while Jeremiah debates careers as a high school guidance counselor or touring comedy clubs. Throughout the book Tianne tries to chart a path though the instabilities of her body, Jeremiah's body, their career paths, and their romantic relationship, knowing that nothing is permanent. Hers is a story not of looking for stability, but coming to terms with instability, and finding spaces of adaptation to constant change.

Frobenius closure and prime characteristic singularities

2020 ◽  
Author(s):  
◽  
Kyle Logan Maddox
Keyword(s):  
Local Ring ◽  
Local Cohomology ◽  
Sufficient Condition ◽  
Zariski Topology ◽  
Prime Characteristic ◽  
Joint Work ◽  
University Of Missouri ◽  
Mild Conditions ◽  
Flat Maps ◽  
The University

[ACCESS RESTRICTED TO THE UNIVERSITY OF MISSOURI AT REQUEST OF AUTHOR.] This dissertation outlines several results about prime characteristic singularities for which the nilpotent part under the induced Frobenius action on local cohomology is either finite colength or the entire module, collectively referred to here as nilpotent singularities. First, we establish a sufficient condition for the finiteness of the Frobenius test exponent for a local ring and apply it to conclude that nilpotent singularities have finite Frobenius test exponent. In joint work with Jennifer Kenkel, Thomas Polstra, and Austyn Simpson, we show that under mild conditions nilpotent singularities descend and ascend along faithfully flat maps. Consequently, we then prove that the loci of primes which are weakly F-nilpotent and F-nilpotent are open in the Zariski topology for rings which are either F-finite or essentially of fiiite type over an excellent local ring.

Sign in / Sign up

Export Citation Format

Share Document