In this talk, we will talk about decision problems for linear recurrence sequences (LRS), which are generalizations of the Fibonacci sequence. Starting from the long-standing open Skolem problem (which asks if a given LRS has a zero), we will look at several variants and survey some recent results in this area. Further, we will motivate these highly mathematical problems by showing how they occur rather naturally in the domains of program termination and probabilistic verification.
We present a sampling of some techniques for reasoning about concurrent programs. We begin with the classical extensions of Hoare logic for concurrent programs, by Owicki-Gries and others. We then move on to recent and more automatable approaches. These include Sinha and Wang's data-centric approach to bounded checking, data-flow analysis based techniques of Jhala and others, and finally abstraction-refinement based techniques of Kincaid and others.
Can one decompose a finite automaton into a combination of simple automata, which together manage to simulate its behaviour? This question was answered positively by Kenneth Krohn and John Rhodes (PhD theses 1962, abstract 1963, full paper 1965) using what they called a "prime factorization". Another "holonomy" decomposition was given by Paul Zeiger (FOCS 1965, journal paper 1967, errata 1967).
Usually the question is transformed into the following: can one decompose a finite monoid into wreath products of simple monoids which divide it? Since the Jordan-Holder theorem from group theory breaks up a finite group using its composition series into simple groups, one can use it and concentrate on how to decompose a groupfree monoid. The only "prime" needed for this part is a three-element monoid called U2. That is, any groupfree monoid can be simulated by wreath products of copies of U2.
Groupfree monoids were studied by Marcel-Paul Schutzenberger in 1965. A new proof of Schutzenberger's theorem was found by Thomas Wilke in 1997. Ideas from this proof have led to a new proof of the Krohn-Rhodes theorem (published in 2012).
The talk will concentrate on the concepts used (monoids, division, wreath products), rather than the proofs themselves.
Parameterized concurrent programs are a class of programs where same code is executed by an unbounded number of threads. Device drivers and concurrent data structures are two most common examples of parameterized concurrent programs. In this talk I present the recent work published in POPL'12 (Verification of Parameterzied concurrent programs by modular reasoning about data and control) on the verification of such programs. I also plan to cover a paper on cutoff detection based approach for the verification of such programs(Dynamic cutoff detection in parameterized concurrent programs-CAV'10). Let S(P)n be the set of states reachable by executing n copies (to simulate n threads executing the same program) of a finite state program P. Cutoff of P is a number n such that the for all m>n S(P)m=S(P)n, i.e. to find out all reachable states for any number of threads it is sufficient to explore the set of states reachable by n threads.
References:
We survey a variety of results on the verification of CFSMs (communicating finite state machines), MPDSs (Multi-pushdown systems) and CRPs (communicating recursive processes) in literature. We hope to convince you that a very simple idea underlies all of these results.
Probabilistic models, particularly those with causal dependencies, can be succinctly written as probabilistic programs. Recent years have seen a proliferation of languages for writing such probabilistic programs, as well as tools and techniques for performing inference over these programs In this talk, we show that static and dynamic program analysis techniques can be used to infer quantities of interest to the machine learning community, thereby providing a new and interesting domain of application for program analysis. In particular, we show that static analysis techniques inspired by dataflow analysis and iterative refinement techniques can be used for Bayesian inference. We also show that dynamic analysis techniques inspired by directed testing and symbolic execution can be used for sampling probabilistic programs.
In his classical result, Kamp Showed that the (qualitative) linear temporal logic LTL[U,S] is expressively complete w.r.t. FO[<] over real-time. However, extending Kamp's theorem to quantitative real-time logics has been challenging. Metric Temporal Logic MTL[U_I,S_I] is a prominent real-time logic which specifies quantitative timing properties of timed behaviours. The formulae use non-negative integer constants (or infinity) as end-points of intervals I. A result of Hirshfeld and Rabinovich [3] establishes that MTL (with integer constants) is less expressive than FO[<,+1]. This talk will survey two recent extensions of MTL which for which the 'Kamp theore'” can be retrieved. Hunter, Ouaknine and Worrell [1] have shown that MTL with rational time constants is expressively complete for FO[<,+q] where q in Q (rationals). Rabinovich has shown that MTL[U_I,S_I,int] containing a predicate int, which holds exactly at integral time points, is expressively complete for FO[<,+1,int(x)]. In this talk, we will provide an overview of these results.
References:
There has been considerable interest in Software Transactional Memory in recent years. The reason for rise in STM is due to rise of multicore computers. To fully utlize the power of these machines, applications need to be able to harness the parallelism of the underlying hardware. This is commonly achieved using multi-threading. Yet writing correct and scalable multi-threaded programs is far from trivial. In multi-threaded programs sets of semantically related actions may need to execute in mutual exclusion to avoid semantic inconsistencies.
Traditionally, multi-threaded programs were developed in conjunction with locks to address these issues. But programming with locks has many disadvantages such as deadlocks, priority inversion etc. and makes it difficult to build scalable software systems. Importantly, lock based software components are difficult to compose i.e. build larger software systems using simpler software components. Composition of software components is a very important property which is the basis of modular programming. Nesting of transactions is a way of achieving Composition. STM systems propose natural way of achieving this. at achieving this.
In this talk, I will discuss about the various open research directions in the area of Sofware Transactional Memory.
Program slicing is an operation that for a given program P, and a program variable V, emits a (simplified) program P' that produces the same final value in V as P does for every possible input. There are many techniques in the literature for slicing, with varying degrees of precision (a technique is more precise if it produces a smaller sliced program P'). In this talk we will survey a few such techniques, with emphasis on recent techniques that aim for higher precision than traditional techniques.
The paper [1] reduces proving lock-freedom of a concurrent data-structure to modular thread local termination of concurrent programs in which each thread executes a finite number of data-structure operations. It introduces a compensation based quantitative reasoning technique for proving lock-freedom. This technique is formalised by extending Concurrent Separation Logic (CSL) for total correctness.
Linearizability of concurrent data structures is usually proved by monolithic simulation arguments relying on identifying the so-called linearisation points. However, for several data-structures such as the Herlihy-Wing Concurrent Queue, the task of identifying linearisation points is non-trivial. Paper [2] proposes a modular way of checking linearizability of concurrent queue implementations. It reduces the problem of proving linearizability to establishing four basic properties each of which can be proved independently by much simpler arguments.
References:
Logic provides a framework for reasoning with entities and relationships between them. Probability gives the tool to explicitly deal with uncertainty in the data. Last decade has seen a surge of research in the area of statistical relational learning (SRL) which aims to combine the power of both logic and probability. Markov logic (Richardson and Domingos 2006) achieves this merger by representing the underlying domain using weighted first-order logic formulas which can be seen as defining templates for constructing ground Markov networks. In this talk, I will present the motivation and theory behind Markov logic. I will also describe an illustrative application of Markov logic to the problem of abductive plan recognition.
We consider the reachability problem for timed automata (TA) and probabilistic timed automata (PTA). For TA, the reachability question asks if there exists a run from its initial state to a given goal state. For PTA, the question asks for the maximum probability to reach a given goal state from its initial state. In this talk, we look at state-of-the-art algorithms for these two problems.
Courcelle [3] proposed the idea of using logic, in particular Monadic second-order logic (MSO), to define graph to graph transformations. Transducers, on the other hand, are executable machine models to define transformations, and are typically studied in the context of string-to-string transformations. Engelfriet and Hoogeboom [4] studied two-way finite state string-to-string transducers and showed that their expressiveness matches MSO-definable transformations (MSOT). Alur and Cerny [1,2] introduced streaming transducers---one-way transducers equipped with multiple registers that can store output strings, as an equi-expressive model. Natural generalizations of streaming transducers to string-to-tree and infinite-string-to-string cases preserve MSO-expressiveness. In this talk we survey some key results related to streaming string transducers, and discuss some interesting open problems.
References:
High level specification notations that engineers find usable are important for the widespread acceptance and application of formal methods. Of late variants of Statecharts are gaining acceptance at least in the embedded domain. In this presentation we will introduce the Rhapsody variant of Statecharts and its semantics. We will also present EDT a tabular notation that has been developed by us and compare it with Statecharts.