TMPA-2017: Keynote speakers

Responsiveness -the requirement that every request to a system be eventually handled- is one of the fundamental liveness properties of a reactive system and lies at the heart of all methods for specifying and verifying liveness. Average response time is a quantitative measure for the responsiveness requirement used commonly in performance evaluation. The static computation of average response time has proved remarkably elusive even for finite-state models of reactive systems. We present, for the first time, a robust formalism that allows the specification and computation of quantitative temporal properties including average response time. The formalism is based on nested weighted automata, which can serve as monitors for measuring the response time of a reactive system. We show that the average response time can be computed in exponential space for nondeterministic finite-state models of reactive systems and in polynomial time for probabilistic finite-state models. This work is joint with Krishnendu Chatterjee and Jan Otop.

The Low-Level Virtual Machine (LLVM) compiler provides a modern, industrial-strength SSA-based intermediate representation (IR) along with infrastructure support for many source languages and target platforms. Much of the LLVM compiler is structured as IR to IR translation passes that apply various optimizations and analyses.

In this talk, I will describe the Vellvm project, which seeks to provide a formal framework for developing machine-checkable proofs about LLVM IR programs and translation passes. I'll discuss some of the subtleties of modeling the LLVM IR semantics. I'll also describe some of the proof techniques that we have used for reasoning about LLVM IR transformations and sketch some example applications including verified memory-safety instrumentation and program optimizations.

Vellvm is implemented in the Coq theorem prover and provides facilities for extracting LLVM IR transformation passes and plugging them into the LLVM compiler, thus enabling us to create verified optimization passes for LLVM and evaluate them against their unverified counterparts.

This is joint work with many collaborators at Penn, and Vellvm is part of the NSF Expeditions project: The Science of Deep Specications.

Engineers frequently neglect to carefully consider the impact of their changes to a software system. As a result, the software system’s architecture eventually deviates from the original designers’ intent and degrades through unplanned introduction of new and/or invalidation of existing design decisions. Architectural decay increases the cost of making subsequent modifications and decreases a system’s dependability, until engineers are no longer able to effectively evolve the system. In this talk I will focus on pinpointing the locations in a software system’s architecture that reflect architectural decay, the points in time when that decay tends to occur, and the reasons why that decay occurs. I will present an emerging catalogue of commonly occurring symptoms of decay — architectural “smells”. I will conclude by identifying a number of simple steps that engineers can undertake to stem software system decay.