RiSE Seminar

We aim to enrich the specifications of finite state systems with quantitativeaspects. Specifically, we consider systems (Kripke structures) with numericvariables, and look for a suitable specification language in the form ofa temporal-logic over the accumulative sum and average of the variables. Anexample for such a specification is Always( Sum(energy) > 0 or Sum(money)> 0 ) and Eventually-Always( Average(Revenue) > 1,000,000 ). As a first stage,we examine the expressiveness limits that still allow for a decidablemodel-checking procedure. In the talk, I plan to explain our research directionand the results we have so far. This is a joint work with KrishnenduChatterjee, Thomas Henzinger and Orna Kupferman.

Given a probabilistic system M, i.e. a model withprobabilistic transitions, one may be interested to knowwhether execution paths on M satisfy a given property\phi. When the model is totally observable and \phi isomega-regular, the question can be answered using LinearProgramming or Iteration methods.

We focus on the context of partially observed models, theextreme casebeing the model of Probabilistic Automata: the observerhas no feedback on the current state of an executionpath. Most interesting problems become undecidable, thisis the case for instance for the positive Buchi problem:

Given a probabilistic Automata, is there an input wordsuch that with positive probability the associated pathssatisfy a given Buchi condition?

After an preliminary introduction of the probabilisticmodels of Markov Decision Processes and ProbabilisticAutomata, and an overview of the decidability resultsknown so far, we will present the notion of ``simpleprocesses'', which allows the definition of probabilisticmodels on which the verification of general omega-regularproperties is decidable. The notion of simple process isinspired by works on the structure of the tail sigma fieldof a non homogeneous Markov chain, and a DecompositionSeparation theorem which generalizes the partition of thestate space of a finite homogeneous Markov chain intoirreducible and transient components, to the context offinite non homogeneous Markov chains.

We describe Aligators, a tool for the generation of universally quantifiedarray invariants. Aligators leverages recurrence solving and algebraictechniques to carry out inductive reasoning over array content. The Aligatorsloop extraction module allows treatment of multi-path loops by exploiting theircommutativity and serializability properties. Our experience in applyingAligators on a collection of loops from open source software projects indicatesthe applicability of recurrence and algebraic solving techniques for reasoningabout arrays.

This is a joint work with T. Henzinger, T. Hottelier and A. Rybalchenko.

For Very Large Scale Integrated (VLSI) Circuits intended to be used inhighly reliable applications, formal specification and analysis ismandatory. Two trends in VLSI design favour a modeling approachanalogous to that used for distributed systems: (i) noticeablecommunication delays between circuit components and (ii) increasingfailure rates caused by wear-out and particle hits in circuits withever decreasing feature sizes. Despite these striking similarities,specifying and analyzing circuits by means of classic distributedsystem models is either overly lengthy or not possible. To overcomethese limitations a new modeling and analysis framework tied to thepeculiarities of fault-tolerant on-chip algorithms ispresented.

The capabilities of this framework are then illustrated by applying it(i) to analyze and prove correct a fault-tolerant on-chip tickgeneration algorithm and (ii) to prove the impossibility of solvingthe short-pulse filter problem with purely digital and statelessmodules only.

In the clock synchronization problem, on seeks to keepdevices in a communication network as closely synchronized as possiblein face of drifting clocks and unknown message transmission times. Thisand similar tasks have been research topic for several decades now,both in theory and practice. So, what is different about this talk? Weask not only for the maximum worst-case clock skew between any twonodes in the system to be minimal, but also for devices which canestimate each other's clock values accurately to be synchronizedtightly. For many applications, the latter property is crucial, as theymerely require that devices capable of direct communication arewell-synchronized. Moreover, we allow for arbitrary network dynamics,i.e., communication links may fail and become operative again atarbitrary times. Interestingly, this challenging task can be optimallysolved by a stunningly simple algorithm.

The talk will comprise two parts. First, we present the problem and ourresults to a general audience. In the second, more technical part, wetry to shed light on the techniques by which we obtain ourasymptotically optimal bounds.

Short Bio: Christoph Lenzen studied mathematics at the university ofBonn and received his diploma degree in October 2007. Currently he isPh.D. student in the Distributed Computing Group at ETH Zurich and isgoing to graduate in December. His research topics cover distributedgraph algorithms, clock synchronization, and load balancing algorithms.The line of work on gradient clock synchronization has beenparticularly successful, with publications at FOCS, PODC, and in JACM,as well as the best paper award at PODC 2009.

Notions of specification, implementation, satisfaction, and refinement,together with operators supporting stepwise design, constitute aspecification theory. We construct such a theory for Markov Chains(MCs) employing a new abstraction: Constraint Markov Chains.Constraint MCs permit rich constraints on probability distributions and thusgeneralize prior abstractions such as Interval MCs. Linear (polynomial)constraints suffice for closure under conjunction (respectively parallelcomposition). This is the first specification theory for MCs with suchclosure properties. Despite the generality, all operators and relationsare computable.

In this talk I will first introduce the notion ofhigher-order recursion schemes and give the tightconnection that exists with automata theory. In thiswork, we use schemes as a way to produce an infinitetree: with any schemes one associate a (unique) infinitetree. A paper by Luke Ong [LICS'06] establishes that anytree generated in such a way has a decidable second ordertheory.

We present here a stronger result, namely that given a tree tdescribed by a scheme and an MSO formula phi, the treet_phi, obtained by marking thos nodes in t where phiholds, can be (effectively) generated by a scheme. Acorollary of this result is that the trees generated byschemes are closed by successive application of an MSOinterpretation followed by unfolding.

The talk will be based on the following papers:

• Arnaud Carayol, Matthew Hague, Antoine Meyer, Luke Onget Olivier Serre. Winning regions of higher-orderpushdown games, in Proceedings of the Twenty-Third AnnualIEEE Symposium on Logic in Computer Science, LICS 2008,IEEE Computer Society, pp.193-204, 2008.
• Matthew Hague, Andrzej Murawski, Luke Ong et OlivierSerre. Collapsible Pushdown Automata and RecursionSchemes, in Proceedings of the Twenty-Third Annual IEEESymposium on Logic in Computer Science, LICS 2008, IEEEComputer Society, pp.452-461, 2008.
• Christopher Broadbent, Arnaud Carayol, Luke Ong etOlivier Serre. Recursion Schemes and Logical Reflection,in Proceedings of the Thwenty-fifth Annual IEEE Symposiumon Logic in Computer Science, LICS 2010, IEEE ComputerSociety, pp. 120-129, 2010.

(Very) Short Bio:

Olivier Serre is a full-time researcher employed by CNRSin LIAFA (University Paris 7 & CNRS) since October2005. He is also a part-time assistant professor at EcolePolytechnique. Previously he did a PhD (2001-2004) underthe direction of Anca Muscholl and Jean-Eric Pin. Hismain research interests are games in computer science,automata theory, infinite states system and logic.

I will present an inverse method allowing to synthesizeconstraints on timing delays (seen as parameters) in theframework of timed automata.Given a reference valuation of the parameters, this method synthesizesa constraint on the parameters, guaranteeing the sametime-abstract linear behavior as for the referencevaluation.This is useful for safely relaxing some values of the referencevaluation and gives a criterion of robustness to the system.In particular, LTL formulae are preserved.By iterating this inverse method on various points of a boundedparameter domain, we are then able to partition theparametric space into good and bad zones, with respect to agiven property one wants to verify.A tool, IMITATOR, was developed and was successfully applied tovarious examples of asynchronous circuits and protocols.An extension to probabilistic timed systems allows to synthesize aconstraint on the timing parameters guarantying the value ofthe reachability probabilities.

A control system consists of two subsystems: the controllerand the "plant" (controlled system).In an endless loop the controller measures outputs from and sends commands to theplant in order to drive it towards a given goal region.We focus on software based control systems,that is, systems where the the controllerconsists of software running on a microprocessorand measures from the plant are quantized (AD conversion)before being sent to the control software.

System requirements for control systemsare typically given as specifications for the closed loop system,that is the system consisting ofthe plant and the (to be designed) controller.

Typically, Control engineering techniques are usedto design the control law(i.e. the functional specifications for the control software)from the closed loop system requirements.Software engineering techniques are then used todesign the control software implementing the given controllaw.

Such an approach leaves open many questions about the correctnessof the control software with respect to the closed loop system requirementsand motivates investigation on methods and tools for automatic synthesis ofcorrect-by-construction control software from closed loopsystem requirements.

We present an algorithm that given a Discrete Time Linear Hybrid System(DTLHS) model for the plant P returns acorrect-by-construction software implementation Kfor a (near time optimal)robust Quantized Feedback Controllerfor P along witha suitable representation forthe set of states on which Kis guaranteed to work correctly (controllable region).Furthermore, K has a Worst Case Execution Time(WCET)guaranteed to belinear in the number of bits of the quantization schema.

We implemented our algorithm on top of the CUDD OBDD packageand of the GLPK MILP solver and present results on using such an implementation to synthesize Ccontrollers for the buck DC-DC converter,a widely used mixed-mode analog circuit.Our experimental results show that our proposed approach is viable andthe performance of the automatically synthesized controllers compare wellwith those of controllers designed using ad-hoc approaches.

************

This talk is mainly based on our CAV2010 paper:
Federico Mari, Igor Melatti, Ivano Salvo, Enrico Tronci.
Synthesis of Quantized Feedback Control Software forDiscrete Time Linear Hybrid Systems.
Tayssir Touili, Byron Cook, Paul Jackson (Eds.):
Computer Aided Verification, 22nd International Conference,CAV 2010, Edinburgh, UK,
July 15-19, 2010. Proceedings. Lecture Notes in ComputerScience 6174 Springer 2010,
ISBN 978-3-642-14294-9 CiteSeerX

We introduce streaming data string transducers that mapinput data strings tooutput data strings in a single left-to-right pass inlinear time. Data strings are (unbounded) sequences ofdata values, tagged with symbols from a finite set, over apotentially infinite data domain that supports onlythe operations of equality and ordering. The transduceruses a finite set of states, a finite set of variablesranging over the data domain, and a finite set ofvariables ranging over data strings. At every step, it canmake decisions based on the next input symbol, updatingits state, remembering the input data value in its datavariables, and updating data-string variables byconcatenating data-string variables and new symbols formedfrom data variables, while avoiding duplication. Weestablish PSPACE bounds for the problems of checkingfunctional equivalence of two streaming transducers, andof checking whether a streaming transducer satisfiespre/post verification conditions specified by streamingacceptors over input/output data-strings.

We identify a class of imperative and a class offunctional programs, manipulating lists of data items,which can be effectively translated to streamingdata-string transducers. The imperative programsdynamically modify a singly-linked heap by changingnext-pointers of heap-nodes and by adding new nodes. Themain restriction specifies how the next-pointers can beused for traversal. We also identify an expressivelyequivalent fragment of functional programs that traverse alist using syntactically restricted recursive calls. Ourresults lead to algorithms for assertion checking and forchecking functional equivalence of two programs, writtenpossibly in different programming styles, for commonlyused routines such as insert, delete, and reverse.

Computer systems are routinely deployed in life- andmission- critical situations, yet in most cases theirsecurity, safety or dependability cannot be assured to thedegree warranted by the appli- cation. In other words,trusted computer systems are rarely really trustworthy.

We believe that this is highly unsatisfactory, and have embarked on alarge research program aimed at bringing reality in linewith expectations. In this talk describes NICTA�s researchagenda for achieving true trustworthiness in systems. Thefirst pahse has been concluded, with the world's firstformal proof of functional correctness of a complete OSmicrokernel. The second phase, in progress, aims at makingdependability guarantees for complete real-world systems,comprising millions of lines of code.

Bio:

Gernot Heiser holds the position of Scientia Professro andJohn Lions Chair of Operating Systems at theUniversity of New South Wales (UNSW), and leads the TrustworthyEmbedded Systems (ERTOS) group at NICTA, Australia'sNational Centre of Excellence for ICT Research. He joinedNICTA at its creation in 2002, and before that was afull-time member of academic staff at UNSW from 1991. Hispast work included the Mungi single-address-spaceoperating system, several un-broken records in IPCperformance, and the best-ever reported performance foruser-level device drivers.

In 2006, Gernot with a number of his students founded OpenKernel Labs, now the market leader in secureoperating-systems and virtualization technology for mobilewireless devices. The company's OKL4 operating system, adescendent of L4 kernels developed by his group at UNSWand NICTA, is deployed in more than a billion mobilephones. This includes the Motorola Evoke, the first (andto date only) mobile phone running a high-level OS (Linux)and a modem stack on the same processor core.

In a former life, Gernot developed semiconductor devicesimulators and models of device physics for suchsimulators, and pioneered the use of three-dimensionaldevice simulation for the characterisation andoptimisation of high-performance silicon solar cells.

Faulty device drivers are the leading source of reliability problems inmodern operating systems. Automatic device driver synthesis aims toaddress this problem by achieving driver correctness by construction.To this end, the driver implementation is generated automatically basedon a formal specification of the device and the interface between thedriver and the operating system.

In this talk I will give a high-level overview of the driver synthesismethodology, present a formalisation of the driver synthesis problem asa controller synthesis problem, and discuss the main challenges thatmust be addressed in order to turn driver synhtesis into a practicaltechnique capable of generating drivers for a wide range of devices.

In this talk, we will show how synchrony conditions can be added to theasynchronous distributed computing model in a way that avoids anyreference to message delays and computing step times, as well as anyglobal constraints on communication patterns and network topology. Morespecifically, we will introduce the Asynchronous Bounded-Cycle (ABC)model, where clock synchronization and lock-step rounds can easily beimplemented and proved correct, even in the presence of Byzantinefailures. Furthermore, we will describe some weaker variants of the ABCmodel that allow even more relaxed system assumptions. We will also seehow the ABC model relates to existing partially synchronous system models,in particular, to the Theta Model of Le Lann and Schmid, anddiscuss some aspects of the ABC model's applicability in real systems.

Automated verification of multi-threaded programs requiresexplicit identification of the interplay betweeninteracting threads, so called environment transitions, toenable scalable, compositional reasoning. Once theenvironment transitions are identified, we can proveprogram properties by considering each program thread inisolation, as the environment transitions keep track ofthe interleaving with other threads. Finding adequateenvironment transitions that are sufficiently precise toyield conclusive results and yet do not overwhelm theverifier with unnecessary details about the interleavingwith other threads is a major challenge.

In this talk, I will present a method for safetyverification of multi-threaded programs that applies(transition) predicate abstraction-based discovery ofenvironment transitions, exposing a minimal amount ofinformation about the thread interleaving. The crux of ourmethod is an abstraction refinement procedure that usesrecursion-free Horn clauses to declaratively stateabstraction refinement queries. Then, the queries areresolved by a corresponding constraint solvingalgorithm. We present preliminary experimental results formutual exclusion protocols and multi-threaded devicedrivers.

Software synthesis is a technique for automatically generating codegiven a specification. The goal of software synthesis is to make codingeasier while increasing both the productivity of the programmer and thecorrectness of the produced code. Code produced this way is correct byconstruction. However, due to the high computational cost ofsynthesizing code, this idea was not further explored until recently. We arewitnessing a regaining interest in software synthesis that is driven by theincreasing computational power. Today even desktop machines areable to construct code from complex input specifications.

In this talk I will present our new approach to synthesis that relies onthe use of automated reasoning and decision procedures. We handlecomplex specifications by employing efficient algorithms for reasoningabout the domain of the specification. I will describe how togeneralize decision procedures into predictable and complete synthesisprocedures. Here completeness means that the procedure is guaranteed tofind code that satisfies the given specification. Moreover, thesynthesis procedure also outputs preconditions on input values thatguarantee the existence of the output values. As an example, I willexplain how to transform a decision procedure for lineararithmetic into such a synthesis procedure.

I will also outline a synthesis procedure for specifications given inthe form of type constraints. The procedure takes into accountpolymorphic type constraints as well as code behavior and derives codesnippets that use given library functions. We use a first-orderresolution-based theorem prover to solve these constraints and derivecode snippets. The constraints can have multiple solutions and hence thetheorem prover may produce more than one code snippet. Therefore, we usean additional weight function to rank the derived snippets.

These procedures are implemented as extensions to the Scala compiler andI will include a demo in my talk.

We consider game models for the design of reactive systems working in resource-constrained environments. In mean-payoff games, the resource usage is computed as the long-run average resource level. In energy games, the resource usage is the initial amount of resource necessary to maintain the resource level positive. The resource can be memory, battery, or network usage for example.

While mean-payoff games are a well-established model in game theory and computer science, energy games have received attention only recently.The talk reviews recent results about these games and their relationship.Although they differ very basically in their definition, it is known that energy and mean-payoff games are equivalent forthe simple decision problem of existence of a winning strategy.This observation provides new complexity results for solvingmean-payoff games, and new insights for mean-payoff games combinedwith other conditions such as fairness, imperfect information, or multi-resource systems, though the strong equivalence with energy games usually breaks in such cases.

Reasoning with very large theories expressed in first-order logic canstrongly benefit from a good selection method for relevant axioms.This is confirmed by the fact that the largest available first-orderknowledge base (the Open CYC) contains over 3 million axioms, whileanswering queries to it usually requires not more than a few dozenaxioms.

A method for axiom selection has been proposed in the Sumo INferenceEngine (SInE) system. SInE has won the large theory division of CASCin 2008. The method turned out to be so successful that the next twoyears it was used by the winner of this division, as well as byseveral other competing systems. In this talk we will present thealgorithm and show experimental results based on its implementation inthe Vampire theorem prover.

My talk is intending to encourage research in what I call "physical algorithms". The area of physical algorithms deals with networked systemsof active agents. These agents have access to limited information forvarying reasons; examples are communication constraints, evolving topologies, various types of faults and dynamics. The networked systems we envision include traditional computer networks, but also more generally networked systems, such as social networks, highly dynamic and mobile networks, e.g. networks of entities such as cars or ants. In my talk I will present a few examples from the theory branch of my research group. I should mention that the talk is an updated version of my recent ICALP invited talk.

Systems code is ubiquitous and complex. Moreover, the complexity ofcode is expected to increase as systems designers can no longer expect increasing processor speeds, and thus must turn to concurrency for improved performance. How can we be sure that these programs, running on platforms ranging from human implant devices to nuclear power plant controls, will behave as intended? Addressing systems code correctness in the face of concurrency involves advances in two intertwined fields: automatic software verification and concurrent programming paradigms.

In this talk I will discuss some of our recent work on improving both the correctness as well as the performance of systems software. I will focus primarily on describing a new automatic method of temporal logic verification of programs (POPL'11, CAV'11). I will also discuss recent results on a new language feature that has enabled more concurrency in transactional memory systems, improving performance by an order of magnitude (POPL'10, PPoPP'08, SPAA'08).

Bio:Eric Koskinen's research is centered around developing mathematical techniques which improve the safety and performance of software, and applying those techniques to realistic computer systems. He is currently a PhD candidate at the University of Cambridge, under the supervision of Dr. Byron Cook and Prof. Michael Gordon. Eric was awarded the Gates Cambridge Scholarship, completed an Sc.M from Brown University where he worked with Maurice Herlihy, interned thrice at Microsoft Research, and previously spent three years as a software engineer at Amazon.com.

Even the most advanced reverse engineering techniques and products are weak in recovering data structures in stripped binaries - binaries without symbol tables. Unfortunately, forensics and reverse engineering without data structures is exceedingly hard. In this talk, I will present a new solution, known as Howard, to extract data structures from C binaries without any need for symbol tables. Our results are significantly more accurate than those of previous methods - sufficiently so to allow us to generate our own (partial) symbol tables without access to source code. Thus, debugging such binaries becomes feasible and reverse engineering becomes simpler. Also, we show that we can protect existing binaries from popular memory corruption attacks, without access to source code. Unlike most existing tools, our system uses dynamic analysis (on a QEMU-based emulator) and detects data structures by tracking how a program uses memory.

Despite acknowledged success of model checking, its application faces several problems generally inherent to the approach. In this talk we address such problems as parameterized model checking and combinatorial state explosion.

The uniform verification problem is to prove that a temporal property is satisfied on every instance of a system composed of an arbitrary number of homogeneous processes. We extend the network invariants technique by introducing three simulation relations on labelled transition systems (LTSs) that capture correspondence between paths of two systems with different number of processes. This allows us to apply the technique to parameterized families of LTSs generated by a network grammar in the asynchronous setting.

Using this extension we implemented CheAPS, the checker of asynchronous parameterized systems. The tool iteratively generates candidate invariants of a parameterized family and then it checks invariance property by constructing a semi-block simulation on a few finite LTSs. As soon as required invariant LTSs are found, these are passed to Spin for finite-state model checking.

Our tool, like many others, suffers from the state explosion effect. This observation and a case study of Generic Attribute Registration Protocol brought us to the investigation of symmetry reduction techniques. One recent method in this field, which allows one to check safety properties is lazy symmetry reduction. It copes with partially symmetric systems by refining abstract state space on-the-fly, where abstraction is built w.r.t. symmetry preserving constraints.

We found that the spirit of the original search algorithm is close to the well-known nested depth first search. This enables integration of lazy symmetry reduction into the algorithm of checking a linear temporal logic formula against a finite-state LTS. However, a great care should be taken when performing lasso detection on the abstract state space. To this end we introduced special notions of pseudo-cycles and feasibility conditions that provided us with the basis for proving soundness and completeness of the new algorithm.

The next bold step is the implementation of the algorithm in Spin. As it is heavily optimized for a specific set of techniques, embedding a new one in this tool is a technical challenge. We believe that in general implementation is close to completion, though its experimental evaluation is still in progress.

Usual techniques in abstract interpretation apply "join" operations when control flows from several nodes. Unfortunately, these techniques introduce imprecision, resulting in not being able to prove desired properties.

Modern SMT-solving techniques allow enumerating paths "on demand". We shall see how such path techniques may be combined with conventional polyhedral analysis, quantifier elimination, or with policy iteration, in order to obtain more precise invariants.

As online data sets grow over time, computations that process bulk data become increasingly more expensive. Furthermore, often the same computation runs on evolving data sets repeatedly, which implies that consecutive runs share a large fraction of their input. This motivates an incremental approach where results are incrementally updated as data evolves, instead of being recomputed from scratch. To achieve this, new systems for incremental bulk data processing have been proposed, such as Google's Percolator or Yahoo!'s CBP. However, using these systems comes at a price of losing compatibility with the interface offered by systems like MapReduce, and more importantly, requiring the programmer to implement application-specific dynamic algorithms, which the literature shows to be difficult to develop and implement even for simple problems.

In this talk I will describe the architecture, implementation, and evaluation of incoop, a generic MapReduce framework for incremental computations. incoop detects changes to the inputs to computations and enables the automatic update of the outputs by employing an efficient, fine-grained propagation mechanism. By integrating the proposed approach into the MapReduce framework, we transparently benefit a large class of existing applications. Furthermore, by adopting principles from algorithms and programming languages research, we are able to systematically identify the shortcomings of an initial, task memoization-based approach, and address them using several novel techniques such as a new storage system to store the input of consecutive runs, a new contraction phase that make the incremental computation of the reduce tasks more efficient, and a new scheduling algorithm for Hadoop that is aware of the location of previously computed results.

Computing bounds on the resource usage of a program often requires finding a symbolic worst-case bound on the number of visits to a given program location in terms of the inputs to that program; we call this the reachability-bound problem. The automatic computation of reachability-bounds is challenging because in general such bounds are complicated expressions that hinder the direct application of standard abstract domains and require disjunctive invariants.

We propose a two-step methodology for computing a reachability-bound of a given program location: First, we generate a transition system that disjunctively summarizes all pairs of states for which there is a program execution that visits the location once and again. Second, we compute a bound of the transition system to derive a reachability-bound. We present two approaches that implement this methodology.

Our first approach brings together an abstract-interpretation based iterative technique for computing disjunctive loop invariants and a non-iterative proof-rules based technique for loop bound computation.

Our second approach is based on the so-called size-change abstraction (SCA). We use a closure property of SCA for computing disjunctive loop invariants. We show that SCA offers a separation of concerns for bound computation: we extract local progress measures from small program parts, and then compose these local progress measures to a global bound. We state two program transformations that make imperative programs amenable to bound analysis with SCA.

Recent research in program synthesis has made it possible to effectively synthesize small programs in a variety of domains. In this talk, I will describe two useful applications of this technology that have thepotential to influence daily lives of billions of people. One application involves automating end-user programming using examples, which can allow non-programmers to effectively use computational devices such as cell-phones, computers (and in the future robots) to perform a variety of repetitive tasks. Another application involves building automated tutoring systems that can help students with problem solving in math and science domains.

Bio:Sumit Gulwani is a researcher in the RiSE group at Microsoft Research, Redmond. His primary research interest is in the area of program synthesis with applications to automating end user programming andbuilding automated tutoring systems. Sumit obtained his PhD in computer science from UC-Berkeley in 2005, and was awarded the C.V. Ramamoorthy Award and the ACM SIGPLAN Outstanding Doctoral Dissertation Award. He obtained his BTech in computer science and engineering from the Indian Institute of Technology (IIT) Kanpur in 2000 and was awarded the President's Gold Medal.

In this talk, we discuss the verification problem of parameterized concurrent programs. We propose a semi-compositional reasoning method for verifying safety properties of infinite-thread programs based on computing an over-approximation of the set of reachable states. Our approach is sound and terminating, even for infinite state programs (e.g. programs with recursion or unbounded integers). The essential idea of the technique is to reason about a program with many threads by considering only two thread abstractions at a time, and then combining information across all pairs of threads. Our algorithm consists of a feedback loop that combines techniques from abstract interpretation to compute numerical invariants with techniques from model checking to compute the effects of interference. We implemented our approach in a prototype tool and evaluated it on a selection of parameterized programs including Boolean programs generated by the SatAbs tool by performing predicate abstraction on Linux device drivers.

A simplicial complex is shellable if it can be constructed by gluing a sequence of n-simplexes to one another along (n-1)-faces only. Shellable complexes have been well-studied in combinatorial topology because they have many nice properties.

We show that many standard models of concurrent computation can be captured either as shellable complexes, or as the simple union of shellable complexes. We exploit their common shellability structure to derive new and remarkably succinct tight (or nearly so) lower bounds on connectivity of protocol complexes and hence on solutions to tasks such as k-set agreement.

This talk does not assume prior familiarity with Distributed Computing or Combinatorial Topology.

Joint work with Sergio Rajsbaum.

Programmable Logic Controllers (PLCs) are industrial control systems used as control devices in the automation industry and for monitoring of safety critical infrastructure. Since they are often used in safety critical environments, where a failure might have serious effects for human health or the environment, formal verification of their programs is advised. This huge strive for functional correctness combined with having small, well-structured programs, makes PLCs a very interesting platform for the application of formal methods.

In this talk, I will give a short introduction to PLCs and their programming modes. Then I will turn to the model checker [mc]square, which is developed at the Embedded Software Laboratory at the RWTH Aachen and allows for the verification of PLC programs. I will discuss current progress and obstacles and detail some of our techniques that make the verification of real world PLCs programs feasible.

We present a verification framework for analysing multiple quantitative objectives of systems that exhibit both nondeterministic and stochastic behaviour. These systems are modelled as MDPs, enriched with cost or reward structures that capture, for example, energy usage or performance metrics. Quantitative properties of these models are expressed in a specification language that incorporates probabilistic safety and liveness properties, expected total cost or reward, and supports multiple objectives of these types. We propose and implement an efficient verification framework for such properties and then present two distinct applications of it: firstly, controller synthesis subject to multiple quantitative objectives; and, secondly, quantitative compositional verification. The practical applicability of both approaches is illustrated with experimental results from several large case studies. The talk is joint work with with D. Parker, G. Norman, M. Kwiatkowska and H. Qu which, presented at TACAS 2011.

Binary executables are a promising analysis target in many scenarios, ranging from bug finding over execution time analysis to malware detection. Still, problems such as indirect control flow and the lack of types make it hard to adapt traditional static analysis tool-chains to binaries. While earlier attempts mostly use heuristics to preprocess binaries into a format understandable by static analyzers, we argue for the integration of disassembly, control flow reconstruction, and static analysis in a unified process. This enables sound static analysis of binaries, without fragile and generally unsound preprocessing by heuristic disassemblers.

The result of our work is the novel binary analysis tool Jakstab, which supports classic data flow analysis with domains such as intervals, but also path sensitive, bounded model checking style explicit analysis. Jakstab works directly on binaries and disassembles instructions on demand while exploring the program's state space. We demonstrate its practical usefulness in case studies on open and closed source Windows drivers and system tools. In ongoing work, we are extending our framework to support under-approximate information from execution traces to recover from unknown control flow due to imprecision of the analysis.

The DPLL algorithm for deciding propositional satisfiability is a fundamental algorithm with applications across computer science. The modern algorithm combines model search, deduction, and lemma generation in an elegant and highly efficient manner. An important question is whether the DPLL algorithm can be generalised to richer problems such as program verification.

In this talk I show that DPLL operates over a strict abstraction of propositional logic. This is surprising because it uses an imprecise abstraction to obtain precise results. I will show that DPLL very naturally fits in the framework of abstract interpretation. This view leads straight to a generalisation to programs. The application of this algorithm allows complex properties of non-linear programs to be proved automatically using very simple abstractions. Such proofs are well beyond the scope of significantly more mature tools using richer abstractions.

Software failures can be sorted into two groups: those that cause the software to do something wrong (e.g. crashing), and those that result in the software not doing something useful (e.g. hanging). In recent years automatic tools have been developed which use mathematical proof techniques to certify that software cannot crash. But, based on Alan Turing's proof of the halting problem's undecidablity, many have considered the dream of automatically proving the absence of hangs to be impossible. While not refuting Turing's original result, recent research now makes this dream a reality. This lecture will describe this recent work and its application to industrial software.

Bio: Dr. Byron Cook is a Principal Researcher at Microsoft Research in Cambridge, UK as well as Professor of Computer Science at Queen Mary, University of London. He is one of the developers of the Terminator program termination proving tool, as well as the SLAM software model checker.

The automata-based model checking approach for randomized distributed systems relies on an operational interleaving semantics of the system by means of a Markov decision process and a formalization of the desired event E by an !-regular linear-time property, e.g., an LTL formula. The task is then to compute the greatest lower bound for the probability for E that can be guaranteed even in worst-case scenarios. Such bounds can be computed by a combination of polynomially time-bounded graph algorithm with methods for solving linear programs. In the classical approach, the "worst-case" is determined when ranging over all schedulers that decide which action to perform next. In particular, all possible interleavings and resolutions of other nondeterministic choices in the system model are taken into account.

As in the nonprobabilistic case, the commutativity of independent concurrent actions can be used to avoid redundancies in the system model and to increase the efficiency of the quantitative analysis. However, there are certain phenomena that are specific for the probabilistic case and require additional conditions for the reduced model to ensure that the worst-case probabilities are preserved. Related to this observation is also the fact that the worst-case analysis that ranges over all schedulers is often too pessimistic and leads to extreme probability values that can be achieved only by schedulers that are unrealistic for parallel systems. This motivates the switch to more realistic classes of schedulers that respect the fact that the individual processes only have partial information about the global system states. Such classes of partial information schedulers yield more realistic worst-case probabilities, but computationally they are much harder. A wide range of verification problems turns out to be undecidable when the goal is to check that certain probability bounds hold under all partial-information schedulers.

Cardiac disorders such as tachycardia and fibrillation, are spatial-temporal behaviors of cardiac-cell networks, which correspond to the build-up and break-up of electrical spiral-waves, respectively, and which emerge in certain conditions. To understand and predict these conditions, mathematical models of cardiac cells (mostly differential equations models) have been constructed, which range from 4 to 67 variables and from 27 to 94 associated parameters. The main tool for the analysis of such models is simulation. In this talk I will address the challenges and opportunities associated with the techniques that go beyond simulation, such as model checking and parameter-range identification.

This lecture introduces a theory for the identification, modeling, and formalization of three complementary views onto software and software intensive systems called the problem view, thespecification view, and the solution view. The problem view addresses requirements engineering;the specification view describes the overall system functionality from the users' point of view aiming at the specification of the functional requirements of multi-functional systems in terms of their functions as well as their mutual dependencies. This view leads to a function or service hierarchy. The solution view essentially addresses the design phase to decompose systems into logical architectures formed by networks of interactive components specified by their interface behavior.

These views are closely related and are helpful for the structured modeling of multi-functional systems during their development. We show how the three complementary views work and fit together as major milestones in the early phases of software and systems development. We, in particular, base our approach on a purely logical version of the FOCUS theory for describing interface behavior and the structuring of systems into components. We give a theoretical treatment of all three views by extending the FOCUS model and its interface theory accordingly.

In the distributed balls-into-bins problem, one strives for distributing n balls into n bins as evenly as possible. In each communication round, balls may contact some bins, bins may respond, and balls may commit to a bin. Goals are to minimize the individual and overall message complexities, the maximum bin load, and the number of communication rounds.

Classical algorithms are non-adaptive, that is, each ball decides on the bins it will contact before communication commences. We will show how dropping this requirement drastically improves the trade-offs between the above optimization criterions. Concretely, we present a stunningly simple algorithm that guarantees a maximum bin load of two within log* n + O(1) rounds using O(n) total messages. This is provably optimal for a natural class of algorithms, while dropping any of the requirements of this class enables to achieve a constant running time. To round of the presentation, we discuss how our techniques can be applied to a basic communication task in a clique.

Bio:Christoph Lenzen received his diploma in Mathematics from the university of Bonn in 2007. He continued his studies at ETH Zurich in Roger Wattenhofer's group and received his Ph.D. degree in 2011. Presently he is a postdoc at the Hebrew University of Jerusalem with Danny Dolev. His main area of interest are distributed algorithms, for instance for graph problems such as dominating or independent sets, randomized load balancing, and clock synchronization.

Establishing liabilities in component-based systems is a challenging task, as it requires to establish convincing evidence with respect to occurrence of a failure, and the cae causality relation between the failure and a damage.The second issue is especially complex when several failures are detected and their impact on the occurrence of the damage has to be assessed. In this talk I will propose a formal framework for reasoning about logical causality between component failures and the violation of a system-level specification.

Bio:

This talk will introduce CompCertTSO, a fully-fledged certified compilerfrom a concurrent extension of a C-like language to x86 assembler thathas been programmed and proved correct in Coq, and will describe somesimple compiler optimisations for removing redundant memory fences in programs running on top of the x86-TSO relaxed memory model. While theoptimisations will be performed using standard thread-local control flowanalyses, their correctness is subtle and relies on a non-standard globalsimulation argument.

Bio:

Hard real-time systems are subject to stringent timing constraints, which are dictated by the surrounding physical environment. A schedulability analysis has to be performed in order to guarantee that all timing constraints will be met. Existing techniques for schedulability analysis require upper bounds for the execution times of all the system's tasks to be known. These upper bounds are commonly called worst-case execution times (WCETs). The WCET-determination problem has become non-trivial due to the advent of processor features such as caches, pipelines, and all kinds of speculation, which make the execution time of an individual instruction locally unpredictable. Such execution times may vary between a few cycles and several hundred cycles.A combination of Abstract Interpretation (AI) with Integer Linear Programming (ILP) has been successfully used to determine precise upper bounds on the execution times of real-time programs. The task solved by abstract interpretation is to compute invariants about the processor's execution states at all program points. These invariants describe the contents of caches, of the pipeline, of prediction units etc. They allow to verify local safety properties, safety properties who correspond to the absence of "timing accidents". Timing accidents, e.g. cache misses, pipeline stalls are reasons for the increase of the execution time of an individual instruction in an execution state.The technology and tools have been used in the certification of several time-critical subsystems of the Airbus A380. The AbsInt tool, aiT, is the only tool worldwide, validated for these avionics applications.I will give an introduction to our timing-analysis method, present results about the predictability of cache architectures, and give an overview of current work and open problems.

Bio:
Prof. Reinhard Wilhelm is a full Professor of Computer Science at the Saarland University, Saarbruecken and the Scientific Director of the International Conference and Research Center for Computer Science, Schloss Dagstuhl, Germany. He is the cofounder of AbsInt, a company developing software tools for embedded systems.The research activities of Prof. Reinhard Wilhelm cover a wide range of topics, including compiler generation, program analysis, and software visualisation. His contributions to research have been honored by several awards and prizes. To name a few, Prof. Wilhelm is an ACM Fellow, and he received the European IST Prize with the spin-off company AbsInt, the Alwin Walther Medal, the Konrad-Zuse Medal and the ACM Distinguished Service Award.

We present a construction for turning games with imperfect information into games with perfect information by preserving winning strategies. The generic construction yields an infinite game tree. For games with observable objectives, we define an abstraction method that yields finite, and thus decidable, instances in some relevant cases and furthermore provides a semi-decision procedure for solving distributed games. The talk is on joint work with Lukasz Kaiser and Bernd Puchala forthcoming at FSTTCS 2011.

It is notoriously difficult to make distributed systems reliable. Thisbecomes even harder in the case of the widely-deployed systems thatare heterogeneous (multiple implementations) and federated (multipleadministrative entities). The set of routers in charge of theInternet's inter-domain routing is a prime example of such a system.
We argue that a key step in making these systems reliable is the needto automatically explore the system behavior to check for potentialfaults. In this talk, I will describe the design and implementationof DiCE, a system for online testing of heterogeneous and federateddistributed systems. DiCE runs concurrently with the production systemby leveraging distributed checkpoints and isolated communicationchannels. DiCE orchestrates the exploration of relevant system statesby controlling the inputs that drive system actions. While respectingprivacy among different administrative entities, DiCE detects faultsby checking for violations of properties that capture the desiredsystem behavior. We demonstrate the ease of integrating DiCE with aBGP router and a DNS server, the building blocks of two vital servicesin the Internet. Our evaluation in the testbed shows that DiCE quicklyand successfully detects three important classes of faults, resultingfrom configuration mistakes, policy conflicts and programming errors.
Joint work with Marco Canini, Vojin Jovanovic, Daniele Venzano, GautamKumar, Dejan Novakovic, Boris Spasojevic, and Olivier Crameri

Bio:

In this talk I will give an introduction and present some of my recentresults in to two of the most fundamental problems in algorithmic gametheory and mechanism design: the problem of designing truthfulauctions for selling multiple items and of scheduling unrelatedmachines to minimize the makespan.
In the problem of designing truthful auctions we want to auctionmultiple items together. There might also exist budget and demandconstraints. In the problem of scheduling unrelated machines we assumethat the machines behave like selfish players: they have to get paidin order to process the tasks, and would lie about their processingtimes if they could increase their utility in this way.

Recently, it has been shown how block-wise transferfunctions for linear template constraints can be derivedfor programs defined over piece-wise linear arithmetic.Quantifier elimination is then applied to find a directrelationship between the inputs and the outputs of a block.We extend this work towards bit-vector programs, i.e.programs whose semantics is defined over finite-precisionintegers, by operating in the computational domain ofpropositional Boolean formulae. The drawback of this methodis that it relies on existential quantification, whichinduces a computational bottleneck. To sidestep thiscomplexity, we present a novel method for computing transferfunctions that does not depend on quantifier elimination atall, but uses incremental SAT solving instead.

Bio:

We present a coverage metric targeted at shared memory concurrent programs: the Location Pairs (LP) coverage metric. The goals of this metric are (i) to measure how thoroughly a program has been tested from a concurrency standpoint, i.e., whether enough qualitatively different thread interleavings have been explored, and (ii) to guide testing towards unexplored concurrency scenarios. This metric was inspired by an access pattern known to lead to high-level concurrency errors. We built a tool for measuring LP coverage and used the LP metric for interactive debugging. We also compared LP coverage with other concurrency coverage metrics on Java benchmarks. Using mutations and manually-inserted bugs, we demonstrated that LP coverage corresponds better to concurrency errors, is a better measure of how well a program is exercised concurrency-wise by a test set, reaches saturation later than other coverage metrics, and is viable and useful as an interactive testing and debugging tool.

Bio:
Serdar Tasiran received his BS in Electrical Engineering from Bilkent University in 1991, and his MS and PhD from UC Berkeley in Electrical Engineering and Computer Sciences in 1995 and 1998, respectively. He was a researcher at the Gigascale Systems Research Center, a multi-university, multi-company consortium until 2000. From 2000 to 2003, he was a research scientist at the Systems Research Center (part of DEC, Compaq and later HP Labs) in Palo Alto, CA. Since 2003, he has been at Koc University, Istanbul, Turkey. While at Koc University, he has had visiting appointments at MIT, EPFL, Microsoft Research, USA and India. His research interests are the specification, verification, performance estimation and optimization of concurrent systems.

Automata theory in the 1960s gave a method to prove that certain logical theoriesare decidable. Implicit in this work is the notion of an automatic structure. I will present essential properties of automatic structures, give concrete examples, and mention some foundational problems that are still open. Basic familiarity with logic and automata areenough to follow this talk.

Bio:

We consider verification of programs manipulating dynamic linked data structures such as various forms of singly and doubly-linked lists or trees. We consider important properties for this kind of systems like no null-pointer dereferences, absence of garbage, shape properties, etc.In the first part of the talk, we present a verification method based on a novel use of tree automata to represent heap configurations. A heap is split into several ``separated'' parts such that each of them can be represented by a tree automaton. The automata can refer to each other allowing the different parts of the heaps to mutually refer to their boundaries. Moreover, we allow for a hierarchical representation of heaps by allowing alphabets of the tree automata to contain other, nested tree automata. Program instructions can easily be encoded as operations on our representation structure. This allows verification of programs based on a symbolic state-space exploration together with refinable abstraction within the so-called abstract regular tree model checking.In the second part of the talk, a new separation-logic-based tool called Predator will briefly be presented. The tool is specifically tuned to handle various kinds of linked lists in the low-level form used in system software.(Forester is a joint work with Peter Habermehl from LIAFA, Paris, Lukas Holik and Adam Rogalewicz from FIT, Brno University of Technology, and Jiri Simacek from FIT BUT and VERIMAG, Grenoble. Predator is a joint work with Kamil Dudka and Petr Peringer from FIT BUT.)

Bio:

In this talk I will present results on the problem of scheduling tasksfor execution by a processor when the tasks can stochasticallygenerate new tasks. Tasks can be of different types, and each type hasa fixed, known probability of generating d tasks for each number d. Weare interested in the random variables modeling the time and spaceneeded to completely execute a task T, that is, to empty the pool ofunprocessed tasks assuming that initially the pool only contains thetask T. We derive tail bounds for the distributions of these variablesfor various classes of schedulers. We also provide bounds on theexpected values of these variables.

There are many web applications that require users to coordinate and communicate. Friends want to coordinate travel plans, students want to jointly enroll in the same set of courses, and busy professionals want to coordinate their schedules. These tasks are difficult to program using existing abstractions provided by database systems since they all require some type of coordination between users. However, this type of information flow is fundamentally incompatible with classical isolation in database transactions. In this talk, I will argue that it is time to look beyond isolation towards principled and elegant abstractions that allow for communication and coordination between some notion of (suitably generalized) transactions. This new area of declarative data-driven coordination is motivated by many novel applications and is full of challenging research problems. This talk describes joint work with Gabriel Bender, Nitin Gupta, Christoph Koch, Lucja Kot, Milos Nikolic, and Sudip Roy.

Bio:
Johannes Gehrke is a Professor in the Department of Computer Science at Cornell University. Johannes' research interests are in the areas of database systems, data mining, data privacy, and applications of database and data mining technology to marketing and the sciences. Johannes has received a National Science Foundation Career Award, an Arthur P. Sloan Fellowship, an IBM Faculty Award, the Cornell College of Engineering James and Mary Tien Excellence in Teaching Award, the Cornell University Provost's Award for Distinguished Scholarship, a Humboldt Research Award from the Alexander von Humboldt Foundation, and the 2011 IEEE Computer Society Technical Achievement Award. He is the author of numerous publications on data mining and database systems, and he co-authored the undergraduate textbook Database Management Systems (McGrawHill (2002), currently in its third edition), used at universities all over the world. Johannes is also an Adjunct Faculty Member at the University of Tromso in Norway. Johannes was co-Chair of the 2003 ACM SIGKDD Cup, Program co-Chair of the 2004 ACM International Conference on Knowledge Discovery and Data Mining (KDD 2004), Program Chair of the 33rd International Conference on Very Large Data Bases (VLDB 2007), and Program co-Chair of the 28th IEEE International Conference on Data Engineering (ICDE 2012). From 2007 to 2008, he was Chief Scientist at FAST, A Microsoft Subsidiary.

Applications in many different areas of computer science are required to make discrete decisions under uncertainty. Under uncertainty, the individual decisions made by a program are inevitably nondeterministic. A serious implication of this is that the decisions made by the program at different points of an execution may not even be consistent with each other. As a result, a program that is otherwise correct may execute along paths that would not be executed {\em on any input} in the program's usual semantics, and violate essential program invariants on the way.The property of em robustness asserts that a decision-making program does not suffer from the above kind of violations. In this paper, we present a program analysis to verify that a program P is robust in this sense. Our analysis constructs a decision monitor that observes the decisions made along executions of P and derives every corollary of these decisions. The problem of proving P robust is reduced to assertion checking in the product of P and this monitor.We apply our analysis to the domain of geometric computations, where typical programs make boolean decisions in the presence of numerical uncertainty. Robustness is known to be a critical and frequently-violated correctness property in this domain---for example, violation of robustness can cause everyday algorithms for computing convex hulls or triangulations to crash, go into infinite loops, or violate essential postconditions. While there is alarge body of work on robust geometric computation, ours is the first attempt at static verification of robustness of geometric programs. An evaluation using a suite of well-known geometric algorithms demonstrates the utility of our method.

In a process algebra with hiding and recursion it is possible to createprocesses which compute internally without ever communicating with theirenvironment. Such processes are said to diverge or livelock. We show howit is possible to conservatively classify processes as livelock-freethrough a static analysis of their syntax. In particular, we present acollection of rules, based on the inductive structure of terms, whichguarantee livelock-freedom of the denoted process. This gives rise to analgorithm which conservatively fl ags processes that can potentiallylivelock. We illustrate our approach by applying both BDD-based andSAT-based implementations of our algorithm to a range of benchmarks, andshow that our technique in general substantially outperforms the modelchecker FDR whilst exhibiting a low rate of inconclusive results.
Joint work with Joel Ouaknine, James Worrell and A. W. Roscoe.

The talk surveys recent results about infinite-state Markov chains and stochastic games generated by automata with one or more counters. Special attention will be devoted to stochastic one-counter automata and their basic properties such as termination probability or expected termination time. We also present some fresh (unpublished) results about one-counter Markov decision processes and non-stochastic games with multiple counters.

Interpolation is an important technique in verification and static analysis of programs. In particular, interpolants extracted from proofs of various properties are used in invariant generation and bounded model checking. A number of recent papers studies interpolation in various theories and also extraction of smaller interpolants from proofs. In particular, there are several algorithms for extracting of interpolants from so-called local proofs.

In this talk we describe a technique of minimising interpolants based on transformations of what we call the "grey area" of local proofs. We also present how to translate arbitrary proofs, under certain common conditions, into local ones.

Unlike many other interpolation techniques, our technique is very general and applies to arbitrary theories. Our approach is implemented in the theorem prover Vampire and evaluated on a large number of benchmarks coming from first-order theorem proving and bounded model checking using logic with equality, uninterpreted functions and linear arithmetic. Our experiments demonstrate the power of the new techniques: for example, it is not unusual that our proof transformation gives more than a tenfold reduction in the size of interpolants.

This is a joint work with Krystof Hoder and Andrei Voronkov (The University of Manchester).

The decade of genomic revolution following the human genome's sequencing has produced significant medical advances, and yet again, revealed how complicated human biology is, and how much more remains to be understood. Biology is an extraordinary complicated puzzle; we may know some of its pieces but have no clue how they are assembled to orchestrate the symphony of life, which renders the comprehension and analysis of living systems a major challenge. Recent efforts to create executable models of complex biological phenomena - an approach we call Executable Biology - entail great promise for new scientific discoveries, shading new light on the puzzle of life. At the same time, this new wave of the future forces computer science to stretch far and beyond, and in ways never considered before, in order to deal with the enormous complexity observed in biology. This talk will focus on our recent success stories in using formal methods to model cell fate decisions during development and cancer, and on going efforts to develop dedicated tools for biologists to model cellular processes in a visual-friendly way.

Human ventricular cells have currently more then ten increasingly detailed differential equations models (DEM), ranging from four variables and 27 parameters to more than 90 variables and hundreds of parameters. The detailed DEMs encapsulate the most up-to-date knowledge about the ionic processes involved at the intra and inter cellular level. While their differential equations are relatively simple (often of the law of mass action type) the sheer number of variables and parameters they contain, makes their analysis and even realistic 3D simulation intractable. It is therefore necessary, to map such DEMs to reduced order DEMs, whose analysis is still tractable. Our preliminary work shows that achieving such a map is possible: one uses simplifying assumptions to systematically eliminate variables whose behavior is not observable in the property of interest. For example, one can reduce the number of variables of the most up-to-date description of the sodium channel by assuming that its subunits are independent (Hodgkin-Huxley assumption) and by observing the overall open-close probability of the channel only.

Even with impressive advances in automated formal methods, certain problems in system verification and synthesis remain challenging. Examples include the verification of quantitative properties of software involving constraints on timing and energy consumption, and the automatic synthesis of systems from specifications. The challenges mainly arise from three sources: environment modeling, incompleteness in specifications, and the complexity of underlying decision problems.

In this talk, I will present SCIDUCTION, a methodology to tackle these challenges. Sciduction combines inductive inference (learning from examples), deductive reasoning (such as SAT/SMT solving), and structure hypotheses. We have demonstrated several applications of sciduction including timing analysis of embedded software, synthesis of loop-free programs, synthesis from temporal logic (LTL), term-level verification of hardware (RTL) designs, and switching logic synthesis of hybrid systems. This talk will present some core theory, a couple of illustrative applications, and directions for future work.

Biography: Sanjit A. Seshia is an Associate Professor in the Department of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He received an M.S. and Ph.D. in Computer Science from Carnegie Mellon University, and a B.Tech. in Computer Science and Engineering from the Indian Institute of Technology, Bombay. His research interests are in dependable computing and computational logic, with a current focus on applying automated formal methods to problems in embedded systems, electronic design automation, computer security, and program analysis. His work on the UCLID verifier and decision procedure helped pioneer the area of satisfiability modulo theories (SMT) and SMT-based verification. He is co-author of a textbook on embedded systems. He has received a Presidential Early Career Award for Scientists and Engineers (PECASE), an Alfred P. Sloan Research Fellowship, and the School of Computer Science Distinguished Dissertation Award from Carnegie Mellon University.

The challenging task of Byzantine self-stabilizing pulse synchronization requires that, in the presence of a minority of nodes that are permanently maliciously faulty, the non-faulty nodes must start firing synchronized pulses in a regular fashion after a finite amount of time, regardless of the initial state of the system. We study this problem under full connectivity in a model where nodes have local clocks of unknown, but bounded drift, and messages are delayed for an unknown, but bounded time.

We present a generic scheme that, given a synchronous consensus protocol P, defines a self-stabilizing pulse synchronization algorithm A(P). If P terminates within R rounds (deterministically or with high probability), A(P) stabilizes within O(R) time (deterministically or with high probability, respectively). Utilizing different consensus routines, our transformation yields various improvements over previous techniques in terms of stabilization time and bit complexity. Finally, we sketch how to establish the abstraction of synchronous, integer-labeled rounds on top of pulse synchronization, at essentially the same complexity bounds. We will discuss our approach and its merits assuming no previous knowledge on the problem, however, basic familiarity with consensus will be beneficial.

Short bio: Christoph Lenzen received a diploma degree in Mathematics from the University of Bonn, Germany, and subsequently performed his graduate studies in Distributed Computing in the group of Professor Roger Wattenhofer at ETH Zurich. In 2011, he was a postdoctoral Fellow at the Hebrew University of Jerusalem, with Danny Dolev. Currently, he is a postdoctoral fellow at the Weizmann Institue of Science, with Professor David Peleg. His research interests cover distributed computing in a wider sense, including topics such as randomized load balancing, graph algorithms, and clock synchronization. He published e.g. at PODC, SPAA, FOCS, and STOC, and in JACM. In 2009, he and his coauthors received the PODC best paper award for their work on gradient clock synchronization.

Linear max-plus dynamical systems describe the time behavior of a large variety of distributed systems. These include transportation networks, manufacturing plants, and network synchronizers, as well as link reversal algorithms for routing and scheduling. It is known that these systems show a periodic behavior after an initial transient phase. Assessment of the length of this transient phase provides important information on complexity measures of such systems. By identifying parameters in a graph representation of these systems, we give the first potentially subquadratic upper bounds on the transient, which can help during system design.

I will describe a new approach to the old problem of automatic temporal property verification. As well as leading to dramatic performance improvements over existing techniques, this approach also brings some light to a couple of age-old questions.

Bio: Dr. Byron Cook is a Principal Researcher at Microsoft Research Cambridge, as well as Professor of Computer Science at University College London. His research interests focus on formal verification, theorem proving, operating systems and biology. Byron is particularly well known for his work on the Terminator program termination prover as well as the SLAM software model checker.

Several applications from program analysis, design and testing rely critically on solving SMT problems. Many applications build on top of SMT solvers in sophisticated ways by carefully crafting the solver interaction. Many applications at their core solve for recursive predicates and so far SMT solvers have no direct support for these. This talk presents a new extension of Z3 and an algorithm, PDR extended to SMT domains, for handling recursive predicates. The IC3 algorithm was recently introduced for proving properties of finite state reactive systems. It has been applied very successfully to hardware model checking.

We provide a specification of the algorithm using an abstract transition system and highlight its dual operation: model search and conflict resolution. We then generalize it along two dimensions. Along one dimension we address nonlinear fixed-point operators (push-down systems) and evaluate the algorithm on Boolean programs. In the second dimension we leverage proofs and models and generalize the method to Boolean constraints involving theories. A side-effect of our approach is a model-based method for computing interpolants of recursion-free Horn clauses for linear real arithmetic. The method also produces a decision procedure for timed push-down systems.

The talk is based on joint work with Krystof Hoder that will appear at SAT 2012.

Equivalence checking problem is that of verifying whether two given programs have the same behavior. By formalizing the terms "program" and "behavior" in different bases, we obtain numerous variants of this problem. It has been always regarded as one of the most fundamental problems in computer science which has a wide range of applications in software engineering. The talk provides a comprehensive survey of significant achievements in the study of equivalence checking problem for various models of programs since the early 50-s XX.

This talk reports on a true RiSE cooperation. I will present joint work with Thomas A. Henzinger and Ali Sezgin from IST Austria as well as Christoph M. Kirsch and Hannes Payer from the University of Salzburg. The cooperation was initiated during one of the RiSE meetings.

There is a trade-off between performance and correctness in implementing concurrent data structures. Better performance may be achieved at the expense of relaxing correctness, by redefining the semantics of data structures. We address such a redefinition of data structure semantics and present a systematic and formal framework for obtaining new data structures by quantitatively relaxing existing ones. We view a data structure as a sequential specification S containing all "legal" sequences over an alphabet A of method calls. Relaxing the data structure corresponds to defining a distance from any sequence over A to the sequential specification: the relaxed sequential specification Sk contains all sequences over A within distance k from S. In contrast to other existing work, our relaxations are semantic (distance in terms of data structure states).

As an instantiation of our framework, we present a simple yet generic relaxation scheme. We show that this relaxation, when further instantiated on queues, stacks, and priority queues, amounts to tolerating bounded out-of-order behavior, which cannot be captured by a purely syntactic relaxation (distance in terms of sequence manipulation, e.g. edit distance). We also present various concurrent implementations of queue, stack, and priority queue relaxations and argue that bounded relaxations provide the means for trading correctness for performance in a controlled way. The relaxations are monotonic which further highlights the trade-off: increasing k increases the number of permitted sequences, which increases the performance.

Program verification is the only way to be certain that a given piece of software is free of (certain types of) errors --- errors that could otherwise disrupt operations in the field. To date, formal verification has been done manually, by specially-trained engineers. Labor costs have heretofore made formal verification too costly to apply beyond small, critical software components.

Our goal is to make verification more cost-effective by reducing the skill set required for program verification and increasing the pool of people capable of performing program verification. Our approach is to transform the verification task (a program and a goal property) into a visual puzzle task --- a game --- that gets solved by people. The solution of the puzzle is then translated back into a proof of correctness. The puzzle is engaging and intuitive enough that ordinary people can through game-play become experts.

This talk presents the status of the Verification Games project and our Pipe Jam prototype game.

A pluggable type system extends a language's built-in type system to confer additional compile-time guarantees. We will explain the theory and practice of pluggable types. The material is relevant for researchers who wish to apply type theory, and for anyone who wishes to increase confidence in their code. After this session, you will have the knowledge to: analyze a problem to determine whether pluggable type-checking is appropriate; design a domain-specific type system; implement a simple type-checker (in as little as 4 lines of code!); scale a simple type-checker to more sophisticated properties; and better appreciate both object-oriented types and flexible verification techniques.

While the theory is general, our hands-on exercises will use a state-of-the-art system, the Checker Framework, that works for the Java language, scales to millions of lines of code, and is being adopted in the research and industrial communities. Such a framework enables researchers to easily evaluate their type systems in the context of a widely-used industrial language, Java. It enables non-researchers to verify their code in a lightweight way and to create custom analyses. And it enables students to better appreciate type system concepts.

Hybrid systems are those which exhibit both discrete "jump" and continuous "flow" dynamics. Their importance---as components of cyber-physical systems---is paramount now that more and more physical systems (cars, airplanes, etc.) are controlled with computers.

There are naturally two directions towards the study of hybrid systems: control theory (typically continuous) and formal verification (typically discrete). For us from the formal verification community, therefore, the big challenge is how to incorporate continuous "flow" dynamics. Many existing techniques---such as hybrid automaton or Platzer's differential dynamic logic---include differential equations explicitly. This incurs a difficult (and very interesting) question of how to handle differential equations.

In our project we take a different path of turning flow into jump---more precisely into infinitely many jumps each of which is infinitesimal (i.e. infinitely small). This makes everything discretejump dynamics, to which all the discrete techniques accumulated in the community of formal verification readily apply. This venture is mathematically supported by *nonstandard analysis*, where we canrigorously speak about infinites and infinitesimals.

In the talk I will lay out: 1) our framework of a while-language and a Hoare-style program logic, augmented with an infinitesimal constant, for modeling and verification of hybrid systems; 2) how discrete verification techniques can be *transferred*, as they are, to hybrid applications, via the celebrated *transfer principle* in nonstandard analysis; and 3) the overview of our prototype automatic prover.

The talk is based on the joint work with Kohei Suenaga, Kyoto University.

A major result concerning temporal logics is Kamp's Theorem (1968) which states that the pair of modalities "until" and "since" is expressively complete for the first-order fragment of the monadic logic over the linear time canonical models.

We provide a simple proof of Kamp's theorem.

Developing modern software applications typically involves composing functionality from existing libraries. This task is difficult because libraries may expose many methods to the developer. To help developers in such scenarios, in this talk I will present a technique that synthesizes and suggests valid expressions of a given type at a given program point. As the basis of our technique we use type reconstruction for lambda calculus with subtyping. We show that the inhabitation problem in the presence of subtyping remains PSPACE-complete. We introduce a succinct representation for type judgements that merges types into equivalence classes to reduce the search space. We introduce a proof rule on this succinct representation of types and show that it is sound and complete for inhabitation. We implemented the resulting algorithm and deployed it as a plugin for the Eclipse IDE for Scala.

~This is a joint work with Tihomir Gvero and Viktor Kuncak~

Localizing the cause of an error in an error trace is one of the most time-consuming aspects of debugging. In this talk, I present a novel technique to automate this task. For this purpose, I introduce the concept of "error invariants". An error invariant for a position in an error trace is a formula over program variables that over-approximates the reachable states at the given position while only capturing states that will still produce the error, if execution of the trace is continued from that position. Error invariants can be used for slicing error traces and for obtaining concise error explanations. I will present an algorithm that computes error invariants from Craig interpolants, which we construct from proofs of unsatisfiability of formulas that explain why an error trace violates a particular correctness assertion. This is joint work with Evren Ermis and Martin Schaef.

In this talk we introduce a new method for solving systems of linear inequalities and linear optimisation. The algorithm incorporates many state-of-the-art techniques from DPLL-style reasoning. We prove soundness, completeness and termination of the method.

Interpreters inhabit a sweet spot on the performance/price curve of programming language implementation. This means that it is cheaper toimplement an interpreter than a compiler, but on the other hand thatcompilers are usually faster than interpreters. This is particularlytrue for high abstraction-level interpreters, where many traditionaloptimizations are not effective. Consequently, such interpreters havea bad reputation for being too slow.

This talk focuses on a previously successful line of research inpurely interpretative optimizations carried out at the Compilers andLanguages group of the Institute of Computer Languages, and presentsnew results of continuing this line of research. In particular, wegive a brief overview of purely interpretative inline caching usingquickening and show how to leverage this foundation for a noveladaptive optimization: native machine-abstraction execution, or NAMASTE forshort. We have implemented NAMASTE and report that this techniqueboosts our previously maximum reported speedup by more than 40%: froma factor of up to 2.4 to a factor of up to 3.4. Since this techniqueis purely interpretative, too, it offers the usual benefits ofinterpreters: ease of implementation, portability, and---compared to ajust-in-time compiler, constant and low memory usage.

We describe a novel technique for bounded analysis of asynchronousmessage-passing programs with ordered message queues. Our boundingparameter does not limit the number of pending messages, nor thenumber of “context-switches” between processes. Instead, we limit thenumber of process communication cycles, in which an unbounded numberof messages are sent to an unbounded number of processes across anunbounded number of contexts. We show that remarkably, despite thepotential for such vast exploration, our bounding scheme gives rise toa simple and efficient program analysis by reduction to sequentialprograms. As our reduction avoids explicitly representing messagequeues, our analysis scales irrespectively of queue content andvariation.

I will talk about notions of computation in a model of set theory extended by "atoms". Sets with atoms where introduced in 1922 by Fraenkel in order to construct a model of a variant of the Zermelo-Frankel axioms in which the axiom of choice fails. They where rediscovered many times under various names (sets with urelements, Fraenkel-Mostowski models, nominal sets, permutation models); in automata theory they appeared in the context of register automata over data words, in a paper by Bojańczyk, Klin, Lasota from LICS'11.

I will recall the basic notions of this set theory. Afterwards, I will define several models of computation based on sets with atoms, including automata, Turing machines and imperative while-programs. Finally, I will sketch a proof that P is not equal to NP for this model of computation.More precisely, I will show a language that is in NP, but is not recognizable by any deterministic Turing machine (even with unlimited time resources). This language is related to the Cai-Fürer-Immerman construction known from finite model theory.

A fundamental task in distributed systems (like the Internet) is to determine efficient routing paths between all pairs of nodes. For efficiency reasons, one frequently resorts to constructing approximate shortest path based on new node labels that encapsulate some hints on a node's location in its name. While the optimal trade-off between routing tables size and approximation ratio is fairly well-understood in this setting, little attention has been paid to quick construction of such tables in a distributed manner. This is crucial, since usually it is impractical - or even infeasible - to aggregate the topology of large systems in a single location, and in a dynamic environment the solution might be already outdated before it can be put to use.

In this talk, we present a novel technique for distributed routing table construction running in O(n^(1/2+eps)+D) rounds of communication (up to polylogarithmic factors in n), where n is the number of nodes in the system and D the diameter of the communication graph. Our algorithm uses messages of size O(log n) and guarantees approximation ratio O(eps^(-1) log eps^(-1)). Under these constraints, our solution is near-optimal: Every algorithm using messages of size O(log n) and achieving a polylogarithmic approximation must run for Omega(n^(1/2)+D) rounds. In constrast, previous algorithms incur running times of Omega(n) even in graphs of constant diameter. Our approach yields improved distributed algorithms for a number of related problems, including distance approximation and Generalized Steiner Forest approximation.

The subject of this talk is to present regular cost functions, a quantitative extension to the notion of regular languages (of words, trees, finite or infinite) for which powerful decision procedures are available.

We will motivate this presentation starting from an open question (FOSSACS 2011) of Rabinovich and Velner concerning an extension of Church synthesis problem in which Player I is allowed, afterward, to change a bounded number of moves he played. Formally, the question is as follows: two players, I and II, which alternatively play a bit, thus producing an infinite play.This play is said n-winning if, up to modifying n of the bits player I has played so far, the play belongs to a given regularlanguage of infinite words. The problem is to decide if there is a natural number n such that Player I can guarantee n-winning.

We will see that this question is naturally (and positively) solved using regular cost functions over infinite words.

Logical methods can be used to unify results for individual graph-theoretic objects, by providing meta-theorems which apply to all suchobjects definable in an appropriate logic. In this talk we discuss graphproperties and graph polynomials definable in First Order Logic and MonadicSecond Order Logic in terms of their definability and combinatorialmeta-theorem. In particular, we show a method of proving non-definabilityusing connection matrices. We extend the results for graph properties byshowing a Feferman-Vaught type theorem for First Order Logic extended withcounting quantifiers.

First, we review how proving reachability and termination properties of transition systems, procedural programs, multi-threaded programs, and higher-order functional programs can be reduced to constraint solving. Second, we show how CTL* properties can be proved using contraint-based setting.Finally, we discuss adequate solving algorithms and tools.

When program verification tools fail to verify a program, either theprogram is buggy or the report is a false alarm. In this situation, theburden is on the user to manually classify the report, but this taskis time-consuming, error-prone, and does not utilize facts alreadyproven by the analysis. We present a new technique for assistingusers in classifying error reports. Our technique computes small,relevant queries presented to a user that capture exactly the information the analysis is missing to either discharge or validate the error. Our insight is that identifying these missing facts is an instanceof the abductive inference problem in logic, and we present a newalgorithm for computing the smallest and most general abductionsin this setting. We perform the first user study to rigorously evaluatethe accuracy and effort involved in manual classification of error reports. Our study demonstrates that our new technique is very usefulfor improving both the speed and accuracy of error report classification.

Model-based testing relies on models of a SUT and its environment. To define a notion of "interesting" test cases, test selection criteria need to be defined. Structural criteria lend themselves to automated generation and may be required by development standards. Yet, when used as test selection criterion, coverage usually does not correlate with failure detection. I'll motivate the need to overcome the a-priori use of coverage criteria for test selection by presenting one conceptualization from the literature. Using this conceptualization, one can show that in general, partition-based testing – which relies on a partition of a program’s input domain for test selection and which therefore subsumes coverage-based test selection – can be better, the same, or worse than random testing. This questions the very idea of partition-based testing in the typical situation where increased a-priori likelihoods of some of the blocks in the input domain partition cannot be assumed. On these grounds, I’ll present one approach to generating tests via model-based flaw injection. These tests (1) targeted security properties and attacks such as cross site scripting attacks rather than structural criteria, and (2) are turned into implementation-level tests that are run in a semi-automatic way and that often can reproduce attacks at the implementation level.

In this talk, I describe our work in automating thedeductive verification method of proving inductive invariants fornetworks of hybrid automata that are parameterized by the number ofinteracting automata. Our approach is inspired by the invisibleinvariants method for discrete systems. I present a small modeltheorem for hybrid automata networks, which allows us to reduce safetyverification of arbitrarily many interacting automata to verificationof a (usually small) finite number. The verification method isimplemented in a tool, Passel, which uses the Z3 satisfiability modulotheories (SMT) solver. I use the Small Aircraft Transportation System(SATS) landing protocol as an example, where aircraft coordinate toensure collisions do not occur while attempting to land at a runway.Lastly, I describe our current work to finish automating theverification process by synthesizing inductive invariants using SATSand Fischer's mutual exclusion protocol as examples.

We characterize the complexity of the safety verification problem forparameterized systems consisting of a leader process and arbitrarily manyanonymous and identical contributors. Processes communicate through ashared, bounded-value register. While each operation on the registeris atomic, there is no synchronization primitive to execute a sequenceof operations atomically. The model is inspired by distributedalgorithms implemented on sensor networks.We analyze the complexity of the safety verification problem whenprocesses are modeled by finite-state machines, pushdown machines, andTuring machines. Our proofs use combinatorial characterizations ofcomputations in the model, and in case of pushdown-systems, some novellanguage-theoretic constructions of independent interest.

With multi-core processors now in common use,implementations of data structures which allow forefficient, concurrent access by many processeshave become an important basic building block for applications.The talk will introduce linearizability and lock-freedom asthe standard safety and liveness criteria for concurrentdata structures. The first part of the talk then will present asound and complete proof technique for linearizability basedon backward simulations.The second half of the talk will sketch a temporal logic frameworkimplemented in the interactive theorem prover KIV, that has been usedto verify both linearizability and lock-freedom for several casestudies.

Data-centric dynamic systems are systems where both the process controlling the dynamics and the manipulation of data are equally central. We study verification of (first-order) μ-calculus variants over relational data-centric dynamic systems, where data are maintained in a relational database, and the process is described in terms of atomic actions that evolve the database. Action execution may involve calls to external services, thus inserting fresh data into the system. As a result such systems are infinite-state. We show that verification is undecidable in general, and we isolate notable cases where decidability is achieved. Specifically we start by considering service calls that return values deterministically (depending only on passed parameters). We show that in a μ-calculus variant that preserves knowledge of objects appeared along a run we get decidability under the assumption that the fresh data introduced along a run are bounded, though they might not be bounded in the overall system. In fact we tie such a result to a notion related to weak acyclicity studied in data exchange. Then, we move to nondeterministic services and we investigate decidability under the assumption that knowledge of objects is preserved only if they are continuously present. We show that if infinitely many values occur in a run but do not accumulate in the same state, then we get again decidability. We give syntactic conditions to avoid this accumulation through the novel notion of "generate-recall acyclicity", which ensures that every service call activation generates new values that cannot be accumulated indefinitely.

Modern software tends to undergo frequent requirement changes and typically is deployed in many different scenarios. This poses significant challenges to formal software verification, because it is not feasible to verify a software product from scratch after each change. It is essential to perform verification in a modular fashion instead. The goal must be to reuse not merely software artifacts, but also specification and verification effort.In our setting code reuse is realized by delta-oriented programming, an approach where a core program is gradually transformed by code "deltas" each of which corresponds to a product feature. The delta-oriented paradigm is then extended to contract-based formal specifications and to verification proofs. As a next step towards modular verification we transpose Liskov's behavioural subtyping principle to the delta world. Finally, based on the resulting theory, we perform a syntactic analysis of contract deltas that permits to automatically factor out those parts of a verification proof that stays valid after applying a code delta. This is achieved by a novel verification paradigm called "abstract symbolic execution".

Today’s software systems become more complex. Main factors that determine software complexity are huge amounts of distributed components, heterogeneity, problem size and dynamic changes of the environment. These challenges are especially emphasized in distributed software systems. One promising way that can cope with the increased complexity is to employ principles of self-organization at different levels in the software architecture in order to shift the complexity from one central coordinator component to many distributed, autonomously acting software components. The intention is to learn from the environment - to use different bio-mechanisms that are going to be mapped and adapted for certain problems - and apply this knowledge to complex software systems. The methods to be applied for a new conception of self-organizing coordination infrastructures comprise a combination of: shared data spaces, intelligent and adaptive algorithms, benchmarking, multi-agent technologies, formal specification, and interdisciplinary literature research. Communication via shared data uses blackboard based interaction patterns which is proven to be useful for communication between autonomous agents, and offers a highly agile software architecture style. The expected results are findings about how and in which use cases the principles of self-organization can contribute to reduce software complexity, theoretical foundations of new bio-inspired algorithms, and some case studies that prove the feasibility of the approaches.

Clock synchronization is the foundation of distributed real-time architectures such as the Timed-Triggered Architecture. Maintaining the local clocks synchronized is particularly important for fault tolerance, as it allows one to use simple and effective fault-tolerance algorithms that have been developed in the synchronous system model. Clock synchronization algorithms have been extensively studied since the 1980s, and many fundamental results have been established. Traditionally, the correctness of a new clock synchronization algorithm is shown by reduction to these results. Until now, formal proofs of correctness all relied on interactive theorem provers such as PVS or Isabelle/HOL. In this talk, we discuss an automated proof of the TTEthernet clock-synchronization algorithm that is based on the SAL model checker. Furthermore, we present how the formal models and proofs can be reused in the verification of more advanced algorithms.

In this talk I will describe a technique to synthesize models representing certain biological phenomena from specification given by mutation experiments.The synthesis algorithm had to address two conceptual problems.First, how to automatically synthesize a concurrent in-silico model for cell development given in-vivo experiments of how particular mutations influence the experiment outcome? The problem of synthesis under mutations is unique because mutations may produce non-deterministic outcomes (presumably by introducing races between competing signaling pathways in the cells) and the synthesized model must be able to replay all these outcomes in order to faithfully describe the modeled cellular processes. In contrast, a "regular" concurrent program is correct if it picks any outcome allowed by the non-deterministic specification. We developed synthesis algorithms and synthesized a model of cell fate determination of the earthworm C. elegans. A version of this model previously took systems biologists months to develop.Second, how to address the problem of under-constrained specifications that arise due to incomplete sets of mutation experiments? Under-constrained specifications give rise to distinct models, each explaining the same phenomenon differently. Addressing the ambiguity of specifications corresponds to analyzing the space of plausible models. We develop algorithms for detecting ambiguity in specifications, i.e., whether there exist alternative models that would produce different fates on some unperformed experiment, and for removing redundancy from specifications, i.e., computing minimal non-ambiguous specifications.If time permits, I will briefly describe our modeling language (embedded into Scala) and how this language design and embedding allows us to build an efficient synthesizer.

In this talk we look at randomized leader election in synchronous distributednetworks. We first present a distributed leader election algorithm for completen-node networks that runs in O(1) rounds and (with high probability) takes onlyO(\sqrt{n} \log^{3/2}(n)) messages to elect a unique leader (with highprobability). We extend this algorithm to solve leader election on anyconnected non-bipartite n-node network G in O(\tau(G)) time andO(\tau(G) \sqrt{n} \log^{3/2}(n)) messages, where \tau(G) is the mixing time ofa random walk on G. The above result implies highly efficient (sublinearrunning time and messages) leader election algorithms for arbitrary networkswith small mixing times, such as expander graphs and hypercubes. In contrast,previous leader election algorithms had at least linear message complexity incomplete graphs and even super-linear message complexity when consideringtime-efficient algorithms.Finally, we show a lower bound of \Omega(\sqrt{n}) messages for any leaderelection algorithm that succeeds with probability at least 1/e + \epsilon, forany arbitrarily small constant \epsilon > 0.This talk is based on joint work with Shay Kutten, Gopal Pandurangan,David Peleg, and Amitabh Trehan.

Automatic construction (synthesis) of correct-by-design software,directly from specification is, of course, more desireable thant theusual software development process. The latter typically includesseveral cycles of coding, testing or automatic verification atdifferent development levels, and new errors may be introduced evenwhen attempting to remove the old ones. While automatic verificationis already provably and and practically difficult, code synthesis hasan ever higher, prohibitive, complexity. Even worse, the automaticconstruction of concurrent code iwas shown, under some simpleassumptions, to be undecideable.In this lecture, I will present some recent results and ideas that tryto circumvent the classical dead-end results on concurrent softwaresynthesis.The first techniques uses a combination of model checking and geneticprogramming in a, mostly automatic, process of finding correct codefromtemporal specification. The second technique will add control to anexisting concurrent system in order to impose further properties to anexisting code. This is done using logic of knowledge, and with therelaxing assumption that additional interactions between processes maybe added, when needed.The third technique will be based on using a high level, large granularity,modeling formalism, which can be used for the high level design of thesystem and can be implemented simply and automatically on standardconcurrent architectures.The lecture would assume only very basic familiarity of logic and concurrentmodeling of systems.

When constructing complex concurrent and distributed systems, abstraction is vital: programmers should be able to reason about system components in terms of abstract specifications that hide the implementation details. Nowadays such components often provide only weak consistency guarantees about the data they manage: in shared-memory systems because of the effects of relaxed memory models, and in distributed systems because of the effects of replication. This makes existing notions of component abstraction inapplicable.In this talk I will describe our ongoing effort to specify consistency guarantees provided by modern shared-memory and distributed systems in a uniform framework and to propose notions of abstraction for components of such systems. I will illustrate our results using the examples of the C/C++ memory model and eventually consistent distributed systems.This is joint work with Mark Batty (University of Cambridge), Sebastian Burckhardt (Microsoft Research), Mike Dodds (University of York), Hongseok Yang (University of Oxford) and Marek Zawirski (UPMC).

We aim to enrich the specifications of finite state systems with quantitativeaspects. Specifically, we consider systems (Kripke structures) with numericvariables, and look for a suitable specification language in the form ofa temporal-logic over the accumulative sum and average of the variables. Anexample for such a specification is Always( Sum(energy) > 0 or Sum(money)> 0 ) and Eventually-Always( Average(Revenue) > 1,000,000 ). As a first stage,we examine the expressiveness limits that still allow for a decidablemodel-checking procedure. In the talk, I plan to explain our research directionand the results we have so far. This is a joint work with KrishnenduChatterjee, Thomas Henzinger and Orna Kupferman.

Given a probabilistic system M, i.e. a model withprobabilistic transitions, one may be interested to knowwhether execution paths on M satisfy a given property\phi. When the model is totally observable and \phi isomega-regular, the question can be answered using LinearProgramming or Iteration methods.

We focus on the context of partially observed models, theextreme casebeing the model of Probabilistic Automata: the observerhas no feedback on the current state of an executionpath. Most interesting problems become undecidable, thisis the case for instance for the positive Buchi problem:

Given a probabilistic Automata, is there an input wordsuch that with positive probability the associated pathssatisfy a given Buchi condition?

After an preliminary introduction of the probabilisticmodels of Markov Decision Processes and ProbabilisticAutomata, and an overview of the decidability resultsknown so far, we will present the notion of ``simpleprocesses'', which allows the definition of probabilisticmodels on which the verification of general omega-regularproperties is decidable. The notion of simple process isinspired by works on the structure of the tail sigma fieldof a non homogeneous Markov chain, and a DecompositionSeparation theorem which generalizes the partition of thestate space of a finite homogeneous Markov chain intoirreducible and transient components, to the context offinite non homogeneous Markov chains.

We describe Aligators, a tool for the generation of universally quantifiedarray invariants. Aligators leverages recurrence solving and algebraictechniques to carry out inductive reasoning over array content. The Aligatorsloop extraction module allows treatment of multi-path loops by exploiting theircommutativity and serializability properties. Our experience in applyingAligators on a collection of loops from open source software projects indicatesthe applicability of recurrence and algebraic solving techniques for reasoningabout arrays.

This is a joint work with T. Henzinger, T. Hottelier and A. Rybalchenko.

For Very Large Scale Integrated (VLSI) Circuits intended to be used inhighly reliable applications, formal specification and analysis ismandatory. Two trends in VLSI design favour a modeling approachanalogous to that used for distributed systems: (i) noticeablecommunication delays between circuit components and (ii) increasingfailure rates caused by wear-out and particle hits in circuits withever decreasing feature sizes. Despite these striking similarities,specifying and analyzing circuits by means of classic distributedsystem models is either overly lengthy or not possible. To overcomethese limitations a new modeling and analysis framework tied to thepeculiarities of fault-tolerant on-chip algorithms ispresented.

The capabilities of this framework are then illustrated by applying it(i) to analyze and prove correct a fault-tolerant on-chip tickgeneration algorithm and (ii) to prove the impossibility of solvingthe short-pulse filter problem with purely digital and statelessmodules only.

In the clock synchronization problem, on seeks to keepdevices in a communication network as closely synchronized as possiblein face of drifting clocks and unknown message transmission times. Thisand similar tasks have been research topic for several decades now,both in theory and practice. So, what is different about this talk? Weask not only for the maximum worst-case clock skew between any twonodes in the system to be minimal, but also for devices which canestimate each other's clock values accurately to be synchronizedtightly. For many applications, the latter property is crucial, as theymerely require that devices capable of direct communication arewell-synchronized. Moreover, we allow for arbitrary network dynamics,i.e., communication links may fail and become operative again atarbitrary times. Interestingly, this challenging task can be optimallysolved by a stunningly simple algorithm.

The talk will comprise two parts. First, we present the problem and ourresults to a general audience. In the second, more technical part, wetry to shed light on the techniques by which we obtain ourasymptotically optimal bounds.

Short Bio: Christoph Lenzen studied mathematics at the university ofBonn and received his diploma degree in October 2007. Currently he isPh.D. student in the Distributed Computing Group at ETH Zurich and isgoing to graduate in December. His research topics cover distributedgraph algorithms, clock synchronization, and load balancing algorithms.The line of work on gradient clock synchronization has beenparticularly successful, with publications at FOCS, PODC, and in JACM,as well as the best paper award at PODC 2009.

Notions of specification, implementation, satisfaction, and refinement,together with operators supporting stepwise design, constitute aspecification theory. We construct such a theory for Markov Chains(MCs) employing a new abstraction: Constraint Markov Chains.Constraint MCs permit rich constraints on probability distributions and thusgeneralize prior abstractions such as Interval MCs. Linear (polynomial)constraints suffice for closure under conjunction (respectively parallelcomposition). This is the first specification theory for MCs with suchclosure properties. Despite the generality, all operators and relationsare computable.

In this talk I will first introduce the notion ofhigher-order recursion schemes and give the tightconnection that exists with automata theory. In thiswork, we use schemes as a way to produce an infinitetree: with any schemes one associate a (unique) infinitetree. A paper by Luke Ong [LICS'06] establishes that anytree generated in such a way has a decidable second ordertheory.

We present here a stronger result, namely that given a tree tdescribed by a scheme and an MSO formula phi, the treet_phi, obtained by marking thos nodes in t where phiholds, can be (effectively) generated by a scheme. Acorollary of this result is that the trees generated byschemes are closed by successive application of an MSOinterpretation followed by unfolding.

The talk will be based on the following papers:

• Arnaud Carayol, Matthew Hague, Antoine Meyer, Luke Onget Olivier Serre. Winning regions of higher-orderpushdown games, in Proceedings of the Twenty-Third AnnualIEEE Symposium on Logic in Computer Science, LICS 2008,IEEE Computer Society, pp.193-204, 2008.
• Matthew Hague, Andrzej Murawski, Luke Ong et OlivierSerre. Collapsible Pushdown Automata and RecursionSchemes, in Proceedings of the Twenty-Third Annual IEEESymposium on Logic in Computer Science, LICS 2008, IEEEComputer Society, pp.452-461, 2008.
• Christopher Broadbent, Arnaud Carayol, Luke Ong etOlivier Serre. Recursion Schemes and Logical Reflection,in Proceedings of the Thwenty-fifth Annual IEEE Symposiumon Logic in Computer Science, LICS 2010, IEEE ComputerSociety, pp. 120-129, 2010.

(Very) Short Bio:

Olivier Serre is a full-time researcher employed by CNRSin LIAFA (University Paris 7 & CNRS) since October2005. He is also a part-time assistant professor at EcolePolytechnique. Previously he did a PhD (2001-2004) underthe direction of Anca Muscholl and Jean-Eric Pin. Hismain research interests are games in computer science,automata theory, infinite states system and logic.

I will present an inverse method allowing to synthesizeconstraints on timing delays (seen as parameters) in theframework of timed automata.Given a reference valuation of the parameters, this method synthesizesa constraint on the parameters, guaranteeing the sametime-abstract linear behavior as for the referencevaluation.This is useful for safely relaxing some values of the referencevaluation and gives a criterion of robustness to the system.In particular, LTL formulae are preserved.By iterating this inverse method on various points of a boundedparameter domain, we are then able to partition theparametric space into good and bad zones, with respect to agiven property one wants to verify.A tool, IMITATOR, was developed and was successfully applied tovarious examples of asynchronous circuits and protocols.An extension to probabilistic timed systems allows to synthesize aconstraint on the timing parameters guarantying the value ofthe reachability probabilities.

A control system consists of two subsystems: the controllerand the "plant" (controlled system).In an endless loop the controller measures outputs from and sends commands to theplant in order to drive it towards a given goal region.We focus on software based control systems,that is, systems where the the controllerconsists of software running on a microprocessorand measures from the plant are quantized (AD conversion)before being sent to the control software.

System requirements for control systemsare typically given as specifications for the closed loop system,that is the system consisting ofthe plant and the (to be designed) controller.

Typically, Control engineering techniques are usedto design the control law(i.e. the functional specifications for the control software)from the closed loop system requirements.Software engineering techniques are then used todesign the control software implementing the given controllaw.

Such an approach leaves open many questions about the correctnessof the control software with respect to the closed loop system requirementsand motivates investigation on methods and tools for automatic synthesis ofcorrect-by-construction control software from closed loopsystem requirements.

We present an algorithm that given a Discrete Time Linear Hybrid System(DTLHS) model for the plant P returns acorrect-by-construction software implementation Kfor a (near time optimal)robust Quantized Feedback Controllerfor P along witha suitable representation forthe set of states on which Kis guaranteed to work correctly (controllable region).Furthermore, K has a Worst Case Execution Time(WCET)guaranteed to belinear in the number of bits of the quantization schema.

We implemented our algorithm on top of the CUDD OBDD packageand of the GLPK MILP solver and present results on using such an implementation to synthesize Ccontrollers for the buck DC-DC converter,a widely used mixed-mode analog circuit.Our experimental results show that our proposed approach is viable andthe performance of the automatically synthesized controllers compare wellwith those of controllers designed using ad-hoc approaches.

************

This talk is mainly based on our CAV2010 paper:
Federico Mari, Igor Melatti, Ivano Salvo, Enrico Tronci.
Synthesis of Quantized Feedback Control Software forDiscrete Time Linear Hybrid Systems.
Tayssir Touili, Byron Cook, Paul Jackson (Eds.):
Computer Aided Verification, 22nd International Conference,CAV 2010, Edinburgh, UK,
July 15-19, 2010. Proceedings. Lecture Notes in ComputerScience 6174 Springer 2010,
ISBN 978-3-642-14294-9 CiteSeerX

We introduce streaming data string transducers that mapinput data strings tooutput data strings in a single left-to-right pass inlinear time. Data strings are (unbounded) sequences ofdata values, tagged with symbols from a finite set, over apotentially infinite data domain that supports onlythe operations of equality and ordering. The transduceruses a finite set of states, a finite set of variablesranging over the data domain, and a finite set ofvariables ranging over data strings. At every step, it canmake decisions based on the next input symbol, updatingits state, remembering the input data value in its datavariables, and updating data-string variables byconcatenating data-string variables and new symbols formedfrom data variables, while avoiding duplication. Weestablish PSPACE bounds for the problems of checkingfunctional equivalence of two streaming transducers, andof checking whether a streaming transducer satisfiespre/post verification conditions specified by streamingacceptors over input/output data-strings.

We identify a class of imperative and a class offunctional programs, manipulating lists of data items,which can be effectively translated to streamingdata-string transducers. The imperative programsdynamically modify a singly-linked heap by changingnext-pointers of heap-nodes and by adding new nodes. Themain restriction specifies how the next-pointers can beused for traversal. We also identify an expressivelyequivalent fragment of functional programs that traverse alist using syntactically restricted recursive calls. Ourresults lead to algorithms for assertion checking and forchecking functional equivalence of two programs, writtenpossibly in different programming styles, for commonlyused routines such as insert, delete, and reverse.

Computer systems are routinely deployed in life- andmission- critical situations, yet in most cases theirsecurity, safety or dependability cannot be assured to thedegree warranted by the appli- cation. In other words,trusted computer systems are rarely really trustworthy.

We believe that this is highly unsatisfactory, and have embarked on alarge research program aimed at bringing reality in linewith expectations. In this talk describes NICTA�s researchagenda for achieving true trustworthiness in systems. Thefirst pahse has been concluded, with the world's firstformal proof of functional correctness of a complete OSmicrokernel. The second phase, in progress, aims at makingdependability guarantees for complete real-world systems,comprising millions of lines of code.

Bio:

Gernot Heiser holds the position of Scientia Professro andJohn Lions Chair of Operating Systems at theUniversity of New South Wales (UNSW), and leads the TrustworthyEmbedded Systems (ERTOS) group at NICTA, Australia'sNational Centre of Excellence for ICT Research. He joinedNICTA at its creation in 2002, and before that was afull-time member of academic staff at UNSW from 1991. Hispast work included the Mungi single-address-spaceoperating system, several un-broken records in IPCperformance, and the best-ever reported performance foruser-level device drivers.

In 2006, Gernot with a number of his students founded OpenKernel Labs, now the market leader in secureoperating-systems and virtualization technology for mobilewireless devices. The company's OKL4 operating system, adescendent of L4 kernels developed by his group at UNSWand NICTA, is deployed in more than a billion mobilephones. This includes the Motorola Evoke, the first (andto date only) mobile phone running a high-level OS (Linux)and a modem stack on the same processor core.

In a former life, Gernot developed semiconductor devicesimulators and models of device physics for suchsimulators, and pioneered the use of three-dimensionaldevice simulation for the characterisation andoptimisation of high-performance silicon solar cells.

Faulty device drivers are the leading source of reliability problems inmodern operating systems. Automatic device driver synthesis aims toaddress this problem by achieving driver correctness by construction.To this end, the driver implementation is generated automatically basedon a formal specification of the device and the interface between thedriver and the operating system.

In this talk I will give a high-level overview of the driver synthesismethodology, present a formalisation of the driver synthesis problem asa controller synthesis problem, and discuss the main challenges thatmust be addressed in order to turn driver synhtesis into a practicaltechnique capable of generating drivers for a wide range of devices.

In this talk, we will show how synchrony conditions can be added to theasynchronous distributed computing model in a way that avoids anyreference to message delays and computing step times, as well as anyglobal constraints on communication patterns and network topology. Morespecifically, we will introduce the Asynchronous Bounded-Cycle (ABC)model, where clock synchronization and lock-step rounds can easily beimplemented and proved correct, even in the presence of Byzantinefailures. Furthermore, we will describe some weaker variants of the ABCmodel that allow even more relaxed system assumptions. We will also seehow the ABC model relates to existing partially synchronous system models,in particular, to the Theta Model of Le Lann and Schmid, anddiscuss some aspects of the ABC model's applicability in real systems.

Automated verification of multi-threaded programs requiresexplicit identification of the interplay betweeninteracting threads, so called environment transitions, toenable scalable, compositional reasoning. Once theenvironment transitions are identified, we can proveprogram properties by considering each program thread inisolation, as the environment transitions keep track ofthe interleaving with other threads. Finding adequateenvironment transitions that are sufficiently precise toyield conclusive results and yet do not overwhelm theverifier with unnecessary details about the interleavingwith other threads is a major challenge.

In this talk, I will present a method for safetyverification of multi-threaded programs that applies(transition) predicate abstraction-based discovery ofenvironment transitions, exposing a minimal amount ofinformation about the thread interleaving. The crux of ourmethod is an abstraction refinement procedure that usesrecursion-free Horn clauses to declaratively stateabstraction refinement queries. Then, the queries areresolved by a corresponding constraint solvingalgorithm. We present preliminary experimental results formutual exclusion protocols and multi-threaded devicedrivers.

Software synthesis is a technique for automatically generating codegiven a specification. The goal of software synthesis is to make codingeasier while increasing both the productivity of the programmer and thecorrectness of the produced code. Code produced this way is correct byconstruction. However, due to the high computational cost ofsynthesizing code, this idea was not further explored until recently. We arewitnessing a regaining interest in software synthesis that is driven by theincreasing computational power. Today even desktop machines areable to construct code from complex input specifications.

In this talk I will present our new approach to synthesis that relies onthe use of automated reasoning and decision procedures. We handlecomplex specifications by employing efficient algorithms for reasoningabout the domain of the specification. I will describe how togeneralize decision procedures into predictable and complete synthesisprocedures. Here completeness means that the procedure is guaranteed tofind code that satisfies the given specification. Moreover, thesynthesis procedure also outputs preconditions on input values thatguarantee the existence of the output values. As an example, I willexplain how to transform a decision procedure for lineararithmetic into such a synthesis procedure.

I will also outline a synthesis procedure for specifications given inthe form of type constraints. The procedure takes into accountpolymorphic type constraints as well as code behavior and derives codesnippets that use given library functions. We use a first-orderresolution-based theorem prover to solve these constraints and derivecode snippets. The constraints can have multiple solutions and hence thetheorem prover may produce more than one code snippet. Therefore, we usean additional weight function to rank the derived snippets.

These procedures are implemented as extensions to the Scala compiler andI will include a demo in my talk.

We consider game models for the design of reactive systems working in resource-constrained environments. In mean-payoff games, the resource usage is computed as the long-run average resource level. In energy games, the resource usage is the initial amount of resource necessary to maintain the resource level positive. The resource can be memory, battery, or network usage for example.

While mean-payoff games are a well-established model in game theory and computer science, energy games have received attention only recently.The talk reviews recent results about these games and their relationship.Although they differ very basically in their definition, it is known that energy and mean-payoff games are equivalent forthe simple decision problem of existence of a winning strategy.This observation provides new complexity results for solvingmean-payoff games, and new insights for mean-payoff games combinedwith other conditions such as fairness, imperfect information, or multi-resource systems, though the strong equivalence with energy games usually breaks in such cases.

Reasoning with very large theories expressed in first-order logic canstrongly benefit from a good selection method for relevant axioms.This is confirmed by the fact that the largest available first-orderknowledge base (the Open CYC) contains over 3 million axioms, whileanswering queries to it usually requires not more than a few dozenaxioms.

A method for axiom selection has been proposed in the Sumo INferenceEngine (SInE) system. SInE has won the large theory division of CASCin 2008. The method turned out to be so successful that the next twoyears it was used by the winner of this division, as well as byseveral other competing systems. In this talk we will present thealgorithm and show experimental results based on its implementation inthe Vampire theorem prover.

My talk is intending to encourage research in what I call "physical algorithms". The area of physical algorithms deals with networked systemsof active agents. These agents have access to limited information forvarying reasons; examples are communication constraints, evolving topologies, various types of faults and dynamics. The networked systems we envision include traditional computer networks, but also more generally networked systems, such as social networks, highly dynamic and mobile networks, e.g. networks of entities such as cars or ants. In my talk I will present a few examples from the theory branch of my research group. I should mention that the talk is an updated version of my recent ICALP invited talk.

Systems code is ubiquitous and complex. Moreover, the complexity ofcode is expected to increase as systems designers can no longer expect increasing processor speeds, and thus must turn to concurrency for improved performance. How can we be sure that these programs, running on platforms ranging from human implant devices to nuclear power plant controls, will behave as intended? Addressing systems code correctness in the face of concurrency involves advances in two intertwined fields: automatic software verification and concurrent programming paradigms.

In this talk I will discuss some of our recent work on improving both the correctness as well as the performance of systems software. I will focus primarily on describing a new automatic method of temporal logic verification of programs (POPL'11, CAV'11). I will also discuss recent results on a new language feature that has enabled more concurrency in transactional memory systems, improving performance by an order of magnitude (POPL'10, PPoPP'08, SPAA'08).

Bio:Eric Koskinen's research is centered around developing mathematical techniques which improve the safety and performance of software, and applying those techniques to realistic computer systems. He is currently a PhD candidate at the University of Cambridge, under the supervision of Dr. Byron Cook and Prof. Michael Gordon. Eric was awarded the Gates Cambridge Scholarship, completed an Sc.M from Brown University where he worked with Maurice Herlihy, interned thrice at Microsoft Research, and previously spent three years as a software engineer at Amazon.com.

Even the most advanced reverse engineering techniques and products are weak in recovering data structures in stripped binaries - binaries without symbol tables. Unfortunately, forensics and reverse engineering without data structures is exceedingly hard. In this talk, I will present a new solution, known as Howard, to extract data structures from C binaries without any need for symbol tables. Our results are significantly more accurate than those of previous methods - sufficiently so to allow us to generate our own (partial) symbol tables without access to source code. Thus, debugging such binaries becomes feasible and reverse engineering becomes simpler. Also, we show that we can protect existing binaries from popular memory corruption attacks, without access to source code. Unlike most existing tools, our system uses dynamic analysis (on a QEMU-based emulator) and detects data structures by tracking how a program uses memory.

Despite acknowledged success of model checking, its application faces several problems generally inherent to the approach. In this talk we address such problems as parameterized model checking and combinatorial state explosion.

The uniform verification problem is to prove that a temporal property is satisfied on every instance of a system composed of an arbitrary number of homogeneous processes. We extend the network invariants technique by introducing three simulation relations on labelled transition systems (LTSs) that capture correspondence between paths of two systems with different number of processes. This allows us to apply the technique to parameterized families of LTSs generated by a network grammar in the asynchronous setting.

Using this extension we implemented CheAPS, the checker of asynchronous parameterized systems. The tool iteratively generates candidate invariants of a parameterized family and then it checks invariance property by constructing a semi-block simulation on a few finite LTSs. As soon as required invariant LTSs are found, these are passed to Spin for finite-state model checking.

Our tool, like many others, suffers from the state explosion effect. This observation and a case study of Generic Attribute Registration Protocol brought us to the investigation of symmetry reduction techniques. One recent method in this field, which allows one to check safety properties is lazy symmetry reduction. It copes with partially symmetric systems by refining abstract state space on-the-fly, where abstraction is built w.r.t. symmetry preserving constraints.

We found that the spirit of the original search algorithm is close to the well-known nested depth first search. This enables integration of lazy symmetry reduction into the algorithm of checking a linear temporal logic formula against a finite-state LTS. However, a great care should be taken when performing lasso detection on the abstract state space. To this end we introduced special notions of pseudo-cycles and feasibility conditions that provided us with the basis for proving soundness and completeness of the new algorithm.

The next bold step is the implementation of the algorithm in Spin. As it is heavily optimized for a specific set of techniques, embedding a new one in this tool is a technical challenge. We believe that in general implementation is close to completion, though its experimental evaluation is still in progress.

Usual techniques in abstract interpretation apply "join" operations when control flows from several nodes. Unfortunately, these techniques introduce imprecision, resulting in not being able to prove desired properties.

Modern SMT-solving techniques allow enumerating paths "on demand". We shall see how such path techniques may be combined with conventional polyhedral analysis, quantifier elimination, or with policy iteration, in order to obtain more precise invariants.

As online data sets grow over time, computations that process bulk data become increasingly more expensive. Furthermore, often the same computation runs on evolving data sets repeatedly, which implies that consecutive runs share a large fraction of their input. This motivates an incremental approach where results are incrementally updated as data evolves, instead of being recomputed from scratch. To achieve this, new systems for incremental bulk data processing have been proposed, such as Google's Percolator or Yahoo!'s CBP. However, using these systems comes at a price of losing compatibility with the interface offered by systems like MapReduce, and more importantly, requiring the programmer to implement application-specific dynamic algorithms, which the literature shows to be difficult to develop and implement even for simple problems.

In this talk I will describe the architecture, implementation, and evaluation of incoop, a generic MapReduce framework for incremental computations. incoop detects changes to the inputs to computations and enables the automatic update of the outputs by employing an efficient, fine-grained propagation mechanism. By integrating the proposed approach into the MapReduce framework, we transparently benefit a large class of existing applications. Furthermore, by adopting principles from algorithms and programming languages research, we are able to systematically identify the shortcomings of an initial, task memoization-based approach, and address them using several novel techniques such as a new storage system to store the input of consecutive runs, a new contraction phase that make the incremental computation of the reduce tasks more efficient, and a new scheduling algorithm for Hadoop that is aware of the location of previously computed results.

Computing bounds on the resource usage of a program often requires finding a symbolic worst-case bound on the number of visits to a given program location in terms of the inputs to that program; we call this the reachability-bound problem. The automatic computation of reachability-bounds is challenging because in general such bounds are complicated expressions that hinder the direct application of standard abstract domains and require disjunctive invariants.

We propose a two-step methodology for computing a reachability-bound of a given program location: First, we generate a transition system that disjunctively summarizes all pairs of states for which there is a program execution that visits the location once and again. Second, we compute a bound of the transition system to derive a reachability-bound. We present two approaches that implement this methodology.

Our first approach brings together an abstract-interpretation based iterative technique for computing disjunctive loop invariants and a non-iterative proof-rules based technique for loop bound computation.

Our second approach is based on the so-called size-change abstraction (SCA). We use a closure property of SCA for computing disjunctive loop invariants. We show that SCA offers a separation of concerns for bound computation: we extract local progress measures from small program parts, and then compose these local progress measures to a global bound. We state two program transformations that make imperative programs amenable to bound analysis with SCA.

Recent research in program synthesis has made it possible to effectively synthesize small programs in a variety of domains. In this talk, I will describe two useful applications of this technology that have thepotential to influence daily lives of billions of people. One application involves automating end-user programming using examples, which can allow non-programmers to effectively use computational devices such as cell-phones, computers (and in the future robots) to perform a variety of repetitive tasks. Another application involves building automated tutoring systems that can help students with problem solving in math and science domains.

Bio:Sumit Gulwani is a researcher in the RiSE group at Microsoft Research, Redmond. His primary research interest is in the area of program synthesis with applications to automating end user programming andbuilding automated tutoring systems. Sumit obtained his PhD in computer science from UC-Berkeley in 2005, and was awarded the C.V. Ramamoorthy Award and the ACM SIGPLAN Outstanding Doctoral Dissertation Award. He obtained his BTech in computer science and engineering from the Indian Institute of Technology (IIT) Kanpur in 2000 and was awarded the President's Gold Medal.

In this talk, we discuss the verification problem of parameterized concurrent programs. We propose a semi-compositional reasoning method for verifying safety properties of infinite-thread programs based on computing an over-approximation of the set of reachable states. Our approach is sound and terminating, even for infinite state programs (e.g. programs with recursion or unbounded integers). The essential idea of the technique is to reason about a program with many threads by considering only two thread abstractions at a time, and then combining information across all pairs of threads. Our algorithm consists of a feedback loop that combines techniques from abstract interpretation to compute numerical invariants with techniques from model checking to compute the effects of interference. We implemented our approach in a prototype tool and evaluated it on a selection of parameterized programs including Boolean programs generated by the SatAbs tool by performing predicate abstraction on Linux device drivers.

A simplicial complex is shellable if it can be constructed by gluing a sequence of n-simplexes to one another along (n-1)-faces only. Shellable complexes have been well-studied in combinatorial topology because they have many nice properties.

We show that many standard models of concurrent computation can be captured either as shellable complexes, or as the simple union of shellable complexes. We exploit their common shellability structure to derive new and remarkably succinct tight (or nearly so) lower bounds on connectivity of protocol complexes and hence on solutions to tasks such as k-set agreement.

This talk does not assume prior familiarity with Distributed Computing or Combinatorial Topology.

Joint work with Sergio Rajsbaum.

Programmable Logic Controllers (PLCs) are industrial control systems used as control devices in the automation industry and for monitoring of safety critical infrastructure. Since they are often used in safety critical environments, where a failure might have serious effects for human health or the environment, formal verification of their programs is advised. This huge strive for functional correctness combined with having small, well-structured programs, makes PLCs a very interesting platform for the application of formal methods.

In this talk, I will give a short introduction to PLCs and their programming modes. Then I will turn to the model checker [mc]square, which is developed at the Embedded Software Laboratory at the RWTH Aachen and allows for the verification of PLC programs. I will discuss current progress and obstacles and detail some of our techniques that make the verification of real world PLCs programs feasible.

We present a verification framework for analysing multiple quantitative objectives of systems that exhibit both nondeterministic and stochastic behaviour. These systems are modelled as MDPs, enriched with cost or reward structures that capture, for example, energy usage or performance metrics. Quantitative properties of these models are expressed in a specification language that incorporates probabilistic safety and liveness properties, expected total cost or reward, and supports multiple objectives of these types. We propose and implement an efficient verification framework for such properties and then present two distinct applications of it: firstly, controller synthesis subject to multiple quantitative objectives; and, secondly, quantitative compositional verification. The practical applicability of both approaches is illustrated with experimental results from several large case studies. The talk is joint work with with D. Parker, G. Norman, M. Kwiatkowska and H. Qu which, presented at TACAS 2011.

Binary executables are a promising analysis target in many scenarios, ranging from bug finding over execution time analysis to malware detection. Still, problems such as indirect control flow and the lack of types make it hard to adapt traditional static analysis tool-chains to binaries. While earlier attempts mostly use heuristics to preprocess binaries into a format understandable by static analyzers, we argue for the integration of disassembly, control flow reconstruction, and static analysis in a unified process. This enables sound static analysis of binaries, without fragile and generally unsound preprocessing by heuristic disassemblers.

The result of our work is the novel binary analysis tool Jakstab, which supports classic data flow analysis with domains such as intervals, but also path sensitive, bounded model checking style explicit analysis. Jakstab works directly on binaries and disassembles instructions on demand while exploring the program's state space. We demonstrate its practical usefulness in case studies on open and closed source Windows drivers and system tools. In ongoing work, we are extending our framework to support under-approximate information from execution traces to recover from unknown control flow due to imprecision of the analysis.

The DPLL algorithm for deciding propositional satisfiability is a fundamental algorithm with applications across computer science. The modern algorithm combines model search, deduction, and lemma generation in an elegant and highly efficient manner. An important question is whether the DPLL algorithm can be generalised to richer problems such as program verification.

In this talk I show that DPLL operates over a strict abstraction of propositional logic. This is surprising because it uses an imprecise abstraction to obtain precise results. I will show that DPLL very naturally fits in the framework of abstract interpretation. This view leads straight to a generalisation to programs. The application of this algorithm allows complex properties of non-linear programs to be proved automatically using very simple abstractions. Such proofs are well beyond the scope of significantly more mature tools using richer abstractions.

Software failures can be sorted into two groups: those that cause the software to do something wrong (e.g. crashing), and those that result in the software not doing something useful (e.g. hanging). In recent years automatic tools have been developed which use mathematical proof techniques to certify that software cannot crash. But, based on Alan Turing's proof of the halting problem's undecidablity, many have considered the dream of automatically proving the absence of hangs to be impossible. While not refuting Turing's original result, recent research now makes this dream a reality. This lecture will describe this recent work and its application to industrial software.

Bio: Dr. Byron Cook is a Principal Researcher at Microsoft Research in Cambridge, UK as well as Professor of Computer Science at Queen Mary, University of London. He is one of the developers of the Terminator program termination proving tool, as well as the SLAM software model checker.

The automata-based model checking approach for randomized distributed systems relies on an operational interleaving semantics of the system by means of a Markov decision process and a formalization of the desired event E by an !-regular linear-time property, e.g., an LTL formula. The task is then to compute the greatest lower bound for the probability for E that can be guaranteed even in worst-case scenarios. Such bounds can be computed by a combination of polynomially time-bounded graph algorithm with methods for solving linear programs. In the classical approach, the "worst-case" is determined when ranging over all schedulers that decide which action to perform next. In particular, all possible interleavings and resolutions of other nondeterministic choices in the system model are taken into account.

As in the nonprobabilistic case, the commutativity of independent concurrent actions can be used to avoid redundancies in the system model and to increase the efficiency of the quantitative analysis. However, there are certain phenomena that are specific for the probabilistic case and require additional conditions for the reduced model to ensure that the worst-case probabilities are preserved. Related to this observation is also the fact that the worst-case analysis that ranges over all schedulers is often too pessimistic and leads to extreme probability values that can be achieved only by schedulers that are unrealistic for parallel systems. This motivates the switch to more realistic classes of schedulers that respect the fact that the individual processes only have partial information about the global system states. Such classes of partial information schedulers yield more realistic worst-case probabilities, but computationally they are much harder. A wide range of verification problems turns out to be undecidable when the goal is to check that certain probability bounds hold under all partial-information schedulers.

Cardiac disorders such as tachycardia and fibrillation, are spatial-temporal behaviors of cardiac-cell networks, which correspond to the build-up and break-up of electrical spiral-waves, respectively, and which emerge in certain conditions. To understand and predict these conditions, mathematical models of cardiac cells (mostly differential equations models) have been constructed, which range from 4 to 67 variables and from 27 to 94 associated parameters. The main tool for the analysis of such models is simulation. In this talk I will address the challenges and opportunities associated with the techniques that go beyond simulation, such as model checking and parameter-range identification.

This lecture introduces a theory for the identification, modeling, and formalization of three complementary views onto software and software intensive systems called the problem view, thespecification view, and the solution view. The problem view addresses requirements engineering;the specification view describes the overall system functionality from the users' point of view aiming at the specification of the functional requirements of multi-functional systems in terms of their functions as well as their mutual dependencies. This view leads to a function or service hierarchy. The solution view essentially addresses the design phase to decompose systems into logical architectures formed by networks of interactive components specified by their interface behavior.

These views are closely related and are helpful for the structured modeling of multi-functional systems during their development. We show how the three complementary views work and fit together as major milestones in the early phases of software and systems development. We, in particular, base our approach on a purely logical version of the FOCUS theory for describing interface behavior and the structuring of systems into components. We give a theoretical treatment of all three views by extending the FOCUS model and its interface theory accordingly.

In the distributed balls-into-bins problem, one strives for distributing n balls into n bins as evenly as possible. In each communication round, balls may contact some bins, bins may respond, and balls may commit to a bin. Goals are to minimize the individual and overall message complexities, the maximum bin load, and the number of communication rounds.

Classical algorithms are non-adaptive, that is, each ball decides on the bins it will contact before communication commences. We will show how dropping this requirement drastically improves the trade-offs between the above optimization criterions. Concretely, we present a stunningly simple algorithm that guarantees a maximum bin load of two within log* n + O(1) rounds using O(n) total messages. This is provably optimal for a natural class of algorithms, while dropping any of the requirements of this class enables to achieve a constant running time. To round of the presentation, we discuss how our techniques can be applied to a basic communication task in a clique.

Bio:Christoph Lenzen received his diploma in Mathematics from the university of Bonn in 2007. He continued his studies at ETH Zurich in Roger Wattenhofer's group and received his Ph.D. degree in 2011. Presently he is a postdoc at the Hebrew University of Jerusalem with Danny Dolev. His main area of interest are distributed algorithms, for instance for graph problems such as dominating or independent sets, randomized load balancing, and clock synchronization.

Establishing liabilities in component-based systems is a challenging task, as it requires to establish convincing evidence with respect to occurrence of a failure, and the cae causality relation between the failure and a damage.The second issue is especially complex when several failures are detected and their impact on the occurrence of the damage has to be assessed. In this talk I will propose a formal framework for reasoning about logical causality between component failures and the violation of a system-level specification.

Bio:

This talk will introduce CompCertTSO, a fully-fledged certified compilerfrom a concurrent extension of a C-like language to x86 assembler thathas been programmed and proved correct in Coq, and will describe somesimple compiler optimisations for removing redundant memory fences in programs running on top of the x86-TSO relaxed memory model. While theoptimisations will be performed using standard thread-local control flowanalyses, their correctness is subtle and relies on a non-standard globalsimulation argument.

Bio:

Hard real-time systems are subject to stringent timing constraints, which are dictated by the surrounding physical environment. A schedulability analysis has to be performed in order to guarantee that all timing constraints will be met. Existing techniques for schedulability analysis require upper bounds for the execution times of all the system's tasks to be known. These upper bounds are commonly called worst-case execution times (WCETs). The WCET-determination problem has become non-trivial due to the advent of processor features such as caches, pipelines, and all kinds of speculation, which make the execution time of an individual instruction locally unpredictable. Such execution times may vary between a few cycles and several hundred cycles.A combination of Abstract Interpretation (AI) with Integer Linear Programming (ILP) has been successfully used to determine precise upper bounds on the execution times of real-time programs. The task solved by abstract interpretation is to compute invariants about the processor's execution states at all program points. These invariants describe the contents of caches, of the pipeline, of prediction units etc. They allow to verify local safety properties, safety properties who correspond to the absence of "timing accidents". Timing accidents, e.g. cache misses, pipeline stalls are reasons for the increase of the execution time of an individual instruction in an execution state.The technology and tools have been used in the certification of several time-critical subsystems of the Airbus A380. The AbsInt tool, aiT, is the only tool worldwide, validated for these avionics applications.I will give an introduction to our timing-analysis method, present results about the predictability of cache architectures, and give an overview of current work and open problems.

Bio:
Prof. Reinhard Wilhelm is a full Professor of Computer Science at the Saarland University, Saarbruecken and the Scientific Director of the International Conference and Research Center for Computer Science, Schloss Dagstuhl, Germany. He is the cofounder of AbsInt, a company developing software tools for embedded systems.The research activities of Prof. Reinhard Wilhelm cover a wide range of topics, including compiler generation, program analysis, and software visualisation. His contributions to research have been honored by several awards and prizes. To name a few, Prof. Wilhelm is an ACM Fellow, and he received the European IST Prize with the spin-off company AbsInt, the Alwin Walther Medal, the Konrad-Zuse Medal and the ACM Distinguished Service Award.

We present a construction for turning games with imperfect information into games with perfect information by preserving winning strategies. The generic construction yields an infinite game tree. For games with observable objectives, we define an abstraction method that yields finite, and thus decidable, instances in some relevant cases and furthermore provides a semi-decision procedure for solving distributed games. The talk is on joint work with Lukasz Kaiser and Bernd Puchala forthcoming at FSTTCS 2011.

It is notoriously difficult to make distributed systems reliable. Thisbecomes even harder in the case of the widely-deployed systems thatare heterogeneous (multiple implementations) and federated (multipleadministrative entities). The set of routers in charge of theInternet's inter-domain routing is a prime example of such a system.
We argue that a key step in making these systems reliable is the needto automatically explore the system behavior to check for potentialfaults. In this talk, I will describe the design and implementationof DiCE, a system for online testing of heterogeneous and federateddistributed systems. DiCE runs concurrently with the production systemby leveraging distributed checkpoints and isolated communicationchannels. DiCE orchestrates the exploration of relevant system statesby controlling the inputs that drive system actions. While respectingprivacy among different administrative entities, DiCE detects faultsby checking for violations of properties that capture the desiredsystem behavior. We demonstrate the ease of integrating DiCE with aBGP router and a DNS server, the building blocks of two vital servicesin the Internet. Our evaluation in the testbed shows that DiCE quicklyand successfully detects three important classes of faults, resultingfrom configuration mistakes, policy conflicts and programming errors.
Joint work with Marco Canini, Vojin Jovanovic, Daniele Venzano, GautamKumar, Dejan Novakovic, Boris Spasojevic, and Olivier Crameri

Bio:

In this talk I will give an introduction and present some of my recentresults in to two of the most fundamental problems in algorithmic gametheory and mechanism design: the problem of designing truthfulauctions for selling multiple items and of scheduling unrelatedmachines to minimize the makespan.
In the problem of designing truthful auctions we want to auctionmultiple items together. There might also exist budget and demandconstraints. In the problem of scheduling unrelated machines we assumethat the machines behave like selfish players: they have to get paidin order to process the tasks, and would lie about their processingtimes if they could increase their utility in this way.

Recently, it has been shown how block-wise transferfunctions for linear template constraints can be derivedfor programs defined over piece-wise linear arithmetic.Quantifier elimination is then applied to find a directrelationship between the inputs and the outputs of a block.We extend this work towards bit-vector programs, i.e.programs whose semantics is defined over finite-precisionintegers, by operating in the computational domain ofpropositional Boolean formulae. The drawback of this methodis that it relies on existential quantification, whichinduces a computational bottleneck. To sidestep thiscomplexity, we present a novel method for computing transferfunctions that does not depend on quantifier elimination atall, but uses incremental SAT solving instead.

Bio:

We present a coverage metric targeted at shared memory concurrent programs: the Location Pairs (LP) coverage metric. The goals of this metric are (i) to measure how thoroughly a program has been tested from a concurrency standpoint, i.e., whether enough qualitatively different thread interleavings have been explored, and (ii) to guide testing towards unexplored concurrency scenarios. This metric was inspired by an access pattern known to lead to high-level concurrency errors. We built a tool for measuring LP coverage and used the LP metric for interactive debugging. We also compared LP coverage with other concurrency coverage metrics on Java benchmarks. Using mutations and manually-inserted bugs, we demonstrated that LP coverage corresponds better to concurrency errors, is a better measure of how well a program is exercised concurrency-wise by a test set, reaches saturation later than other coverage metrics, and is viable and useful as an interactive testing and debugging tool.

Bio:
Serdar Tasiran received his BS in Electrical Engineering from Bilkent University in 1991, and his MS and PhD from UC Berkeley in Electrical Engineering and Computer Sciences in 1995 and 1998, respectively. He was a researcher at the Gigascale Systems Research Center, a multi-university, multi-company consortium until 2000. From 2000 to 2003, he was a research scientist at the Systems Research Center (part of DEC, Compaq and later HP Labs) in Palo Alto, CA. Since 2003, he has been at Koc University, Istanbul, Turkey. While at Koc University, he has had visiting appointments at MIT, EPFL, Microsoft Research, USA and India. His research interests are the specification, verification, performance estimation and optimization of concurrent systems.

Automata theory in the 1960s gave a method to prove that certain logical theoriesare decidable. Implicit in this work is the notion of an automatic structure. I will present essential properties of automatic structures, give concrete examples, and mention some foundational problems that are still open. Basic familiarity with logic and automata areenough to follow this talk.

Bio:

We consider verification of programs manipulating dynamic linked data structures such as various forms of singly and doubly-linked lists or trees. We consider important properties for this kind of systems like no null-pointer dereferences, absence of garbage, shape properties, etc.In the first part of the talk, we present a verification method based on a novel use of tree automata to represent heap configurations. A heap is split into several ``separated'' parts such that each of them can be represented by a tree automaton. The automata can refer to each other allowing the different parts of the heaps to mutually refer to their boundaries. Moreover, we allow for a hierarchical representation of heaps by allowing alphabets of the tree automata to contain other, nested tree automata. Program instructions can easily be encoded as operations on our representation structure. This allows verification of programs based on a symbolic state-space exploration together with refinable abstraction within the so-called abstract regular tree model checking.In the second part of the talk, a new separation-logic-based tool called Predator will briefly be presented. The tool is specifically tuned to handle various kinds of linked lists in the low-level form used in system software.(Forester is a joint work with Peter Habermehl from LIAFA, Paris, Lukas Holik and Adam Rogalewicz from FIT, Brno University of Technology, and Jiri Simacek from FIT BUT and VERIMAG, Grenoble. Predator is a joint work with Kamil Dudka and Petr Peringer from FIT BUT.)

Bio:

In this talk I will present results on the problem of scheduling tasksfor execution by a processor when the tasks can stochasticallygenerate new tasks. Tasks can be of different types, and each type hasa fixed, known probability of generating d tasks for each number d. Weare interested in the random variables modeling the time and spaceneeded to completely execute a task T, that is, to empty the pool ofunprocessed tasks assuming that initially the pool only contains thetask T. We derive tail bounds for the distributions of these variablesfor various classes of schedulers. We also provide bounds on theexpected values of these variables.

There are many web applications that require users to coordinate and communicate. Friends want to coordinate travel plans, students want to jointly enroll in the same set of courses, and busy professionals want to coordinate their schedules. These tasks are difficult to program using existing abstractions provided by database systems since they all require some type of coordination between users. However, this type of information flow is fundamentally incompatible with classical isolation in database transactions. In this talk, I will argue that it is time to look beyond isolation towards principled and elegant abstractions that allow for communication and coordination between some notion of (suitably generalized) transactions. This new area of declarative data-driven coordination is motivated by many novel applications and is full of challenging research problems. This talk describes joint work with Gabriel Bender, Nitin Gupta, Christoph Koch, Lucja Kot, Milos Nikolic, and Sudip Roy.

Bio:
Johannes Gehrke is a Professor in the Department of Computer Science at Cornell University. Johannes' research interests are in the areas of database systems, data mining, data privacy, and applications of database and data mining technology to marketing and the sciences. Johannes has received a National Science Foundation Career Award, an Arthur P. Sloan Fellowship, an IBM Faculty Award, the Cornell College of Engineering James and Mary Tien Excellence in Teaching Award, the Cornell University Provost's Award for Distinguished Scholarship, a Humboldt Research Award from the Alexander von Humboldt Foundation, and the 2011 IEEE Computer Society Technical Achievement Award. He is the author of numerous publications on data mining and database systems, and he co-authored the undergraduate textbook Database Management Systems (McGrawHill (2002), currently in its third edition), used at universities all over the world. Johannes is also an Adjunct Faculty Member at the University of Tromso in Norway. Johannes was co-Chair of the 2003 ACM SIGKDD Cup, Program co-Chair of the 2004 ACM International Conference on Knowledge Discovery and Data Mining (KDD 2004), Program Chair of the 33rd International Conference on Very Large Data Bases (VLDB 2007), and Program co-Chair of the 28th IEEE International Conference on Data Engineering (ICDE 2012). From 2007 to 2008, he was Chief Scientist at FAST, A Microsoft Subsidiary.

Applications in many different areas of computer science are required to make discrete decisions under uncertainty. Under uncertainty, the individual decisions made by a program are inevitably nondeterministic. A serious implication of this is that the decisions made by the program at different points of an execution may not even be consistent with each other. As a result, a program that is otherwise correct may execute along paths that would not be executed {\em on any input} in the program's usual semantics, and violate essential program invariants on the way.The property of em robustness asserts that a decision-making program does not suffer from the above kind of violations. In this paper, we present a program analysis to verify that a program P is robust in this sense. Our analysis constructs a decision monitor that observes the decisions made along executions of P and derives every corollary of these decisions. The problem of proving P robust is reduced to assertion checking in the product of P and this monitor.We apply our analysis to the domain of geometric computations, where typical programs make boolean decisions in the presence of numerical uncertainty. Robustness is known to be a critical and frequently-violated correctness property in this domain---for example, violation of robustness can cause everyday algorithms for computing convex hulls or triangulations to crash, go into infinite loops, or violate essential postconditions. While there is alarge body of work on robust geometric computation, ours is the first attempt at static verification of robustness of geometric programs. An evaluation using a suite of well-known geometric algorithms demonstrates the utility of our method.

In a process algebra with hiding and recursion it is possible to createprocesses which compute internally without ever communicating with theirenvironment. Such processes are said to diverge or livelock. We show howit is possible to conservatively classify processes as livelock-freethrough a static analysis of their syntax. In particular, we present acollection of rules, based on the inductive structure of terms, whichguarantee livelock-freedom of the denoted process. This gives rise to analgorithm which conservatively fl ags processes that can potentiallylivelock. We illustrate our approach by applying both BDD-based andSAT-based implementations of our algorithm to a range of benchmarks, andshow that our technique in general substantially outperforms the modelchecker FDR whilst exhibiting a low rate of inconclusive results.
Joint work with Joel Ouaknine, James Worrell and A. W. Roscoe.

The talk surveys recent results about infinite-state Markov chains and stochastic games generated by automata with one or more counters. Special attention will be devoted to stochastic one-counter automata and their basic properties such as termination probability or expected termination time. We also present some fresh (unpublished) results about one-counter Markov decision processes and non-stochastic games with multiple counters.

Interpolation is an important technique in verification and static analysis of programs. In particular, interpolants extracted from proofs of various properties are used in invariant generation and bounded model checking. A number of recent papers studies interpolation in various theories and also extraction of smaller interpolants from proofs. In particular, there are several algorithms for extracting of interpolants from so-called local proofs.

In this talk we describe a technique of minimising interpolants based on transformations of what we call the "grey area" of local proofs. We also present how to translate arbitrary proofs, under certain common conditions, into local ones.

Unlike many other interpolation techniques, our technique is very general and applies to arbitrary theories. Our approach is implemented in the theorem prover Vampire and evaluated on a large number of benchmarks coming from first-order theorem proving and bounded model checking using logic with equality, uninterpreted functions and linear arithmetic. Our experiments demonstrate the power of the new techniques: for example, it is not unusual that our proof transformation gives more than a tenfold reduction in the size of interpolants.

This is a joint work with Krystof Hoder and Andrei Voronkov (The University of Manchester).

The decade of genomic revolution following the human genome's sequencing has produced significant medical advances, and yet again, revealed how complicated human biology is, and how much more remains to be understood. Biology is an extraordinary complicated puzzle; we may know some of its pieces but have no clue how they are assembled to orchestrate the symphony of life, which renders the comprehension and analysis of living systems a major challenge. Recent efforts to create executable models of complex biological phenomena - an approach we call Executable Biology - entail great promise for new scientific discoveries, shading new light on the puzzle of life. At the same time, this new wave of the future forces computer science to stretch far and beyond, and in ways never considered before, in order to deal with the enormous complexity observed in biology. This talk will focus on our recent success stories in using formal methods to model cell fate decisions during development and cancer, and on going efforts to develop dedicated tools for biologists to model cellular processes in a visual-friendly way.

Human ventricular cells have currently more then ten increasingly detailed differential equations models (DEM), ranging from four variables and 27 parameters to more than 90 variables and hundreds of parameters. The detailed DEMs encapsulate the most up-to-date knowledge about the ionic processes involved at the intra and inter cellular level. While their differential equations are relatively simple (often of the law of mass action type) the sheer number of variables and parameters they contain, makes their analysis and even realistic 3D simulation intractable. It is therefore necessary, to map such DEMs to reduced order DEMs, whose analysis is still tractable. Our preliminary work shows that achieving such a map is possible: one uses simplifying assumptions to systematically eliminate variables whose behavior is not observable in the property of interest. For example, one can reduce the number of variables of the most up-to-date description of the sodium channel by assuming that its subunits are independent (Hodgkin-Huxley assumption) and by observing the overall open-close probability of the channel only.

Even with impressive advances in automated formal methods, certain problems in system verification and synthesis remain challenging. Examples include the verification of quantitative properties of software involving constraints on timing and energy consumption, and the automatic synthesis of systems from specifications. The challenges mainly arise from three sources: environment modeling, incompleteness in specifications, and the complexity of underlying decision problems.

In this talk, I will present SCIDUCTION, a methodology to tackle these challenges. Sciduction combines inductive inference (learning from examples), deductive reasoning (such as SAT/SMT solving), and structure hypotheses. We have demonstrated several applications of sciduction including timing analysis of embedded software, synthesis of loop-free programs, synthesis from temporal logic (LTL), term-level verification of hardware (RTL) designs, and switching logic synthesis of hybrid systems. This talk will present some core theory, a couple of illustrative applications, and directions for future work.

Biography: Sanjit A. Seshia is an Associate Professor in the Department of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He received an M.S. and Ph.D. in Computer Science from Carnegie Mellon University, and a B.Tech. in Computer Science and Engineering from the Indian Institute of Technology, Bombay. His research interests are in dependable computing and computational logic, with a current focus on applying automated formal methods to problems in embedded systems, electronic design automation, computer security, and program analysis. His work on the UCLID verifier and decision procedure helped pioneer the area of satisfiability modulo theories (SMT) and SMT-based verification. He is co-author of a textbook on embedded systems. He has received a Presidential Early Career Award for Scientists and Engineers (PECASE), an Alfred P. Sloan Research Fellowship, and the School of Computer Science Distinguished Dissertation Award from Carnegie Mellon University.

The challenging task of Byzantine self-stabilizing pulse synchronization requires that, in the presence of a minority of nodes that are permanently maliciously faulty, the non-faulty nodes must start firing synchronized pulses in a regular fashion after a finite amount of time, regardless of the initial state of the system. We study this problem under full connectivity in a model where nodes have local clocks of unknown, but bounded drift, and messages are delayed for an unknown, but bounded time.

We present a generic scheme that, given a synchronous consensus protocol P, defines a self-stabilizing pulse synchronization algorithm A(P). If P terminates within R rounds (deterministically or with high probability), A(P) stabilizes within O(R) time (deterministically or with high probability, respectively). Utilizing different consensus routines, our transformation yields various improvements over previous techniques in terms of stabilization time and bit complexity. Finally, we sketch how to establish the abstraction of synchronous, integer-labeled rounds on top of pulse synchronization, at essentially the same complexity bounds. We will discuss our approach and its merits assuming no previous knowledge on the problem, however, basic familiarity with consensus will be beneficial.

Short bio: Christoph Lenzen received a diploma degree in Mathematics from the University of Bonn, Germany, and subsequently performed his graduate studies in Distributed Computing in the group of Professor Roger Wattenhofer at ETH Zurich. In 2011, he was a postdoctoral Fellow at the Hebrew University of Jerusalem, with Danny Dolev. Currently, he is a postdoctoral fellow at the Weizmann Institue of Science, with Professor David Peleg. His research interests cover distributed computing in a wider sense, including topics such as randomized load balancing, graph algorithms, and clock synchronization. He published e.g. at PODC, SPAA, FOCS, and STOC, and in JACM. In 2009, he and his coauthors received the PODC best paper award for their work on gradient clock synchronization.

Linear max-plus dynamical systems describe the time behavior of a large variety of distributed systems. These include transportation networks, manufacturing plants, and network synchronizers, as well as link reversal algorithms for routing and scheduling. It is known that these systems show a periodic behavior after an initial transient phase. Assessment of the length of this transient phase provides important information on complexity measures of such systems. By identifying parameters in a graph representation of these systems, we give the first potentially subquadratic upper bounds on the transient, which can help during system design.

I will describe a new approach to the old problem of automatic temporal property verification. As well as leading to dramatic performance improvements over existing techniques, this approach also brings some light to a couple of age-old questions.

Bio: Dr. Byron Cook is a Principal Researcher at Microsoft Research Cambridge, as well as Professor of Computer Science at University College London. His research interests focus on formal verification, theorem proving, operating systems and biology. Byron is particularly well known for his work on the Terminator program termination prover as well as the SLAM software model checker.

Several applications from program analysis, design and testing rely critically on solving SMT problems. Many applications build on top of SMT solvers in sophisticated ways by carefully crafting the solver interaction. Many applications at their core solve for recursive predicates and so far SMT solvers have no direct support for these. This talk presents a new extension of Z3 and an algorithm, PDR extended to SMT domains, for handling recursive predicates. The IC3 algorithm was recently introduced for proving properties of finite state reactive systems. It has been applied very successfully to hardware model checking.

We provide a specification of the algorithm using an abstract transition system and highlight its dual operation: model search and conflict resolution. We then generalize it along two dimensions. Along one dimension we address nonlinear fixed-point operators (push-down systems) and evaluate the algorithm on Boolean programs. In the second dimension we leverage proofs and models and generalize the method to Boolean constraints involving theories. A side-effect of our approach is a model-based method for computing interpolants of recursion-free Horn clauses for linear real arithmetic. The method also produces a decision procedure for timed push-down systems.

The talk is based on joint work with Krystof Hoder that will appear at SAT 2012.

Equivalence checking problem is that of verifying whether two given programs have the same behavior. By formalizing the terms "program" and "behavior" in different bases, we obtain numerous variants of this problem. It has been always regarded as one of the most fundamental problems in computer science which has a wide range of applications in software engineering. The talk provides a comprehensive survey of significant achievements in the study of equivalence checking problem for various models of programs since the early 50-s XX.

This talk reports on a true RiSE cooperation. I will present joint work with Thomas A. Henzinger and Ali Sezgin from IST Austria as well as Christoph M. Kirsch and Hannes Payer from the University of Salzburg. The cooperation was initiated during one of the RiSE meetings.

There is a trade-off between performance and correctness in implementing concurrent data structures. Better performance may be achieved at the expense of relaxing correctness, by redefining the semantics of data structures. We address such a redefinition of data structure semantics and present a systematic and formal framework for obtaining new data structures by quantitatively relaxing existing ones. We view a data structure as a sequential specification S containing all "legal" sequences over an alphabet A of method calls. Relaxing the data structure corresponds to defining a distance from any sequence over A to the sequential specification: the relaxed sequential specification Sk contains all sequences over A within distance k from S. In contrast to other existing work, our relaxations are semantic (distance in terms of data structure states).

As an instantiation of our framework, we present a simple yet generic relaxation scheme. We show that this relaxation, when further instantiated on queues, stacks, and priority queues, amounts to tolerating bounded out-of-order behavior, which cannot be captured by a purely syntactic relaxation (distance in terms of sequence manipulation, e.g. edit distance). We also present various concurrent implementations of queue, stack, and priority queue relaxations and argue that bounded relaxations provide the means for trading correctness for performance in a controlled way. The relaxations are monotonic which further highlights the trade-off: increasing k increases the number of permitted sequences, which increases the performance.

Program verification is the only way to be certain that a given piece of software is free of (certain types of) errors --- errors that could otherwise disrupt operations in the field. To date, formal verification has been done manually, by specially-trained engineers. Labor costs have heretofore made formal verification too costly to apply beyond small, critical software components.

Our goal is to make verification more cost-effective by reducing the skill set required for program verification and increasing the pool of people capable of performing program verification. Our approach is to transform the verification task (a program and a goal property) into a visual puzzle task --- a game --- that gets solved by people. The solution of the puzzle is then translated back into a proof of correctness. The puzzle is engaging and intuitive enough that ordinary people can through game-play become experts.

This talk presents the status of the Verification Games project and our Pipe Jam prototype game.

A pluggable type system extends a language's built-in type system to confer additional compile-time guarantees. We will explain the theory and practice of pluggable types. The material is relevant for researchers who wish to apply type theory, and for anyone who wishes to increase confidence in their code. After this session, you will have the knowledge to: analyze a problem to determine whether pluggable type-checking is appropriate; design a domain-specific type system; implement a simple type-checker (in as little as 4 lines of code!); scale a simple type-checker to more sophisticated properties; and better appreciate both object-oriented types and flexible verification techniques.

While the theory is general, our hands-on exercises will use a state-of-the-art system, the Checker Framework, that works for the Java language, scales to millions of lines of code, and is being adopted in the research and industrial communities. Such a framework enables researchers to easily evaluate their type systems in the context of a widely-used industrial language, Java. It enables non-researchers to verify their code in a lightweight way and to create custom analyses. And it enables students to better appreciate type system concepts.

Hybrid systems are those which exhibit both discrete "jump" and continuous "flow" dynamics. Their importance---as components of cyber-physical systems---is paramount now that more and more physical systems (cars, airplanes, etc.) are controlled with computers.

There are naturally two directions towards the study of hybrid systems: control theory (typically continuous) and formal verification (typically discrete). For us from the formal verification community, therefore, the big challenge is how to incorporate continuous "flow" dynamics. Many existing techniques---such as hybrid automaton or Platzer's differential dynamic logic---include differential equations explicitly. This incurs a difficult (and very interesting) question of how to handle differential equations.

In our project we take a different path of turning flow into jump---more precisely into infinitely many jumps each of which is infinitesimal (i.e. infinitely small). This makes everything discretejump dynamics, to which all the discrete techniques accumulated in the community of formal verification readily apply. This venture is mathematically supported by *nonstandard analysis*, where we canrigorously speak about infinites and infinitesimals.

In the talk I will lay out: 1) our framework of a while-language and a Hoare-style program logic, augmented with an infinitesimal constant, for modeling and verification of hybrid systems; 2) how discrete verification techniques can be *transferred*, as they are, to hybrid applications, via the celebrated *transfer principle* in nonstandard analysis; and 3) the overview of our prototype automatic prover.

The talk is based on the joint work with Kohei Suenaga, Kyoto University.

A major result concerning temporal logics is Kamp's Theorem (1968) which states that the pair of modalities "until" and "since" is expressively complete for the first-order fragment of the monadic logic over the linear time canonical models.

We provide a simple proof of Kamp's theorem.

Developing modern software applications typically involves composing functionality from existing libraries. This task is difficult because libraries may expose many methods to the developer. To help developers in such scenarios, in this talk I will present a technique that synthesizes and suggests valid expressions of a given type at a given program point. As the basis of our technique we use type reconstruction for lambda calculus with subtyping. We show that the inhabitation problem in the presence of subtyping remains PSPACE-complete. We introduce a succinct representation for type judgements that merges types into equivalence classes to reduce the search space. We introduce a proof rule on this succinct representation of types and show that it is sound and complete for inhabitation. We implemented the resulting algorithm and deployed it as a plugin for the Eclipse IDE for Scala.

~This is a joint work with Tihomir Gvero and Viktor Kuncak~

Localizing the cause of an error in an error trace is one of the most time-consuming aspects of debugging. In this talk, I present a novel technique to automate this task. For this purpose, I introduce the concept of "error invariants". An error invariant for a position in an error trace is a formula over program variables that over-approximates the reachable states at the given position while only capturing states that will still produce the error, if execution of the trace is continued from that position. Error invariants can be used for slicing error traces and for obtaining concise error explanations. I will present an algorithm that computes error invariants from Craig interpolants, which we construct from proofs of unsatisfiability of formulas that explain why an error trace violates a particular correctness assertion. This is joint work with Evren Ermis and Martin Schaef.

In this talk we introduce a new method for solving systems of linear inequalities and linear optimisation. The algorithm incorporates many state-of-the-art techniques from DPLL-style reasoning. We prove soundness, completeness and termination of the method.

Interpreters inhabit a sweet spot on the performance/price curve of programming language implementation. This means that it is cheaper toimplement an interpreter than a compiler, but on the other hand thatcompilers are usually faster than interpreters. This is particularlytrue for high abstraction-level interpreters, where many traditionaloptimizations are not effective. Consequently, such interpreters havea bad reputation for being too slow.

This talk focuses on a previously successful line of research inpurely interpretative optimizations carried out at the Compilers andLanguages group of the Institute of Computer Languages, and presentsnew results of continuing this line of research. In particular, wegive a brief overview of purely interpretative inline caching usingquickening and show how to leverage this foundation for a noveladaptive optimization: native machine-abstraction execution, or NAMASTE forshort. We have implemented NAMASTE and report that this techniqueboosts our previously maximum reported speedup by more than 40%: froma factor of up to 2.4 to a factor of up to 3.4. Since this techniqueis purely interpretative, too, it offers the usual benefits ofinterpreters: ease of implementation, portability, and---compared to ajust-in-time compiler, constant and low memory usage.

We describe a novel technique for bounded analysis of asynchronousmessage-passing programs with ordered message queues. Our boundingparameter does not limit the number of pending messages, nor thenumber of “context-switches” between processes. Instead, we limit thenumber of process communication cycles, in which an unbounded numberof messages are sent to an unbounded number of processes across anunbounded number of contexts. We show that remarkably, despite thepotential for such vast exploration, our bounding scheme gives rise toa simple and efficient program analysis by reduction to sequentialprograms. As our reduction avoids explicitly representing messagequeues, our analysis scales irrespectively of queue content andvariation.

I will talk about notions of computation in a model of set theory extended by "atoms". Sets with atoms where introduced in 1922 by Fraenkel in order to construct a model of a variant of the Zermelo-Frankel axioms in which the axiom of choice fails. They where rediscovered many times under various names (sets with urelements, Fraenkel-Mostowski models, nominal sets, permutation models); in automata theory they appeared in the context of register automata over data words, in a paper by Bojańczyk, Klin, Lasota from LICS'11.

I will recall the basic notions of this set theory. Afterwards, I will define several models of computation based on sets with atoms, including automata, Turing machines and imperative while-programs. Finally, I will sketch a proof that P is not equal to NP for this model of computation.More precisely, I will show a language that is in NP, but is not recognizable by any deterministic Turing machine (even with unlimited time resources). This language is related to the Cai-Fürer-Immerman construction known from finite model theory.

A fundamental task in distributed systems (like the Internet) is to determine efficient routing paths between all pairs of nodes. For efficiency reasons, one frequently resorts to constructing approximate shortest path based on new node labels that encapsulate some hints on a node's location in its name. While the optimal trade-off between routing tables size and approximation ratio is fairly well-understood in this setting, little attention has been paid to quick construction of such tables in a distributed manner. This is crucial, since usually it is impractical - or even infeasible - to aggregate the topology of large systems in a single location, and in a dynamic environment the solution might be already outdated before it can be put to use.

In this talk, we present a novel technique for distributed routing table construction running in O(n^(1/2+eps)+D) rounds of communication (up to polylogarithmic factors in n), where n is the number of nodes in the system and D the diameter of the communication graph. Our algorithm uses messages of size O(log n) and guarantees approximation ratio O(eps^(-1) log eps^(-1)). Under these constraints, our solution is near-optimal: Every algorithm using messages of size O(log n) and achieving a polylogarithmic approximation must run for Omega(n^(1/2)+D) rounds. In constrast, previous algorithms incur running times of Omega(n) even in graphs of constant diameter. Our approach yields improved distributed algorithms for a number of related problems, including distance approximation and Generalized Steiner Forest approximation.

The subject of this talk is to present regular cost functions, a quantitative extension to the notion of regular languages (of words, trees, finite or infinite) for which powerful decision procedures are available.

We will motivate this presentation starting from an open question (FOSSACS 2011) of Rabinovich and Velner concerning an extension of Church synthesis problem in which Player I is allowed, afterward, to change a bounded number of moves he played. Formally, the question is as follows: two players, I and II, which alternatively play a bit, thus producing an infinite play.This play is said n-winning if, up to modifying n of the bits player I has played so far, the play belongs to a given regularlanguage of infinite words. The problem is to decide if there is a natural number n such that Player I can guarantee n-winning.

We will see that this question is naturally (and positively) solved using regular cost functions over infinite words.

Logical methods can be used to unify results for individual graph-theoretic objects, by providing meta-theorems which apply to all suchobjects definable in an appropriate logic. In this talk we discuss graphproperties and graph polynomials definable in First Order Logic and MonadicSecond Order Logic in terms of their definability and combinatorialmeta-theorem. In particular, we show a method of proving non-definabilityusing connection matrices. We extend the results for graph properties byshowing a Feferman-Vaught type theorem for First Order Logic extended withcounting quantifiers.