Abstract:

Input-output examples have emerged as a practical and user-friendly specification mechanism for program synthesis in many environments. In this talk I will describe our recent work on giving a type-theoretic account of such synthesis processes. In this setting, examples can be seen as _refinement types_, and program synthesis can be seen as proof search. I will explain how ideas from proof search--normal forms and focusing--lead to an algorithm for synthesizing recursive functions that process algebraic datatypes. I'll sketch the theory and describe our experimental results based on two different prototype implementations. This is joint work with Peter-Michael Osera (Grinnell College), David Walker (Princeton University) and Jonathan Frankle (Georgetown Law).

Abstract:

Acceptance of autonomous systems at scales at which they can make societal and economical impact hinges on factors including how capable they are in delivering complicated missions in uncertain and dynamic environments and how much we can trust that they will operate safely and correctly. In this talk, we present a series of algorithms recently developed to address this need. In particular, these algorithms are for the synthesis of control protocols that enable agents to learn from interactions with their environment and/or humans while verifiably satisfying given formal safety and other high-level mission specifications in nondeterministic and stochastic environments. We take two complementing approaches. The first approach merges data efficiency notions from learning (e.g., so-called probably approximate correctness) with probabilistic temporal logic specifications. The second one leverages permissiveness in temporal-logic-constrained strategy synthesis with reinforcement learning.

Abstract:

Can we control a swarm of systems and give guarantees on their collective behavior? In this talk I will discuss an instance of this problem: given a large homogeneous collection of dynamical systems and a novel class of safety constraints, called counting constraints, how to synthesize a controller that guarantees the satisfaction of these constraints. Counting constraints impose restrictions on the number of systems that are in a particular mode or in a given region of the state-space over time. I will present an approach for synthesizing correct-by-construction controllers to enforce such constraints. Our approach exploits the structure of the problem, the permutation invariance of dynamics due to homogeneity and the permutation invariance of counting constraints, to achieve massive scalability. I will discuss several potential applications of this approach and illustrate it on the problem of coordinating a large collection of thermostatically controlled loads while ensuring a bound on the number of loads that are extracting power from the electricity grid at any given time.

Abstract:

Given two systems, the conformance testing problem is to check if the behaviors of the two systems are ``close'' to each other. For example, given two combinational hardware circuits over the same sets of inputs and outputs, the problem is to check that the outputs are equal for all inputs. For dynamical systems, given the same sequence of inputs, the outputs of two models may be close without being identical. This can happen, for example, if the two systems implement real numbers to different degrees of precision. In this setting, one defines a metric on traces and checks that the distance between the output traces is close in the metric, given the same sequence of inputs. The choice of metric is guided by the following desirable properties: (a) the metric should capture common sources of mismatches, (b) it should be robust w.r.t. a set of specifications (close traces should satisfy close specifications), and (c) it should be efficiently computable.

We show how the Skorokhod metric on continuous dynamical systems can be used as a suitable metric. The Skorokhod metric allows for both state value mismatches and timing distortions, and is well suited for checking conformance between idealized models of dynamical systems and their implementations. We show that the metric is robust w.r.t. an expressive quantitative temporal logic and that it can be computed in polynomial time.

We have implemented this algorithm in a simulation framework for testing Simulink blocks and our evaluations show that the Skorokhod metric can be used to find discrepant behaviors in a set of control system benchmarks.

[Joint work with Jyo Deshmukh and Vinayak Prabhu]

Abstract:

Consider the following iterative approach to improving program performance: make a random change to the program and run it on some test cases. If the program passes the tests and is faster, repeat the procedure on the modified program, otherwise try a different random change. Modulo some caveats and details, this is the algorithm that underlies STOKE, a stochastic search-based approach to program optimization and synthesis. This talk will give a survey of the STOKE project from inception to the present and try to answer a few questions, such as
* Why does randomized search over programs work at all?
* How can one prove the correctness of programs generated by a random process?
* What are the limits --- how good can tools based on randomized search really be?

Abstract:

​Perfect software has been a goal since the founding of the field of computer science. This goal has yet to be realized. Instead of attempting to produce perfect software, we instead propose to identify and enforce key acceptability properties. Examples of acceptability properties include data structure consistency, no out of bounds accesses, no infinite loops, no memory leaks, no null dereferences, no divide by zero errors, acceptable response times, and continued execution.

We discuss a variety of relatively simple mechanisms for transforming programs that may contain acceptability property violations into programs that never violate identified acceptability properties. These mechanisms dynamically monitor the execution of the program to detect impending acceptability property violations, then intervene to prevent the violation. ​The program then continues to execute along its normal execution path.

Such mechanisms do not aspire to produce perfect programs. The experimental results show, however, that they are capable of transforming large, widely deployed software systems that contain problematic software defects and security vulnerabilities into extremely robust and resilient systems that execute successfully through otherwise fatal errors and attacks.

Abstract:

Recent years have seen growing interest in high-level languages for programming networks. But the design of these languages has been largely ad hoc, driven more by the needs of applications and the capabilities of network devices than by foundational principles. The lack of a semantic foundation has left language designers with little guidance in determining how to incorporate new features, and programmers without a means to reason precisely about their code. This talk will present NetKAT, a new language for programming networks that is based on a solid mathematical foundation and comes equipped with a sound and complete equational theory. The first part of the talk will present the design of the language, including primitives for filtering, modifying, and transmitting packets; operators for combining programs in parallel and in sequence; and a Kleene star operator for iterating programs. The next part of the talk will explore the semantic underpinnings of the language, by developing a formal connection between NetKAT programs and well studied mathematical structures known as Kleene Algebras with Tests (KAT). The third part of the talk will show this connection can be put to work to solve practical problems including efficient compilation and automatic verification. Finally, I will discuss ongoing work exploring how NetKAT can be extended with constructs for supporting probabilistic programming (a collaboration with incoming ExCAPE postdoc Konstantinos Mamouras). Joint work with Carolyn Anderson (Swarthmore College), Arjun Guha (UMass Amherst), Jean-Baptiste Jeannin (CMU), Dexter Kozen (Cornell), Konstantinos Mamouras (Penn), Matthew Milano (Cornell), Cole Schlesinger (Princeton), Alexandra Silva (Nijmegen), Mark Reitblatt (Facebook), Steffen Smolka (Cornell), Laure Thompson (Cornell), and Dave Walker (Princeton).

Abstract:

Concurrent synthesis of control is undecidable. There have been many attempts to restrict the architecture in order to obtain a decidable theory, however, these restrictions are commonly rather strong. We attack the synthesis of concurrent control from a new angle: we use knowledge in order to provide the control, and when knowledge is insufficient, allow additional processes to communicate in order to achieve the desired knowledge. Hence, our synthesis problem may deviate from the original architecture, but effort is made to make this deviation minimal. With this reformalized synthesis problem, achieving control for concurrent systems becomes decidable (for imposing global invariants). I will present the knowledge based synthesis approach and the related algorithms.

Abstract:

Many security attacks arise from unanticipated behaviors that are inadvertently introduced by the system designer at various stages of development. For example, a number of security protocols that were formally proven to be secure at the abstract level have turned out to be susceptible to attacks when deployed on concrete devices. Fundamentally, there exists an inherent tension between abstraction -- a key technique in design of any large system -- and the complex nature of security attacks, which often involve details across multiple abstraction layers. How do we resolve this tension during construction of secure systems?

To explore this question, my colleagues and I have developed an approach to formal security analysis called the multi-representational security analysis. With our tool, Poirot, a designer begins with an initial, abstract model of the system, and incrementally elaborates the model into a more concrete one by selecting the underlying representations of system components. At each iteration, Poirot's verification engine performs an automated analysis to check the system against a desired security property, and discover attacks that exploit details across multiple levels of abstraction. Poirot also has an extensible library of domain-specific models that can be reused for analysis of multiple systems. In this talk, I will describe our experience applying Poirot to analyze security of publicly deployed web systems.

Abstract:

Motivated by the need to secure critical infrastructure against sensor attacks, in this talk I will focus on a problem known as "secure state estimation”. It consists of estimating the state of a dynamical system when a subset of its sensors is arbitrarily corrupted by an adversary. Although of critical importance, this problem is combinatorial in nature since the subset of attacked sensors in unknown. Previous work in this area can be classified into two broad categories. The first category is based on numerical optimization techniques. These techniques are well suited to handle the continuous part of the problem, estimating the real-valued variable describing the sate, if the combinatorial part of the problem has been solved. The second category is based on Boolean reasoning which is well suited to handle the combinatorial part of the problem, if the continuous part of the problem has been solved. However, since we need to simultaneously solve the combinatorial and the continuous part of the secure state estimation problem, the existing approaches result in algorithms with worst case exponential time complexity.

In this talk, I will present a novel and efficient algorithm for the secure state estimation problem that uses the lazy SMT approach in order to combine the power of both SAT solving as well as convex optimization. While SAT solving is used to perform the combinatorial search, convex optimization techniques are used to reason more efficiently about the real-valued state of the system and/or generating theory lemmas explaining conflicts in the combinatorial search. We show that by splitting the reasoning between the two domains (Booleans and Reals) and intermixing a powerful tool from each domain, we obtain a new suite of tools that scales more favorably compared to the previous techniques. I will start by discussing the simplest case when the underlying dynamics are linear, sensors are perfect (noise-less), and only data collected over a finite window is considered. I will then move forward by showing three extensions to handle noisy measurements, recursive implementations (data over infinite windows) and nonlinear dynamics.

Abstract:

Data manipulation is a common task for many users ranging from developers who need to perform refactorings to data analysts who need to extract information from semi-structure data as text files. Although there are tools for automating these tasks, they may fail to correctly perform the desired data manipulation reducing the user’s confidence in these tools. We envision that program synthesis is a key solution for enabling better data manipulation tools. In this talk, I will present an automated technique for testing of refactoring engines. As test inputs, it exhaustively synthesizes programs for a given scope of Java declarations. Testers can specify the desired test input in a declarative way by using Alloy. The technique has been useful for identifying more than 100 bugs in state-of-the-art industrial and academic refactoring engines. Next, I will present FlashProg, a framework that provides UI support for several programming by example engines related to data manipulation. FlashProg implements two novel user interaction models to resolve ambiguities in example-based specification, thereby increasing user’s trust in the results. Our user studies show that each of these models significantly reduces the number of errors in the performed task. I will conclude the talk by discussing exciting research challenges in program synthesis and possible approaches to tackle them.

Abstract:

Progress in computation and communication technologies has made it easier to integrate software in all walks of life. The social, economical, and environmental benefits of integrating software into avenues such as avionics, automotives, power grid, and medicine lead to the rise of CPS as an important area of research. However, bugs in software systems deployed in such safety-critical scenarios can lead to loss of property and in some cases life. In this talk, I will present dynamic analysis technique for formally verifying annotated Cyber-Physical Systems and prove the absence of bugs. The annotations, called discrepancy functions, are extensions of proof certificates for analyzing convergence or divergence of systems. One of the key advantages of dynamic analysis is that it leverages the testing procedures which are the only known scalable way of ensuring the system specification. I have developed a tool C2E2 that implements this technique and verifies temporal properties of CPS. C2E2 has been applied to verify alerting mechanisms in parallel aircraft landing protocol developed by NASA and to verify specification of powertrain control system presented as a verification challenge problem by Toyota.

Abstract:

Inductive programming (IP) is an area of research concerned with learning recursive programs, typically in some declarative language, from small sets of input/output examples. Since a general program is induced from examples, IP can be seen as a special case of machine learning. In contrast to standard machine learning, induced program hypothesis are required to cover all given examples correctly. In the talk I will give a general introduction to the research area of IP and then focus on induction of functional programs. Here I first will present the classical approach of learning Lisp programs by regularity detection and then I will present a current approach, called IgorII which integrates concepts from this approach, concepts of contemporary programming languages, such as pattern matching, as well as concepts proposed in Inductive Logic Programming (ILP).

Abstract:

Multi-agents games are extensively used for modelling settings in which different entities share resources. For example, the setting in which entities need to route messages in a network is modeled by network-formation games: the network is modeled by a graph, and each agent has to select a path satisfying his reachability objective. In practice, the objectives of the entities are often more involved than reachability. The need to specify and reason about rich specifications has been extensively studied in the context of verification and synthesis of reactive systems. The talk describes a lifting of ideas from formal methods to multi-agent games. For example, in network-formation games with regular objectives, the edges of the graph are labeled by alphabet letters and the objective of each player is a regular language over the alphabet of labels. Thus, beyond reachability, a player may restrict attention to paths that satisfy certain properties, referring, for example, to the providers of the traversed edges, the actions associated with them, their quality of service, security, etc.

The talk assumes no previous knowledge in game theory. We will introduce the basic concepts and problems, describe how their extension to games with more expressive specification of objectives poses new challenges, and study the resulting games.

Joint work with Guy Avni and Tami Tamir.

Abstract:

Parameterized systems consist of an arbitrary number identical interacting components. Parameterized specifications and systems occur quite naturally. There is a large body of work on parameterized verification, but synthesis has thus far received little attention. The typical approach is currently to synthesize systems for a few parameter values, which yields systems that are significantly larger as the parameter increases. Our goal is to automatically construct parameterized systems instead. I will discuss both pragmatic ways to do this and the decidability barrier that we must avoid.

Abstract:

The talk will briefly describe three of Turing’s major achievements, in three different fields: computability, biological modeling and artificial intelligence. Interspersed with this, I will explain how each of them directly motivated and inspired me to work on a number of topics over a period of 35 years, the results of which can all be viewed humbly as extensions and generalizations of Turing’s pioneering and ingenious insights.

Abstract:

We discuss how Horn constraints featuring recursion, forall/exists quantifier alternation, and well-foundedness conditions can be used for expressing a wide range of questions about programs. We also discuss corresponding solving methods and tools.

Abstract:

Software synthesis is a technique for automatically generating code from a given specification. The goal of software synthesis is to make software development easier while increasing both the productivity of the programmer and the correctness of the produced code. In this talk I will present an approach to synthesis that relies on the use of automated reasoning and decision procedures. First I will describe how to generalize decision procedures into predictable and complete synthesis procedures. Here completeness means that the procedure is guaranteed to find code that satisfies the given specification. I will illustrate the process of turning a decision procedure into a synthesis procedure using linear integer arithmetic as an example. In addition, I will outline a procedure that synthesizes code snippets from specifications implicitly given in the form of type constraints. As there can be multiple solutions, more than one code snippet can be a good candidate. We use an additional weight function to rank the derived snippets and direct the search for them. In practical evaluation, our technique scales to programs with thousands of visible declarations in scope and succeeds in 0.5 seconds to suggest program expressions of interest. I will conclude with an outlook on possible future research directions and applications of synthesis procedures.

Abstract:

Designing and fabricating new robotic systems is currently typically limited to experts, requiring engineering background, expensive tools, and considerable time. What if instead, we could automatically generate programmed functional robots from a simple description of the problem at hand? By enabling the creation of integrated electromechanical systems by casual everyday users, we can get to a point where we can say for any task, "there's a robot for that."

We take the first steps towards this vision with a system that can easily create programmed printable robots from high-level structural specifications. A user merely needs to select electromechanical components from a library of basic building blocks and pre-designed mechanisms, then connect them to define custom robot assemblies. The system then generates complete mechanical drawings suitable for fabrication, instructions for the assembly of electronics, and software to control and drive the final robot.

Abstract:

Kestrel's Specware system is designed to support the specification of software requirements in a classical higher-order logic and then to automatically refine the specifications down to correct, executable source code, in CommonLisp, Java, and C. Most refinements are generated by high-level transformations from Specware's library. The developer writes a metaprogram that specifies the sequence of transformations and how they apply. In recent work we have been extending our transformations so that they emit both a refinement step and a checkable proof of the correctness of the refinement step.

To illustrate this approach we discuss an ongoing DARPA-sponsored project focused on the synthesis of concurrent garbage collectors. To handle the specification and refinement of stateful/concurrent processes, we developed techniques for a mixed algebraic/coalgebraic-style of specification, and developed new coalgebraically-oriented refinement techniques. We generate refinements using purely functional calculation based on the axioms and theorems of the domain specification. As a final step, we transform the coalgebraic operators to stateful form and encapsulate the top-level processes as threads. To date we have synthesized a family of collectors from a common specification. Other applications have included the synthesis of high-performance schedulers, constraint solvers, and network protocol handlers.

Abstract:

Configuration updates are a leading cause of instability in networks today. A key factor that makes updates difficult to implement is that networks are distributed systems with hundreds or thousands of nodes all interacting with each other. Even if the initial and final configurations are correct, naively updating individual nodes can easily cause the network to exhibit incorrect behaviors such as forwarding loops, black holes, and security vulnerabilities. This work presents a new approach to the network update problem: we automatically generate updates that are guaranteed to preserve important correctness properties. Our system is based on counterexample-guided search and incorporates heuristics that quickly identify correct updates in many situations. We exploit the fact that the search algorithm asks a series of related model checking questions, and develop an incremental LTL model checking algorithm. We present experimental results showing that our tool efficiently generates updates for real-world topologies with thousands of nodes.

Abstract:

From very early on, philosophers have dreamed of machines that can reason. The idea of automating logical reasoning is nearly as old as formal logic itself, but the limited success of early attempts in this area, as well as discouraging complexity and decidability results, left many with the impression that practical automated reasoning would never be possible. In the last decade, breakthroughs in Boolean satisfiability (SAT) and Satisfiability Modulo Theories (SMT) have begun to change this perception. Today, a wide variety of applications leverage the automated reasoning power of SAT and SMT solvers to do remarkable things. In this talk I will discuss the rise of modern satisfiability techniques, with an emphasis on SMT. I will give a brief overview of how an SMT solver works "under the hood" and will discuss some exciting current applications of SMT solvers. I will conclude with projections for the future of automated reasoning generally and SMT in particular.

Abstract:

Opacity is a confidentiality property that arises in the analysis of security properties in networked systems. It characterizes whether a "secret" of the system can be inferred by an intruder who knows the system model and partially observes the system behavior. The secret could for instance be a set of system states that should not be revealed to the intruder. The secret of the system is opaque if whenever the secret has occurred (i.e., the system has reached a secret state), there exists another "non-secret" behavior that is observationally equivalent to the intruder.

In this work, we capture the dynamics of the system using a finite-state automaton model, and we assume that the system is not opaque at the outset. Our strategy is to enforce opacity by using an "insertion function" at the output of the system. Specifically, an insertion function is an interface that changes the system’s output behavior by inserting additional observable events. This interface does not interact with the system but only affects its output behavior. Such an enforcement mechanism is applicable to systems whose dynamics cannot be modified, such as that of users querying servers for instance. We establish necessary and sufficient conditions for the existence of a valid insertion function that renders the system opaque with respect to the given secret. We describe how to synthesize a valid insertion function when one exists. For this purpose, we develop a finite structure called the "All Insertion Structure" (AIS) that enumerates all valid insertion functions. Then, we address the problem of synthesizing an "optimal" insertion function (with respect to given insertion costs), by solving a minimax optimization problem over the AIS. We illustrate our results on an example where a user of location-based services wishes to keep her location secret from the servers she queries.

This is joint work with Yi-Chin Wu at the University of Michigan.

Abstract:

Domain-specific languages (DSLs) are useful for capturing and reusing engineering expertise. They can formalize industrial patterns and practices while increasing the scalability of verification, because input programs are written at a higher level of abstraction. However, engineering new DSLs with custom verification is a non-trivial task in its own right, and usually requires programming language, formal methods, and automated theorem proving expertise.

In this tutorial we present FORMULA 2.0, which is formal framework for developing DSLs. FORMULA specifications are succinct descriptions of DSLs, and specifications can be immediately connected to state-of-the-art analysis engines without additional expertise. FORMULA provides: (1) succinct specifications of DSLs and compilers, (2) efficient compilation and execution of input programs, (3) program synthesis and compiler verification.

We take a unique approach to provide these features: Specifications are written as strongly-typed open-world logic programs. These specifications are highly declarative and easily express rich synthesis / verification problems. Automated reasoning is enabled by efficient symbolic execution of logic programs into quantifier-free constraints, which are dispatched to the state-of-the-art SMT solver Z3. FORMULA has been applied within Microsoft to develop DSLs for verifiable device drivers and protocols. It has been used by the automotive / embedded systems industries for software / hardware co-design under hard resource allocation constraints.

Abstract:

This talk has two purposes. The first is to describe research on a model of concurrency that we have developed in the Computational Modeling and Analysis of Complex Systems (CMACS) project call Generalized Synchronization Trees. In their original formulation, synchronization trees modeled the behavior of nondeterministic discrete-time reactive systems and served as the foundational theory upon which process algebra, with its rich array of composition operators, was based. Our goal in this work is to provide a similar foundational theory of composition for varieties of different notions of time, including discrete, continuous, hybrid and others. To do this, a general notion of tree is proposed, and different general notions of composition studied. Two different notions of (bi)simulation are compared in this new model and found to yield different equivalences.

The second purpose of this talk is to ruminate on how this work, which was the outcome of extensive interactions between a computer scientist, a control theorist, and an ECE student, came into existence. In particular, I will reflect on the original motivations of the work, the obstacles (terminological, conceptual, and intuitive) we faced in working together, and the means around them that we uncovered.

Abstract:

Completely automated software verification succeeds currently only for shallow properties of programs. Deeper properties of software, like checking whether a memory management routine in an operating system ensures that no two apps get allocated the same block of memory, needs manual help. The paradigm of deductive verification, where programs are annotated with modular annotations of pre/post conditions, object invariants, loop invariants, etc. is about the only scalable approach to building reliable and secure code. Armed with such invariants, the program verification problem reduces to a purely logical validity problem, large parts of which can be tackled using automated logic solvers.

The paradigm is however fraught with significant annotation overhead on the programmer. The burden of annotation comes in two ways: (a) writing loop invariants, which is often hard and awkward to write, and (b) writing proof tactics or triggers which help the underlying theorem prover prove verification conditions, which are also hard and require knowledge of the underlying theorem prover.

I will report work done at Illinois in my group in tackling these problems, in order to aid the programmer to far easily write and verify software. This includes work on (a) natural proofs, which are automatic proof tactics to help prove higher-order properties of heap manipulation, (b) learning techniques to automatically infer plausible loop invariants and pre/post conditions, and (c) experience in building large systems software from scratch with proven security guarantees using deductive verification.

Abstract:

The classical formulation of the program-synthesis problem is to find a program that meets a correctness specification given as a logical formula. Recent work on program synthesis and program optimization illustrates many potential benefits of allowing the user to supplement the logical specification with a syntactic template that constrains the space of allowed implementations. Our goal is to identify the core computational problem common to these proposals in a logical framework. The input to the syntax-guided synthesis problem (SyGuS) consists of a background theory, a semantic correctness specification for the desired program given by a logical formula, and a syntactic set of candidate implementations given by a grammar. The computational problem then is to find an implementation from the set of candidate expressions so that it satisfies the specification in the given theory. We describe three different instantiations of the counter-example-guided-inductive-synthesis (CEGIS) strategy for solving the synthesis problem, report on prototype implementations, and present experimental results on an initial set of benchmarks.

I will also discuss plans for the next steps in this project. These consist of (1) finalizing the input syntax of SYNTH-LIB based on the input format of SMT-LIB2, with an accompanying publicly available parser, (2) building a more extensive and diverse repository of benchmarks, and (3) organizing a competition for SyGuS-solvers. We welcome feedback and help from the community on all of these steps.

Joint work with Ras Bodik, Garvit Juniwal, Milo Martin, Mukund Raghothman, Sanjit Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhsihek Udupa.

Abstract:

Synthesis is the automated construction of a system from its specification. The system has to satisfy its specification in all possible environments. Modern systems often interact with other systems, or agents. Many times these agents have objectives of their own, other than to fail the system. Thus, it makes sense to model system environments not as hostile, but as composed of rational agents; i.e., agents that act to achieve their own objectives. We introduce the problem of synthesis in the context of rational agents (rational synthesis, for short). The input consists of a temporal-logic formula specifying the system and temporal-logic formulas specifying the objectives of the agents. The output is an implementation T of the system and a profile of strategies, suggesting a behavior for each of the agents. The output should satisfy two conditions. First, the composition of T with the strategy profile should satisfy the specification. Second, the strategy profile should be an equilibria in the sense that, in view of their objectives, agents have no incentive to deviate from the strategies assigned to them. We solve the rational-synthesis problem for various definitions of equilibria studied in game theory.

This is a joint work with Orna Kupferman and Yoad Lustig.