These abstracts are for talks at this event.
NEPLS is a venue for ongoing research, so the abstract and supplemental material associated with each talk is necessarily temporal. The work presented here may be in a state of flux. In all cases, please consult the authors' Web pages for up-to-date information. Please don't refer to these pages as a definitive source.
Finding Relevant Code with Causal Inference
James Koppel (MIT)
Given an effect of a program -- say, a window drawn on the screen, or part of its output -- how do you determine what code caused that effect? Previous work is based on variants of slicing, which has the tendency to find large amounts of irrelevant code along with the necessary pieces, and requires access to library code. Our preliminary work promises much better results by taking data from program traces and applying techniques that can distinguish causation from correlation. We use a quantity called the causal influence, which allows us to show when the correlation between two events is sufficiently strong that it proves a causal relation and cannot be purely due to spurious correlation.
Linear Models of Computation and Parametrization of Large Classes of Programs by Matrices
Michael Bukatin (Nokia Corporation, Burlington, MA)
We look at two classes of computations with streams admitting the notion of linear combination of streams: probabilistic sampling and generalized animations. Focusing on these classes of computations does not seem to restrict the computational power of our models, because one can sample from probability distributions over spaces of programs, and because there is enough room for a variety of higher-order programming methods in the architectures we consider in this work. In the context of genetic programming, this architecture can be used to express the notion of regulation of gene expression. We consider dataflow programming with these types of streams and note that adopting a discipline of structuring dataflow programs as bipartite graphs connecting the vertices computed by built-in transformations and the vertices computed by potentially infinitary linear transformations allows to parametrize large classes of dataflow graphs by matrices of real numbers, which makes it possible to modify programs in continuous fashion. Prototype implementations of the architectures in question are at https://github.com/anhinga/fluid repository. There is a mathematical landscape adjacent to this topic which is based on the fact that in the presence of partial contradictions domains for denotational semantics tend to become embedded into vectors spaces. This landscape brings together vector semantics of programming languages, various expressions of partial inconsistency including negative values of measure and probability and negative degrees of set membership, non-monotonic reasoning, bilattices, bitopologies, and more. This is joint work with Steve Matthews (University of Warwick)
Phantom Monitors: A Simple Foundation for Modular Proofs of Fine-Grained Concurrent Programs
Christian J. Bell (MIT)
Formal verification of fine-grained concurrent programs poses many thorny challenges, including the tension between support for optimized implementation techniques and support for modular proofs of libraries that use those techniques. Even surveying just the last few years, many program logics have been proposed to address different subsets of the challenges, with each program logic introducing its own vocabulary of foundational concepts and proof rules. In this work, we take some first steps along a different path to the same goal. We support modular proofs of fine-grained concurrent code within the Coq proof assistant. Instead of defining a program logic, we push almost all work onto the very expressive higher-order logic built into Coq. We define our foundation, phantom monitors, and explore its consequences in verification of two classic data structures (the Treiber lock-free stack and the Harris-Michael lock-free set). We then show how to verify client programs of these data structures, almost completely automatically, leading to highly trustworthy theorems whose statements depend only on the chosen specs and on the operational semantics of our object language.
Slimming Languages by Reducing Sugar: A Case for Semantics-Altering Transformations
Justin Pombrio (Brown University)
What's Wrong with Git? A Conceptual Design Analysis
Santiago Perez De Rosso (MIT)
Git is a widely used version control system that is powerful but complex. Some have claimed that the complexity of Git is not a necessary consequence of its power and flexibility but instead arises from its design. To explore this hypothesis, we analyzed the design of Git using a theory of design that identifies concepts and their distinct purposes. A selection of known complications of Git is presented and explained using this structure. Based on this analysis, we designed a reworking of Git (called Gitless) that attempts to remedy the conceptual difficulties that lead to these complications. We then evaluated Gitless in a small study to determine whether users experienced fewer complications using Gitless in place of Git. This is joint work with Daniel Jackson (MIT CSAIL).
Nested Queries in Nondeterministic and Probabilistic Programming Languages
Jeffrey Mark Siskind (Purdue University)
Early Prolog lacked a construct to aggregate alternative results of deterministic queries, though the setof and bagof extralogical predicates were soon added. Early nondeterministic functional languages, e.g. Schemer, also lacked a construct to aggregate alternative possible values of a nondeterministic expression, though the all-values construct was added to Screamer. Early probabilistic languages, e.g. Church, Anglican, and Probabilistic C, also lacked a construct to aggregate the samples produced by a stochastic processes into a distribution, though a construct to do so was included in R6RS-AD. We investigate the formal semantics of such constructs and find that they raise thorny issues. One can freely nest nondeterministic choice and aggregation constructs in nondeterministic languages with a well defined semantics. Similarly, one can also freely nest stochastic sampling and aggregation constructs in probabilistic languages with a well defined semantics. But surprisingly, arbitrary nesting of such constructs in a language that provides both nondeterminism and stochasticity becomes incoherent unless certain constraints are upheld. Even more surprisingly, this thorny issue has little to do with the mixing of nondeterminism and stochasticity per se. One can extend both nondeterministic and stochastic languages independently with stratified (i.e. tagged) aggregation constructs and cause the same thorny issues to arise. Yet the mixed nondeterministic and stochastic languages, as well as adding stratified aggregation to nondeterministic and/or stochastic languages, is a useful modeling construct. Thus to achieve such utility we must live with these issues.
Composable Modular Atomicity
Mohsen Lesani (MIT)
To preserve the consistency of data, operations that concurrently access objects should execute atomically. Due to the intricacy of synchronization, encapsulating atomicity in modules can improve both the programmability and verifiabilty of user programs. Therefore, mainstream programming languages offer libraries of concurrent data types. An important question is how composable these concurrent data types are. They usually guarantee linearizability that supports horizontal composition. An execution may involve method calls on multiple concurrent objects and each method call appears to take effect atomically. However, they usually don't support vertical composition. The execution of multiple method calls on a concurrent object is not necessarily atomic. I present a sufficient condition called condensability for atomicity of vertical compositions and a tool called Snowflake that generates proof obligations for condensability of composing methods in Java and discharges them using an off-the-shelf SMT solver. As presented in CAV'14, Snowflake could successfully verify a large fraction of composing methods in several open-source applications. Then, I present universally composable concurrent objects and how synthesis from high-level relational specifications can directly target them. Finally, I briefly present our current effort to build a verification framework for composable concurrent objects in Coq.
Using a Portfolio of SMT Solvers in Software Development
Will Blair (Boston University)
SMT solvers are powerful tools that determine the satisfiability of formulas from different first order theories. There are many theories that could be useful for software development and yet are outside the capability of automated solvers. Solving formulas that require induction on algebraic data types, for example, cannot be handled by most current solvers. Yet, earlier this year the CVC4 team demonstrated a new technique for proving formulas that require inductive reasoning. As different solvers develop new capabilities that complement one another, we would like ways to combine them in order to improve the software development process. In this talk, we will describe how dependent types in ATS can be used as an interface for introducing different SMT solvers with their own unique capabilities into software development. The correspondence between the ATS statics that support dependent types and the well supported SMT-LIB language allows us to easily export constraints to a variety of SMT solvers. This allows a programmer to use the decision power of different SMT solvers without needing to interact with them directly. We will illustrate this by discussing a small example of using CVC4's new strategy for inductive proofs to reason about list operations in ATS.
Session Types in Applied Type System
Hanwen Wu (Boston University)
Pi-calculus [Milner91, Milner99] is a powerful tool for describing concurrent computations. Session types [Honda98] later becomes a type discipline for pi-calculus that successfully captures the invariants of communication channels. Since then session types have been actively studied in a variety of literature. Despite the fact that practical implementations are limited, its applications for enforcing communication protocols, guaranteeing global progress, etc, are promising. In this talk, we will show that session types can be easily modeled in ATS [Hongwei04], a statically typed programming language, with the help of its dependent types and linear types. To the best knowledge of the author, this is the first practical session type language that is ready to use in real world. Session type linearity has been studied in several lines of literature from Walder, Pfenning, etc. And that can be clearly shown when we assign types to channels in ATS. Dependent session types are also supported in ATS. Underlying implementation after type erasure is done via Erlang, benefiting from its industrial runtime. Examples will also be given to demonstrate the usage and benefits of session types.
Tierless Programming and Differential Reasoning for Software-Defined Networks
Tim Nelson (Brown University)
Flowlog is a tierless language for programming SDN controllers. We intentionally limit Flowlog's expressive power to enable powerful reasoning support. To showcase this we present Chimp, a tool for differential analysis of Flowlog programs. Given two versions of a program, Chimp produces a set of concrete scenarios where the programs differ in their behavior. By using tools like Chimp, network developers can exploit the power of formal methods without having to be trained in formal logic.
|Last modified Sunday, November 8th, 2015 1:11:35pm|