LLVM [Lattner and Adve, 2004] is designed for the compile-time, link-time and run-time optimization of programs written in various programming languages. The language supported by LLVM targeted by modern compilers is LLVM IR [llvm.org, 2018]. In this paper we define K-LLVM, a reference semantics for LLVM IR. To the best of our knowledge, K-LLVM is the most complete formal LLVM IR semantics to date, including all LLVM IR instructions, intrinsic functions in the LLVM documentation and Standard-C library functions that are necessary to execute many LLVM IR programs. Additionally, K-LLVM formulates an abstract machine that executes all LLVM IR instructions. The machine allows to describe our formal semantics in terms of simulating a conceptual virtual machine that runs LLVM IR programs, including non-deterministic programs. Even though the K-LLVM memory model in this paper is assumed to be a sequentially consistent memory model and does not include all LLVM concurrency memory behaviors, the design of K-LLVM’s data layout allows the K-LLVM abstract machine to execute some LLVM IR programs that previous semantics did not cover, such as the full range of LLVM IR behaviors for the interaction among LLVM IR casting, pointer arithmetic, memory operations and some memory flags (e.g. readonly) of function headers. Additionally, the memory model is modularized in a manner that supports investigating other memory models. To validate K-LLVM, we have implemented it in 𝕂 [Roşu, 2016], which generated an interpreter for LLVM IR. Using this, we ran tests including 1,385 unit test programs and around 3,000 concrete LLVM IR programs, and K-LLVM passed all of them.

The Java Virtual Machine (JVM) postpones running class initialization methods until their classes are first referenced, such as by a new or static instruction. This process is called dynamic class initialization. Jinja is a semantic framework for Java and JVM developed in the theorem prover Isabelle that includes several semantics: Java-level big-step and small-step semantics, JVM-level small-step semantics, and an intermediate compilation step, J1, between these two levels. In this paper, we extend Jinja to include support for static instructions and dynamic class initialization. We also extend and re-prove related proofs, including Java-level type safety, equivalence between Java-level big-step and small-step semantics, and the correctness of a compilation from the Java level to the JVM level through J1. This work is based on the Java SE 8 specification.

While most efforts to improve students' learning in computer science education have focused on designing new pedagogies or tools, comparatively little research has focused on redesigning examinations to improve students' learning. Cognitive science research, however, has robustly demonstrated that getting students to practice using their knowledge in testing environments can significantly improve learning through a phenomenon known as the testing effect. The testing effect has been shown to improve learning more than rehearsal strategies such as re-reading a textbook or re-watching lectures. In this paper, we present a quasi-experimental study to examine the effect of using frequent, automated examinations in an advanced computer science course, "Programming Languages and Compilers" (CS 421). In Fall 2014, students were given traditional paper-based exams, but in Fall 2015 a computer-based testing facility enabled the course to offer more frequent examinations while other aspects of the course were held constant. A comparison of 292 student scores across the two semesters revealed a significant change in the distribution of students' grades with fewer students failing the final examination, and proportionately more students now earning grades of B and C instead. This data suggests that focusing on redesigning the nature of examinations may indeed be a relatively untapped opportunity to improve students' learning.

We characterize the data type of terms with bindings, freshness and substitution, as an initial model in a suitable Horn theory. This characterization yields a convenient recursive definition principle, which we have formalized in Isabelle/HOL and employed in a series of case studies taken from the λ-calculus literature.

Aberrant behavior of human operators in safety critical systems can lead to severe or even fatal consequences. Human operators are unique in their decision making capability, judgment and nondeterminism. There is a need for a generalized framework that can allow capturing, modeling and analyzing the interactions between computer systems and human operators where the operators are allowed to deviate from their prescribed behaviors for executing a task. This will provide a formal understanding of the robustness of a computer system against possible aberrant behaviors by its human operators. We provide a framework for (i) modeling the human operators and the computer systems; (ii) formulating tolerable human operator action variations(protection envelope); (iii) determining whether the computer system can maintain its guarantees if the human operators operate within their protection envelopes; and finally, (iv) determining robustness of the computer system under weakening of the protection envelopes. We present Tutela, a tool that assists in accomplishing the first and second step, automates the third step and modestly assists in accomplishing the fourth step.

Breakdowns in complex systems often occur as a result of system elements interacting in ways unanticipated by analysts or designers. The use of task behavior as part of a larger, formal system model is potentially useful for analyzing such problems because it allows the ramifications of different human behaviors to be verified in relation to other aspects of the system. A component of task behavior largely overlooked to date is the role of human-human interaction, particularly human-human communication in complex human-computer systems. We are developing a multi-method approach based on extending the Enhanced Operator Function Model language to address human agent communications (EOFMC). This approach includes analyses via theorem proving and future support for model checking linked through the EOFMC top level XML description. Herein, we consider an aviation scenario in which an air traffic controller needs a flight crew to change the heading for spacing. Although this example, at first glance, seems to be one simple task, on closer inspection we find that it involves local human-human communication, remote human-human communication, multi-party communications, communication protocols, and human-automation interaction. We show how all these varied communications can be handled within the context of EOFMC.

Safety critical systems can suffer severe and even fatal consequences due to aberrant behavior of human operators. Human operators are unique in their decision making capability, judgment and nondeterminism. There is a need for analyzing the interactions among computer systems and human operators where the operators are allowed to deviate from their prescribed behaviors for executing a task. In this paper we wish to examine the ability of a system to remain safe under broad classes of variations of the prescribed human task. To facilitate this concept we consider the concept of a protection envelope giving a wider class of behaviors than strictly prescribed by the human task while providing guarantees of restrictions on human operator to the system. We develop methods for addressing two issues. The first issue is: given a human task specification and a protection envelope, will the protection envelope properties still hold under standard variations as described by Hollnagel [10]. The second issue is: in the absence of a protection envelope, can we approximate a protection envelope that will at least have the property of being robust against the aforementioned variations. We present methodology and tool for assisting in this regard.

We present a point of view concerning HOAS(Higher-Order Abstract Syntax) and an extensive exercise in HOAS along this point of view. The point of view is that HOAS can be soundly and fruitfully regarded as a definitional extension on top of FOAS (First-Order Abstract Syntax). As such, HOAS is not only an encoding technique, but also a higher-order view of a first-order reality. A rich collection of concepts and proof principles is developed inside the standard mathematical universe to give technical life to this point of view. The exercise consists of a new proof of Strong Normalization for System F. The concepts and results presented here have been formalized in the theorem prover Isabelle/HOL.

Cyber-physical systems are networked, component-based, real-time systems that control and monitor the physical world. We need software architectures that limit fault-propagation across unreliable components. This paper introduces our simplex reference model which is distinguished by: a plant being controlled in an external context, a machine performing the control, a domain model that estimates the plant state, and the safety requirements that must be met. The simplex reference model assists with constructing CPS architectures which limit fault-propagation. We present a representative case study to highlight the ideas behind the model and our particular decomposition.

Advances in networking, sensors, and embedded devices have made it feasible to monitor and provide medical and other assistance to people in their homes. Aging populations will benefit from reduced costs and improved healthcare through assisted living based on these technologies. However, these systems challenge current state-of-the-art techniques for usability, reliability, and security. This is a particular challenge for open and extensible systems that combine software and hardware from many vendors and provide information to diverse clinicians. In this paper we present the I-Living architecture for assisted living that allows independent parties work together in a dependable, secure, and low-cost fashion with predictable properties. Our approach is based on an Assisted Living Service Provider (ALSP) who provides a server that collects and maintains encrypted assisted persons (APs)' records. Our ALSP can be a third party distinct from APs, communication providers, and clinicians; or it can be part of an ISP, hospital or similar enterprise. We have explored the architecture by developing a collection of applications and implementing them in a prototype system. Our system shows the feasibility and opportunity of an open approach to assisted living systems.

Abstract We present a symbolic model checking approach that allows verifying a unit of code, e.g., a single procedure or a collection of procedures that interact with each other. We allow temporal specifications that assert over both theprogram countersand theprogram variables. We decompose the verification into two parts: (1) a search that is based on the temporal behavior of theprogram counters, and (2) the formulation and refutation of a path condition, which inherits conditions constraining theprogram variablesfrom the temporal specification. This verification approach is modular, as we do not require that all the involved procedures are provided. Furthermore, we do not request that the code is based on a finite domain. The presented approach can also be used for automating the generation of test cases for unit testing.

High-level specification of patterns of communications such as protocols can be modeled elegantly by means of session types (Honda et al ., 1998). However, a number of examples suggest that session types fall short when finer precision on protocol specification is required. In order to increase the expressiveness of session types we appeal to the theory of correspondence assertions (Clarke & Marrero, 1998; Gordon & Jeffrey, 2003b). The resulting type discipline augments the types of long-term channels with effects and thus yields types which may depend on messages read or written earlier within the same session. This new type system can be used to check: source of information, whether data is propagated as specified across multiple parties, if there are unspecified communications between parties, and if the data being exchanged has been modified by the code in an unspecified way. We prove that evaluation preserves typability and that well-typed processes are safe. Also, we illustrate how the resulting theory allows us to address shortcomings present in the pure theory of session types.

In an earlier project of VanInwegen and Gunter, the dynamic semantics of the Core of Standard ML (SML) was encoded in the HOL theorem-prover. We extend this by adding the dynamic Module system. We then develop a possible dynamic semantics for a Module system with higher-order functors and encode this as well. Next we relate these two semantics via embeddings and projections and discuss how we use these to prove that evaluation in the proposed system is a conservative extension, in an appropriate sense, of evaluation in the SML Module system.