In order to provide high availability and operate in unreliable environments, many critical applications are implemented as distributed systems. Unfortunately, the need to handle unreliable networks, machine crashes, and churn--the spontaneous arrival and departure of nodes to and from a network--has made these systems difficult to implement correctly. Recent work has proved the correctness of such implementations using proof assistant software. However, these frameworks do not support reasoning about churn. To address this limitation, we introduced support for implementing and verifying systems under churn to the Coq-based Verdi framework. With a model for the network in hand we could implement and begin to verify systems. However, for most systems under churn we need to prove punctuated safety properties. These properties allow a system to break some promises during and after churn, but stipulate that safe behavior be restored sometime after churn stops. Such a property is best proved by reasoning about infinitely long system executions, but this was impossible in Verdi and always awkward in Coq. We built tools for high-level reasoning about infinite sequences of events in Verdi using existing ideas from linear temporal logic in order to prove punctuated safety. To establish the efficacy of all these new tools, we have built an implementation of the Chord distributed lookup protocol and are currently proving it correct. Chord was designed to evenly distribute resources or tasks across a set of nodes even as some enter and leave the network. Recently, a study using a formal model of Chord's protocol showed that certain kinds of node failures or joins could cause system failure. While a new specification has been developed which avoids these problems, it has not been implemented or fully verified. We are developing the first verified implementation of Chord.

Additive manufacturing - the process behind 3D printing - has been growing in widespread use since the introduction of the first commercially-available desktop printer and later improvements in cost, quality, and accessibility. Expanding horizontally and vertically in the global market, the 3D printing industry has been one that not only appeals to hobbyists, but has demonstrated potential as a solution to a variety of challenges faced around the world today, including those in biotechnology, aerospace, and industrial engineering. Seeking to take advantage of the increasing demands in 3D printing technologies, a number of companies and open-source organizations are offering new types of 3D printers and associated software. However, the rapid growth and diversity of the products being released have resulted in a loss of universal standards. Often indented to be accessible and reliable regardless of a user’s technical background, 3D printing technologies have been known to require consumers to learn the more technical aspects of their printer, G-Code, slicing software, materials, etc. in order to configure their overall setup and reduce the prevalence of errors. Our project aims at using advanced parsing strategies, program optimization, and statistical analysis to provide a universal, easy-to-use tool that both analyzes and optimizes G-Code files prior to printing. By automating the common fixes users are required to implement in their G-Code files and identifying common factors in 3D prints (material warping, inadequate temperatures, speed of extruder heads, etc.), this tool is intended to be usable for any consumer, regardless of engineering or design experience. Ultimately, our goal is to help provide a universal solution to the lack of consistency between products, and help leverage the promising field of 3D printing to reach its potential as both a home essential and reliable solution in fields such as biotechnology and industrial engineering.