Invited Talk

Manuel HermenegildoInvited Speaker

IMDEA Software Institute and T.U. of Madrid

Spain

Manuel Hermenegildo is Distinguished Professor at (and was the Founding Director of) the IMDEA Software Institute. He is also full Prof. of Computer Science at the Tech. U. of Madrid, UPM. Previously he held an Endowed Chair in Information Science and Technology at the U. of New Mexico. He was also project leader at the MCC research center and Adjunct Associate Prof. at the CS Department of the U. of Texas, both in Austin, Texas. See his home page for more information.

Research interests: Energy-Aware Computing, Resource / non-functional property analysis, verification, and control; Global Program Analysis, Optimization, Verification, Debugging; Abstract Interpretation; Partial Evaluation; Parallelism and Parallelizing Compilers; Constraint/Logic/Functional Programming Theory and Implementation, Abstract Machines; Automatic Documentation Tools, Execution Visualization; Sequential and Parallel Computer Architecture.

Artifact

We present a specification language aiming at soundly modeling unavailable functions in a static analyzer for C by abstract interpretation. It takes inspiration from Behavioral Interface Specification Languages popular in deductive verification, notably Frama-C’s ACSL, as we annotate function prototypes with pre and post-conditions expressed concisely in a first-order logic, but with key differences. Firstly, the specification aims at replacing a function implementation in a safety analysis, not verifying its functional correctness. Secondly, we do not rely on theorem provers; instead, specifications are interpreted at function calls by our abstract interpreter. We implemented the language into Mopsa, a static analyzer designed to easily reuse abstract domains across widely different languages (such as C and Python). We show how its design helped us support a logic-based language with minimal effort. Notably, it was sufficient to add only a handful transfer functions (including very selective support for quantifiers) to achieve a sound and precise analysis. We modeled a large part of the GNU C library and C execution environment in our language, including the manipulation of unbounded strings, file descriptors, and programs with an unbounded number of symbolic command-line parameters, which allows verifying programs in a realistic setting. We report on the analysis of C programs from the Juliet benchmarks and Coreutils.

Abdelraouf Ouadjaout

Sorbonne Université

France

Antoine Miné

Sorbonne Université

France

Invited Talk

Ezgi ÇiçekInvited Speaker

Facebook London

United Kingdom

I have obtained my PhD in Programming Languages at MPI-SWS (Max Planck Institute for Software Systems, Saarbrücken, Germany) and Saarland University in January 2018. I was advised by Deepak Garg. I am currently a Software Engineer at Facebook’s Static Analysis team, Infer. Nowadays, I am working on a static analysis tool for detecting performance regressions at diff time.

Keynote

The next generation of our connected world calls for a low-latency, low-bandwidth, low-development-effort platform for synchronized interactions. The platform must also enforce privacy from the ground up, in particular in anticipation of an always-on Augmented Reality future.

In traditional synchronization approaches, computations are performed on a server and results are continuously distributed to clients. Croquet moves all computation to the clients. A lightweight “reflector” server directs the clients to advance time in sync, and ensures that any external event is incorporated by all clients at exactly the same point in the computation, leading to synchronized, bit-identical state. All data is end-to-end encrypted by the clients; the server stores and distributes data, but can never peek inside.

Croquet’s programming model separates the synchronized computation of “models” from individually computed “views”. This means the world is the same for everyone, but the display of the world can be tailored to each device and user. Models and views communicate using a publish/subscribe mechanism that routes certain events via the reflector. This model/view separation and pub/sub communication is a major departure from the previous, proxy-based Smalltalk implementation of Croquet. It retains the ability for live programming by atomically incorporating new code.

Vanessa is the chief architect of the current JavaScript-based implementation. She will give an overview of the system, highlight challenges in designing the API, and explore the far-reaching implications of the shift from server to client.

Vanessa Freudenberg

Croquet Corp

United States

Vanessa is a co-founder of Croquet Corp and the principal engineer of the current Teatime client/server architecture underlying Croquet. She has been developing interactive systems for more than 20 years with a focus on live, self-supporting systems (including Squeak Etoys, Scratch, Lively, Smalltalk VMs).

Blockchains support execution of smart contracts: programs encoding complex transactions between distrusting parties. Due to their distributed nature, blockchains rely on third-party miners to execute and validate transactions. Miners are compensated by charging users with gas based on the execution cost of the transaction. To compute the exact gas cost, blockchains track gas cost dynamically creating its own overhead. This paper presents a static exact gas-cost analysis technique that can be employed to eliminate dynamic gas tracking. This approach presents further benefits such as providing miners with a trusted gas bound that can be verified in linear time, and eliminating out-of-gas exceptions. To handle recursion and unbounded computation, we propose a novel amortization technique that stores gas inside data structures. We have implemented our analysis technique in a tool called GasBoX that takes a contract as input and infers the gas cost of its functions automatically. We have evaluated GasBoX on 13 standard smart contracts borrowed from real-world blockchain projects. Our soundness theorem proves that the gas bound inferred by GasBoX exactly matches the gas cost at runtime and no dynamic gas tracking is necessary.

Ankush Das

Carnegie Mellon University

United States

Shaz Qadeer

Novi, USA

United States

Python 3 is a highly dynamic language, but it has introduced a syntax
for expressing types with PEP484. This paper explores how
developers use these type annotations, the type system semantics
provided by type checking and inference tools, and the performance
of these tools. We evaluate the types and tools on a corpus of public
GitHub repositories. We review MyPy and PyType, two canonical static
type checking and inference tools, and their distinct
approaches to type analysis. We then address
three research questions:
(i) How often and in what ways do developers use Python 3 types?
(ii) Which type errors do developers make?
(iii) How do type errors from different tools compare?

Surprisingly, when developers use static types, the code rarely
type-checks with either of the tools. MyPy and PyType exhibit false
positives, due to their static nature, but also flag many useful
errors in our corpus. Lastly, MyPy and PyType embody two distinct type
systems, flagging different errors in many cases.
Understanding the usage of Python types can help guide tool-builders
and researchers. Understanding the performance of popular tools can
help increase the adoption of static types and tools by practitioners,
ultimately leading to more correct and more robust Python code.

Link to Publication: http://design.cs.iastate.edu/splash20/dls20/dls20main-p10-p.pdf

Ingkarat Rak-amnouykit

Rensselaer Polytechnic Institute

Daniel McCrevan

Rensselaer Polytechnic Institute

Ana Milanova

Rensselaer Polytechnic Institute

Martin Hirzel

IBM Research

United States

Julian Dolby

IBM Research, USA

WebAssembly is designed to be an alternative to JavaScript that is a safe, portable, and efficient compilation target for a variety of languages. The performance of high-level languages depends not only on the underlying performance of WebAssembly, but also on the quality of the generated WebAssembly code. In this paper, we identify several features of high-level languages that current approaches can only compile to WebAssembly by generating complex and inefficient code. We argue that these problems could be addressed if WebAssembly natively supported first-class continuations. We then present Wasm/k, which extends WebAssembly with delimited continuations. Wasm/k introduces no new value types, and thus does not require significant changes to the WebAssembly type system (validation). Wasm/k is safe, even in the presence of foreign function calls (e.g., to and from JavaScript). Finally, Wasm/k is amenable to efficient implementation: we implement Wasm/k as a local change to Wasmtime, an existing WebAssembly JIT. We evaluate Wasm/k by implementing C/k, which adds delimited continuations to C/C++. C/k uses Emscripten and its implementation serves as a case study on how to use Wasm/k in a compiler that targets WebAssembly. We present several case studies using C/k, and show that on implementing green threads, it can outperform the state-of-the-art approach Asyncify with an 18% improvement in performance and a 30% improvement in code size.

Link to Publication: http://design.cs.iastate.edu/splash20/dls20/dls20main-p5-p.pdf

Donald Pinckney

Northeastern University

United States

Arjun Guha

University of Massachusetts at Amherst

Yuriy Brun

University of Massachusetts Amherst

Artifact

Practical adoption of static analysis often requires trading precision for performance. This paper focuses on improving the memory efficiency of abstract interpretation without sacrificing precision or time efficiency. Computationally, abstract interpretation reduces the problem of inferring program invariants to computing a fixpoint of a set of equations. This paper presents a method to minimize the memory footprint in Bourdoncle’s iteration strategy, a widely-used technique for fixpoint computation. Our technique is agnostic to the abstract domain used. We prove that our technique is optimal (i.e., it results in minimum memory footprint) for Bourdoncle’s iteration strategy while computing the same result. We evaluate the efficacy of our technique by implementing it in a tool called MIKOS, which extends the state-of-the-art abstract interpreter IKOS. When verifying user-provided assertions, MIKOS shows a decrease in peak-memory usage to 4.07% (24.57x) on average compared to IKOS. When performing interprocedural buffer-overflow analysis, MIKOS shows a decrease in peak-memory usage to 43.7% (2.29x) on average compared to IKOS.

Sung Kook Kim

University of California, Davis

United States

Arnaud J. Venet

Facebook

Aditya V. Thakur

University of California, Davis

United States

Pattern matching allows programs both to extract specific information from complex data types, as well as to branch on the structure of data and thus apply specialized actions to different forms of data. Originally designed for strongly typed functional languages with algebraic data types, pattern matching has since been adapted for object-oriented and even dynamic languages. This paper discusses how pattern matching can be included in the dynamically typed language \emph{Python} in line with existing features that support extracting values from sequential data structures.

Link to Publication: http://design.cs.iastate.edu/splash20/dls20/dls20main-p12-p.pdf

Tobias Kohn

University of Cambridge, UK

United Kingdom

Guido van Rossum

Python Software Foundation

Gary Brandt Bucher, II

Research Affiliates, LLC

United States

Talin

Ivan Levkivskyi

Dropbox Ireland

Artifact

Control dependency is a fundamental concept in many program analyses, transformation, parallelization, and compiler optimization techniques. An overwhelming number of definitions of control dependency relations are found in the literature that captures various kinds of program control flow structures. Weak and strong control closure (WCC and SCC) relations capture nontermination insensitive and sensitive control dependencies and subsume all previously defined control dependency relations. In this paper, we have shown that static dependency-based pro-gram slicing requires the repeated computation of WCC and SCC. The state-of-the-art WCC algorithm provided by Danicic et al. has the cubic worst-case complexity in terms of the size of the control flow graph and is a major obstacle to be used in static program slicing. We have provided a simple yet efficient method to compute the minimal WCC which has the quadratic worst-case complexity and proved the correctness of our algorithms. We implemented ours and the state-of-the-art algorithms in the Clang/LLVM compiler framework and run experiments on a number of SPEC CPU 2017 benchmarks. Our method performs a maximum of 23.8 times and on average 10.6 times faster than the state-of-the-art method. The performance curves of our WCC algorithm for practical applications are closer to the NlogN curve in the microsecond scale. Evidently, we improve the practical performance of WCC computation by an order of magnitude.

Abu Naser Masud

Malardalen University

Many researchers have explored retrofitting static type systems to dynamic languages. This raises the question of how to add type annotations to code that was previously untyped. One obvious solution is type inference. However, in complex type systems, in particular those with structural types, type inference typically produces most general types that are large, hard to understand, and unnatural for programmers. To solve this problem, we introduce InferDL, a novel Ruby type inference system that infers sound and useful type annotations by incorporating heuristics that guess types. For example, we might heuristically guess that a parameter whose name ends in ``count'' is an integer. InferDL works by first running standard type inference and then applying heuristics to any positions for which standard type inference produces overly-general types. Heuristic guesses are added as constraints to the type inference problem to ensure they are consistent with the rest of the program and other heuristic guesses; inconsistent guesses are discarded. We formalized InferDL in a core type and constraint language. We implemented InferDL on top of RDL, an existing Ruby type checker. To evaluate InferDL, we applied it to four Ruby on Rails apps that had been previously type checked with RDL, and hence had type annotations. We found that, when using heuristics, InferDL inferred 22% more types that were as or more precise than the previous annotations, compared to standard type inference without heuristics. We also found one new type error. We further evaluated InferDL by applying it to six additional apps, finding five additional type errors. Thus, we believe InferDL represents a promising approach for inferring type annotations in dynamic languages.

Link to Publication: http://design.cs.iastate.edu/splash20/dls20/dls20main-p14-p.pdf

Milod Kazerounian

University of Maryland, College Park

United States

Brianna M. Ren

University of Maryland

Jeffrey S. Foster

Tufts University

United States

Deep Neural Networks (DNNs) are rapidly being applied to safety-critical domains such as drone and airplane control, motivating techniques for verifying the safety of their behavior. Unfortunately, DNN verification is NP-hard, with current algorithms slowing exponentially with the number of nodes in the DNN. This paper introduces the notion of Abstract Neural Networks (ANNs), which can be used to soundly overapproximate DNNs while using fewer nodes. An ANN is like a DNN except weight matrices are replaced by values in a given abstract domain. We present a framework parameterized by the abstract domain and activation functions used in the DNN that can be used to construct a corresponding ANN. We present necessary and sufficient conditions on the DNN activation functions for the constructed ANN to soundly over-approximate the given DNN. Prior work on DNN abstraction was restricted to the interval domain and ReLU activation function. Our framework can be instantiated with other abstract domains such as octagons and polyhedra, as well as other activation functions such as Leaky ReLU, Sigmoid, and Hyperbolic Tangent.

Matthew Sotoudeh

University of California, Davis

Aditya V. Thakur

University of California, Davis

United States

Most virtual machines employ just-in-time (JIT) compilers to achieve
high-performance. Trace-based compilation and method-based compilation are two
major compilation strategies in JIT compilers. In general, the former excels
in compiling programs with more in-depth method calls and more dynamic
branches, while the latter is suitable for a wide range of programs. Some
previous studies have suggested that each strategy has its advantages and
disadvantages, and there is no clear winner.

In this paper, we present a new approach, namely, the meta-hybrid JIT
compilation strategy. It combines trace-based and method-based compilations to
utilize the advantages of both strategies. Moreover, it is realized as a meta
JIT compiler framework; thus, we can generate a VM with a hybrid JIT compiler
that can apply different program parts by merely writing an interpreter with
our framework.

We chose to extend a meta-tracing JIT compiler and supported the two
compilations on it. As a prototype, we implemented a simple meta-tracing JIT
compiler framework called BacCaml based on the MinCaml compiler by following
RPython’s architecture.

We evaluated its performance by creating a small functional programming
language with BacCaml and running microbenchmark programs. Furthermore, we
performed a synthetic experiment to confirm that there are programs that
run faster by hybrid compilation.

Link to Publication: http://design.cs.iastate.edu/splash20/dls20/dls20main-p4-p.pdf

Yusuke Izawa

Tokyo Institute of Technology

Japan

Hidehiko Masuhara

Tokyo Institute of Technology

Japan

Artifact

We are interested in algorithmically proving the robustness of neural networks. Notions of robustness have been discussed in the literature; we are interested in probabilistic notions of robustness that assume it feasible to construct a statistical model of the process generating the inputs of a neural network. We find this a reasonable assumption given the rapid advances in algorithms for learning generative models of data. A neural network f is then defined to be probabilistically robust if, for a randomly generated pair of inputs, f is likely to demonstrate k-Lipschitzness, i.e., the distance between the outputs computed by $f$ is upper-bounded by the k-th multiple of the distance between the pair of inputs. We name this property, probabilistic Lipschitzness.

We model generative models and neural networks, together, as programs in a simple, first-order, imperative, probabilistic programming language, pcat. Inspired by a large body of existing literature, we define a denotational semantics for this language. Then we develop a sound local Lipschitzness analysis for cat, a non-probabilistic sublanguage of pcat. This analysis can compute an upper bound of the ``Lipschitzness'' of a neural network in a bounded region of the input set. We next present a provably correct algorithm, PROLIP, that analyzes the behavior of a neural network in a user-specified box-shaped input region and computes - (i) lower bounds on the probabilistic mass of such a region with respect to the generative model, (ii) upper bounds on the Lipschitz constant of the neural network in this region, with the help of the local Lipschitzness analysis. Finally, we present a sketch of a proof-search algorithm that uses PROLIP as a primitive for finding proofs of probabilistic Lipschitzness. We implement the PROLIP algorithm and empirically evaluate the computational complexity of PROLIP.

Ravi Mangal

Georgia Institute of Technology

United States

Kartik Sarangmath

Georgia Institute of Technology

United States

Aditya Nori

Alessandro Orso

Georgia Tech

United States

Execution times may be reduced by offloading parallel loop nests to a GPU. Auto-parallelizing compilers are common for static languages, often using a cost model to determine when the GPU execution speed will outweigh the offload overheads. Nowadays scientific software is increasingly written in dynamic languages and would benefit from compute accelerators. The
ALPyNA framework analyses moderately complex Python loop nests and automatically JIT compiles code for heterogeneous CPU and GPU architectures.

We present the first analytical cost model for auto-parallelizing loop nests in a dynamic language on heterogeneous architectures. Predicting execution time in a language like Python is extremely challenging, since aspects like the element types, size of the iteration space, and amenability to parallelization can only be determined at runtime. Hence the cost model must be both staged, to combine compile and run-time information, and lightweight to minimize runtime overhead. GPU execution time prediction must account for factors like data transfer, block-structured execution, and starvation.

We show that a comparatively simple, staged analytical model can accurately determine during execution when it is profitable to offload a loop nest. We evaluate our model on three heterogeneous platforms across 360 experiments with 12 loop-intensive Python benchmark programs. The results show small misprediction intervals and a mean slowdown of just 13.6%, relative to the optimal (oracular) offload strategy.

Link to Publication: http://design.cs.iastate.edu/splash20/dls20/dls20main-p6-p.pdf

Dejice Jacob

University of Glasgow, UK

United Kingdom

Phil Trinder

University of Glasgow

Jeremy Singer

Glasgow University

United Kingdom

Invited Talk

James WorrellInvited Speaker

University of Oxford

United Kingdom

We consider the termination problem for triangular weakly non-linear loops (twn-loops) over some ring S like Z, Q, or R. Essentially, the guard of such a loop is an arbitrary Boolean formula over (possibly non-linear) polynomial inequations, and the body is a single assignment (x₁,…,x_d)⟵(c₁⋅x₁+p₁,…,c_d⋅x_d+p_d) where each x_i is a variable, c_i∈S, and each p_i is a (possibly non-linear) polynomial over S and the variables x_i+1,…,x_d. We present a reduction from the question of termination to the existential fragment of the first-order theory of S and R. For loops over R, our reduction entails decidability of termination. For loops over Z and Q, it proves semi-decidability of non-termination. Furthermore, we present a transformation to convert certain non-twn-loops into twn-form. Then the original loop terminates iff the transformed loop terminates over a specific subset of R, which can also be checked via our reduction. This transformation also allows us to prove tight complexity bounds for the termination problem for two important classes of loops which can always be transformed into twn-loops.

Florian Frohn

Max Planck Institute for Informatics

Germany

Marcel Hark

RWTH Aachen University, Germany

Jürgen Giesl

RWTH Aachen University

Germany

Python is a popular, dynamic language for data science and scientific computing.
To ensure efficiency, significant numerical libraries are implemented in static native languages.
However, performance suffers when switching between native and non-native code, especially if data has to be converted between native arrays and Python data structures.
As GPU accelerators are increasingly used, this problem becomes particularly acute.
Data and control has to be repeatedly transferred between the accelerator and the host.

In this paper, we present DelayRepay, a delayed execution framework for numeric Python programs.
It avoids excessive switching and data transfer by using lazy evaluation and kernel fusion.
Using DelayRepay, operations on NumPy arrays are executed lazily, allowing multiple calls to accelerator kernels to be fused together dynamically.
DelayRepay is available as a drop-in replacement for existing Python libraries.
This approach enables significant performance improvement over the state-of-the-art and is invisible to the application programmer.
We show that our approach provides a maximum $377\times$ speedup over NumPy - a
409% increase over the state of the art.

Link to Publication: http://design.cs.iastate.edu/splash20/dls20/dls20main-p7-p.pdf

John Magnus Morton

University of Edinburgh

Kuba Kaszyk

University of Edinburgh

Lu Li

Linköping University

Jiawen Sun

University of Edinburgh

Christophe Dubach

McGill University

United Kingdom

Michel Steuwer

The University of Edinburgh

United Kingdom

Murray Cole

University of Edinburgh, UK

Michael F. P. O'Boyle

University of Edinburgh

To efficiently execute dynamically typed languages, many language implementations have adopted a two-tier architecture. The first tier aims for low-latency startup times and collects dynamic profiles, such as the dynamic types of variables. The second tier provides high-throughput using an optimizing compiler that specializes code to the recorded type information. If the program behavior changes to the point that not previously seen types occur in specialized code, that specialized code becomes invalid, it is deoptimized, and control is transferred back to the first tier execution engine which will start specializing anew. However, if the program behavior becomes more specific, for instance, if a polymorphic variable becomes monomorphic, nothing changes. Once the program is running optimized code, there are no means to notice that an opportunity for optimization has been missed.

We propose to employ a sampling-based profiler to monitor native code without any instrumentation. The absence of instrumentation means that when the profiler is not active, no overhead is incurred. We present an implementation is in the context of the \v{R} just-in-time, optimizing compiler for the R language. Based on the sampled profiles, we are able to detect when the native code produced by \v{R} is specialized for stale type feedback and recompile it to more type-specific code. We show that sampling adds an overhead of less than 3% in most cases and up to 9% in few cases and that it reliably detects stale type feedback within milliseconds.

Link to Publication: http://design.cs.iastate.edu/splash20/dls20/dls20main-p13-p.pdf

Olivier Flückiger

Northeastern University

Andreas Wälchli

University of Bern

Sebastián Krynski

Czech Technical University, National University of Quilmes

Jan Vitek

Northeastern University / Czech Technical University

Debugging applications that execute within a framework is not always easy:
the call-stack offered to developers is often a mix-up of stack frames that belong to different frameworks, introducing an unnecessary noise that prevents developers from focusing on the debugging task.
Moreover, relevant application code is not always available in the call-stack because it may have already returned, or is available in another thread.
In such cases, manually gathering all relevant information from these different sources is not only cumbersome but also costly.

In this paper we introduce Sarto, a call-stack instrumentation layer that allows developers to tailor the stack to make debugging framework-aware.
The goal is to improve the quality and amount information present in the call-stack to reduce debugging time without impacting the execution time.
Sarto proposes a set of six stack operations that combined hide irrelevant information, introduce missing information, and relate dispersed debugging sources before this is fed to the debugger.

We validate Sarto by applying it to four application cases using inherently different frameworks: unit testing, web server, remote promises and big data processing.
We showcase our experiences in using Sarto in the different frameworks, and perform some performance benchmarks to demonstrate that Sarto does not generate noticeable overhead when instrumenting a call-stack.
We also show that our solution reduces by half the amount of data stored to debug similar exceptions happening in a parallel setup.

Link to Publication: http://design.cs.iastate.edu/splash20/dls20/dls20main-p11-p.pdf

Matteo Marra

Vrije Universiteit Brussel

Belgium

Guillermo Polito

Univ. Lille, CNRS, Centrale Lille, Inria, UMR 9189 - CRIStAL - Centre de Recherche en Informatique Signal et Automatique de Lille

Argentina

Elisa Gonzalez Boix

Vrije Universiteit Brussel, Belgium

Belgium

Artifact

We present an automated procedure for synthesizing sound inductive invariants for floating-point numerical loops. Our procedure generates invariants of the form of a convex polynomial inequality that tightly bounds the values of loop variables. Such invariants are a prerequisite for reasoning about the safety and roundoff errors of floating-point programs.

Unlike previous approaches that rely on policy iteration, linear algebra or semi-definite programming, we propose a heuristic procedure based on simulation and counterexample-guided refinement. We observe that this combination is remarkably effective and general and can handle both linear and nonlinear loop bodies, nondeterministic values as well as conditional statements. Our evaluation shows that our approach can efficiently synthesize loop invariants for existing benchmarks from literature, but that it is also able to find invariants for nonlinear loops that today’s tools cannot handle.

Anastasiia Izycheva

Technical University of Munich

Germany

Eva Darulova

MPI-SWS

Helmut Seidl

Technische Universität München

Invited Talk

In this talk, I will present the static analysis component of the open source Arcs Project, which is an ecosystem for building privacy-preserving AI applications . Specifically, I will talk about how we use static analysis to ensure that data is only used in approved ways in an AI application. First, I will introduce the Arcs programming model, the type system, and a policy specification language. Then, I will talk about how we use abstract interpretation and the guarantees provided by the type system to ensure that the application only uses data as outlined by the data-usage policy.

Gogul BalakrishnanInvited Speaker

Google

United States

I am a staff engineer at Google, where I work on using formal methods for privacy preserving AI. Until recently, I was working as part of the exciting Swift for TensorFlow project. Previously, I led a team that develops static analysis tools to improve the security of Android Apps. Before that I was an engineer at Facebook, and a research staff member in the Systems Analysis and Verification (SAV) group at NEC Laboratories America, Inc. I got my Ph.D in from the University of Wisconsin-Madison.