|
4 April 2016, 1pm EST:
Steve Zdancewic
Type- and Example-Directed Program Synthesis
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).
|
|
7 Mar 2015
Adaptable yet provably correct autonomous systems
by
Ufuk Topcu
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.
|
|
1 Feb 2016
Control synthesis for large collections of dynamical systems with counting constraints
by
Necmiye Ozay
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.
|
|
4 Jan 2016
Testing System Conformance for Cyber-Physical Systems
by
Rupak Majumdar
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]
|
|
2 Nov 2015:
STOKE: Program Optimization and Synthesis using Randomized Search
by
Alex Aiken
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?
|
|
5 Oct 2015:
Intervention and Adaptation for Enforcing Acceptability Properties
by
Martin Rinard
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.
|
|
14 Sep 2015:
Specifying and Verifying Network Behavior with NetKAT
by
Nate Foster
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).
|
|
4 May 2015:
Concurrent Control Synthesis using Knowledge
by
Doron Peled
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.
|
|
30 Apil 2015, 12:45 EDT:
Multi-Representational Security Analysis
by
Eunsuk Kang
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.
|
|
30 Apil 2015, 2:00 EDT:
Secure State Estimation For Cyber Physical Systems Under Sensor Attacks:
A Satisfiability Modulo Theory Approach
by
Yasser Shoukry Sakr
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.
|
|
29 Apil 2015:
Program Synthesis for Data Manipulation
by
Gustavo Soares
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.
|
|
24 Apil 2015:
Dynamic Analysis of Cyber-Physical Systems
by
Parasara Sridhar Duggirala
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.
|
|
13 April 2015:
Inductive Functional Programming
by
Ute Schmid
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).
|
|
2 March 2015:
From Reachability to Temporal Specifications in Game Theory
by
Orna Kupferman
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.
|
|
2 Feb 2015:
Parameterized Synthesis
by
Roderick Bloem
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.
|
|
5 Jan 2015:
Standing on the Shoulders of a Giant:
One Person’s Experience of Turing’s Impact
by David Harel
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.
|
|
1 Dec 2014:
Solving Horn Constraints for Program Verification and Synthesis
by Andrey Rybalchenko
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.
|
|
3 Nov 2014:
Software Synthesis using Automated Reasoning
by Ruzica Piskac
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.
|
|
15 Oct 2014:
On-Demand Printable Robots
by
Ankur Mehta
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.
|
|
5 May 2014:
Automated Program Synthesis at Kestrel Institute
by
Cordell Green and
Doug Smith
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.
|
|
7 April 2014:
Synthesis of Network Updates
by
Pavol Cerny
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.
|
|
3 Mar 2014:
The Satisfiability Revolution and the Rise of SMT
by
Clark Barrett
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.
|
|
3 Feb 2014:
Synthesis of Event Insertion Functions for Enforcement of Opacity Security Properties
by
Stephane Lafortune
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.
|
|
6 Jan 2014:
Engineering Domain-specific Languages with Formula 2.0
by
Ethan Jackson
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.
|
|
4 Nov 2013:
Generealized Synchronization Trees
by
Rance Cleaveland
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.
|
|
7 Oct 2013:
Increasing programmer productivity for building reliable programs using annotations and tactic synthesis
by
Madhusudan Parthasarathy
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.
|
|
9 Sep 2013:
Syntax Guided Synthesis
by
Rajeev Alur
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.
|
|
18 Jul 2013:
Rational Synthesis
by
Dana Fisman
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.
|
|
13 May 2013:
Platform-Based Software Synthesis and Verification Using Contracts
by
Alberto Sangiovanni-Vincetelli
slides
|
|
1 Apr 2013:
Synthesis for Concurrency
by
Martin Vechev
slides
|
|
4 Mar 2013:
Program Synthesis using Smoothed Numerical Search
by
Swarat Chaudhuri
slides
|
|
4 Feb 2013:
Synthesis and Robotics
by
Hadas Kress-Gazit
slides
|
|
14 Jan 2013:
Synthesis for Education
by
Sumit Gulwani
talk
|
|
3 Dec 2012:
Synthesizing Robust Systems
by
Paulo Tabuada
slides
|
|
5 Nov 2012:
Integrating Induction, Deduction and Structure for Synthesis
by
Sanjit A. Seshia
slides
|
|
1 Oct 2012:
Compositional Temporal Synthesis
by
Moshe Vardi
slides
|
|
10 Sep 2012:
Sketch Tutorial
by
Armando Solar-Lezama
slides
|