8:30-9:30 | Breakfast |
9:30-10:30 | Automating Abstract Interpretation | Tom Reps | Details |
Abstract |
Unfortunately, the problem of determining whether a program is correct is undecidable. Program-analysis and verification tools sidestep the tar-pit of undecidability by working on an abstraction of a program, which over-approximates the behavior of the original program. The theory underlying this approach is called abstract interpretation. Abstract interpretation provides a way to obtain information about the possible states that a program reaches during execution, but without actually running the program on specific inputs. Instead, it explores the program's behavior for all possible inputs, thereby accounting for all possible states that the program can reach. Operationally, one can think of abstract interpretation as running the program "in the aggregate". That is, rather than executing the program on ordinary states, the program is executed on abstract states, which are finite-sized descriptors that represent collections of states.
However, there is a glitch: abstract interpretation has a well-deserved reputation of being a kind of "black art", and consequently difficult to work with. This talk will describe a twenty-year quest address this issue by raising the level of automation in abstract interpretation. I will present several different approaches to creating correct-by-construction analyzers. Somewhat surprisingly, this research has recently allowed us to establish connections between our problem and several other areas of computer science, including machine learning, knowledge compilation, data integration, and constraint programming.
(Joint work with Aditya Thakur and a variety of students over several years.) |
Speaker Bio |
Note: these are excerpts from http://pages.cs.wisc.edu/~reps/reps-bio.html.
Thomas W. Reps is the J. Barkley Rosser Professor & Rajiv and Ritu Batra Chair in the Computer Sciences Department of the University of Wisconsin, which he joined in 1985. Reps is the author or co-author of four books and more than one hundred seventy-five papers describing his research (see http://www.cs.wisc.edu/~reps). His work has concerned a wide variety of topics, including program slicing, dataflow analysis, pointer analysis, model checking, computer security, code instrumentation, language-based program-development environments, the use of program profiling in software testing, software renovation, incremental algorithms, and attribute grammars.
His collaboration with Professor Tim Teitelbaum at Cornell University from 1978 to 1985 led to the creation of two systems—the Cornell Program Synthesizer and the Synthesizer Generator—that explored how to build interactive programming tools that incorporate knowledge about the programming language being supported. The systems that they created were similar to modern program-development environments, such as Microsoft Visual Studio and Eclipse, but pre-dated them by more than two decades. Reps is President of GrammaTech, Inc., which he and Teitelbaum founded in 1988 to commercialize this work.
Professor Reps received his Ph.D. in Computer Science from Cornell University in 1982. His Ph.D. dissertation won the 1983 ACM Doctoral Dissertation Award.
Reps has also been the recipient of an NSF Presidential Young Investigator Award (1986), a Packard Fellowship (1988), a Humboldt Research Award (2000), and a Guggenheim Fellowship (2000). He is also an ACM Fellow (2005). In 2013, Reps was elected a foreign member of Academia Europaea.
|
10:30-11:00 | Coffee Break |
11:00-11:20 | Secure Distributed Transactions With Information Flow Restrictions | Isaac Sheff | Details |
Abstract |
Atomic Transactions are a popular programming abstraction for distributed systems. However, when a system incorporates elements in different trust domains, the scheduling and commit procedures for transactions may themselves leak information. Two-phase commit, for example, can issue ""abort"" messages to everyone involved in a transaction, revealing that one participant is busy with some other transaction.
In our ongoing work, we explore the limits of distributed, secure transaction commits. We demonstrate that monotonically increasing security levels are sufficient to create a safe scheduling algorithm for single-threaded transactions, even in an open system (where not all possible transactions are known in advance), and provide examples of impossible-to-schedule transactions, with an eye toward deriving even more permissive, safe scheduling in some circumstances.
|
11:20-11:40 | Tool Demo: An Extensible IDE Framework for Polyglot Languages | Jed Liu | |
11:40-12:00 | Effect Tokens | Andrew K. Hirsch | Details |
Abstract |
Effect tokens are a way of representing the ordering effects impose on a program graph. However, current techniques for deciding when to force ordering are naive. This talks describes our current project, which looks into the mathematical foundations of effect tokens, and when we can soundly not force sequencing in the face of effectful computations.
|
12:00-13:30 | Lunch |
13:30-14:10 | PL Quizzo |
14:10-14:30 | Making Subtyping more Intelligent via Preprocessing | Fabian Muehlboeck | Details |
Abstract |
Advanced type-system features often interact with subtyping in ways that make it difficult to algorithmically prove certain intended subtyping relationships.
In particular, introducing intersection and union types into an otherwise nominal object-oriented type system produces several hard cases for algorithmic subtyping, such as distributivity of intersections through unions. For this reason, existing languages that feature intersection and union types often do not support distributivity, among other features, even though distributivity is the easiest of the features that we are addressing.
We present a general strategy of preprocessing types to make subtyping more intelligent.
We apply this strategy to distributivity, disjointness of types, and consolidating cases of sum types.
Moreover, we extend this strategy to work in the presence of variant generics, addressing the additional challenge of terminating subtyping in this setting.
In summary, we formalize conditions for preprocessing operators on types that enable simple, syntax-directed subtyping relations to capture additional desired subtyping relationships, while still retaining decidability.
|
14:30-14:50 | PreFab: a language for secure open applications | Owen Arden | Details |
Abstract |
Open applications are distributed applications with rich interfaces that can be extended and executed across administrative domains. Web services with APIs, online games with mods, and federated websites like health insurance exchanges are all examples of open applications.
Because open applications blur the boundaries between trusted and untrusted components, traditional approaches to security are inadequate.
To address this shortfall, we are developing PreFab, a language that provides compositional security for open applications using information flow control. PreFab is based on the Flow-Limited Authorization Model (FLAM), a new model for information flow security designed for distributed settings. In this talk I will briefly introduce FLAM, discuss the motivation and design goals of PreFab, and present initial progress.
|
14:50-15:20 | Coffee Break |
15:20-15:30 | ModelPlex: Verified Runtime Validation of Verified CPS Models | André Platzer | Details |
Abstract |
Formal verification and validation play a crucial role in making cyber-physical systems (CPS) safe. Formal methods make strong guarantees about the system behavior if accurate models of the system can be obtained, including models of the controller and of the physical dynamics. In CPS, models are essential; but any model we could possibly build necessarily deviates from the real world. If the real system fits to the model, its behavior is guaranteed to satisfy the correctness properties verified w.r.t. the model. Otherwise, all bets are off. This paper introduces ModelPlex, a method ensuring that verification results about models apply to CPS implementations. ModelPlex provides correctness guarantees for CPS executions at runtime: it combines offline verification of CPS models with runtime validation of system executions for compliance with the model. ModelPlex ensures that the verification results obtained for the model apply to the actual system runs by monitoring the behavior of the world for compliance with the model, assuming the system dynamics deviation is bounded. If, at some point, the observed behavior no longer complies with the model so that offline verification results no longer apply, ModelPlex initiates provably safe fallback actions. This paper, furthermore, develops a systematic technique to synthesize provably correct monitors automatically from CPS proofs in differential dynamic logic.
|
15:30-15:40 | Probabilistic NetKAT | ½ Dexter Kozen + ½ Nate Foster | Details |
Abstract |
This talk will describe a new language for programming software-defined
networks based on a probabilistic semantics. We extend the NetKAT
language with new primitives for expressing probabilistic behaviors
and enrich the semantics from one based on deterministic functions to
one based on measures and measurable functions on sets of packet
histories. We establish fundamental properties of the semantics, prove
that it is a conservative extension of the deterministic semantics,
and show that it satisfies a number of natural equations. We present
case studies that show how the language can be used to model a diverse
collection of scenarios drawn from real-world networks.
|
15:40-15:45 | Managing your digital life | Elisavet Kozyri | Details |
Abstract |
We discuss the problem of creating a personal information management system, which handles in a decentralized manner, the storage and distribution of information that a user daily generates. This presentation is inspired by [1].
[1] Serge Abiteboul, Benjamin Andre, Daniel Kaplan, Managing Your Digital Life, Communications of the ACM, May 2015, Vol. 58, No. 5.
|
15:45-15:50 | Fixing the tragedy of exceptions | Yizhou Zhang | Details |
Abstract |
Exception mechanisms in current languages are not well designed and do not meet the goals of an effective exception mechanism. I will talk about our work in progress on a novel exception mechanism that addresses the weaknesses of existing ones: lack of static reasoning, high performance overhead, and incompatibility with higher-order functions.
|
15:50-15:55 | MyriaStore: programming with heterogeneous consistency | Matthew Milano | Details |
Abstract |
Modern cloud-based application programming requires low latency and high availability across the globe, leading programmers to employ data stores with weakened consistency semantics. To make matters worse, existing web applications often have need for different consistency guarantees on objects in the same program, leading to a heterogeneous consistency semantics where the effect of "x := 5" depends heavily on where "x" is stored. In this talk, we present MyriaStore, a new framework and language which uses an information-flow type system and lightweight runtime causality tracking to provide a sane programming environment atop today's heterogenous data stores.
|
15:55-16:10 | Short talks Q & A |
16:10-17:00 | Panel Discussion: PL research impact | Dexter Kozen, Andrew Myers, and Tom Reps | |
17:00-18:00 | Lawn games |
18:00-20:00 | Dinner and bowling at Atlas |