Every day, we make sequences of decisions to accomplish our goals, and we attempt to achieve these goals in the most favorable way. In many aspects of life, such as in security or economy, the optimality of these decisions is critical, and a computational support for decision making is thus needed. Sequential decision making is, however, computationally challenging in the presence of uncertainty (partially observable Markov decision processes) or even adversaries (partially observable stochastic games). We provide a game theoretic model of one-sided partially observable stochastic games which is motivated by problems arising mainly in security. It captures both the uncertainty of the decision maker and the adversarial nature of the problem into account. Our framework assumes two players where one player is given the advantage of having perfect information. We show that we can solve such games in the similar fashion as one solves POMDPs using the value iteration algorithm, including its more practical approximate variants based on point-based updates of the value function.

Virtually all real-valued computations are carried out using floating-point data types and operations. With the current emphasis of system development often being on computational efficiency, developers as well as compilers are increasingly attempting to optimize floating-point routines. Reasoning about the correctness of these optimizations is complicated, and requires error analysis procedures with different characteristics and trade-offs. In my talk, I will motivate the need for such analyses. Then, I will present both a dynamic and a rigorous static analysis we developed for estimating errors of floating-point routines. Finally, I will describe how we extended our rigorous static analysis into a procedure for mixed-precision tuning of floating-point routines.

Short bio:

Zvonimir Rakamaric is an assistant professor in the School of Computing at the University of Utah. Prior to this, he was a postdoctoral fellow at Carnegie Mellon University in Silicon Valley, where he worked closely with researchers from the Robust Software Engineering Group at NASA Ames Research Center to improve the coverage of testing of NASA’s flight critical systems. Zvonimir received his bachelor’s degree in Computer Science from the University of Zagreb, Croatia; he obtained his M.Sc. and Ph.D. from the Department of Computer Science at the University of British Columbia, Canada.

Zvonimir‘s research mission is to improve the reliability and resilience of complex software systems by empowering developers with practical tools and techniques for analysis of their artifacts. He is a recipient of the NSF CAREER Award 2016, Microsoft Research Software Engineering Innovation Foundation (SEIF) Award 2012, Microsoft Research Graduate Fellowship 2008-2010, Silver Medal in the ACM Student Research Competition at the 32nd International Conference on Software Engineering (ICSE) 2010, and the Outstanding Student Paper Award at the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2007.

For more information about Zvonimir, visit www.zvonimir.info.

Probabilistic programming is en vogue. It is used to describe

complex Bayesian networks, quantum programs, security protocols and

biological systems. Programming languages like C, C#, Java, Prolog,

Scala, etc. all have their probabilistic version. Key features are

random sampling and means to adjust distributions based on obtained

information from measurements and system observations. We show some

semantic intricacies, argue that termination is more involved than the

halting problem, and discuss recursion as well as run-time analysis.

Constrained counting and sampling are two fundamental problems in Computer Science with numerous applications, including network reliability, privacy, probabilistic reasoning, and constrained-random verification. In constrained counting, the task is to compute the total weight, subject to a given weighting function, of the set of solutions of the given constraints . In constrained sampling, the task is to sample randomly, subject to a given weighting function, from the set of solutions to a set of given constraints.

In this talk, I will introduce a novel algorithmic framework for constrained sampling and counting that combines the classical algorithmic technique of universal hashing with the dramatic progress made in Boolean reasoning over the past two decades. This has allowed us to obtain breakthrough results in constrained sampling and counting, providing a new algorithmic toolbox in machine learning, probabilistic reasoning, privacy, and design verification . I will demonstrate the utility of the above techniques on various real applications including probabilistic inference, design verification and our ongoing collaboration in estimating the reliability of critical infrastructure networks during natural disasters.

Bio:

Kuldeep Meel is a final year PhD candidate in Rice University working with Prof. Moshe Vardi and Prof. Supratik Chakraborty. His research broadly lies at the intersection of artificial intelligence and formal methods. He is the recipient of a 2016-17 IBM PhD Fellowship, the 2016-17 Lodieska Stockbridge Vaughn Fellowship and the 2013-14 Andrew Ladd Fellowship. His research won the best student paper award at the International Conference on Constraint Programming 2015. He obtained a B.Tech. from IIT Bombay and an M.S. from Rice in 2012 and 2014 respectively. He co-won the 2014 Vienna Center of Logic and Algorithms International Outstanding Masters thesis award.

Guarded protocols, as introduced by Emerson and Kahlon (2000), describe concurrent systems where transitions of processes are enabled or disabled depending on the existence of other processes in certain local states. Cutoff results reduce reasoning about systems with an arbitrary number of processes to systems of a determined, fixed size. Our work is based on the observation that the existing cutoff results are i) of limited use for liveness properties because the reductions do not preserve fairness, and ii) in many cases give a prohibitively large cutoff. We provide new cutoff results that work under fairness assumptions, and prove tightness or asymptotic tightness for cutoffs that only depend on the size of the process templates. I will also report on ongoing work to obtain smaller cutoffs by considering additional static properties of the process templates, such as the number of different guards that are used in the template.

Automata learning, or regular inference, is a widely used technique for creating an automaton model from observations. In recent years, it has been successfully applied to the verification of security protocols, hardware, and software systems. The original algorithm L* works for deterministic finite automata, and is only capable of learning control-flow models.

In this talk I will present an extension of L* to learn combined control/data-flow models in the form of nominal automata, which are acceptors of languages over infinite (structured) alphabets. After recalling L*, I will briefly present the theory of nominal sets. Then I will show how this theory enables extending L* to infinite alphabets in a seamless way, with almost no modifications to the original code. Finally, I will give a short demo of a tool based on this work, currently being developed at UCL.

Many of the challenging problems in verification and synthesis algorithms are naturally phrased in terms of quantified formulas. Our ability to solve these problems, however, is still unsatisfactory. Even when we take a look at the most basic logical theory with quantification, quantified boolean formulas (QBF), the most effective approach are CEGAR-style algorithms. But CEGAR is a generic algorithmic scheme, which means that we are not yet able to exploit the structure of quantified problems.

In this talk I will discuss some of the fundamental limits of CEGAR-style algorithms and present a novel approach to solve quantified boolean formulas (currently restricted to one quantifier alternation, i.e. 2QBF). The algorithm adds new constraints to the formula until the constraints describe a unique Skolem function – or until the absence of a Skolem function is detected. Backtracking is required if the absence of Skolem functions depends on the newly introduced constraints. The algorithm can be best understood when compared to search algorithms for SAT. We will discuss how to lift propagation, decisions, and conflicts from values (SAT) to Skolem functions (QBF). The algorithm significantly improves over the state of the art in terms of the number of solved instances, solving time, and the size of certificates.

Although not the most popular feature of Java's generics, bounded wildcards have their uses. On the negative side, bounded wildcards render type checking undecidable. On the positive side, bounded wildcards let us encode any computation at compile time; so, Java's type checker can recognize any recursive language. The first part of the talk will review how bounded wildcards are used in the implementation of Java's standard library. The second part of the talk will review the proof that bounded wildcards render subtype checking undecidable. Radu Grigore is a lecturer at University of Kent and an anagram of Argued Rigor.

In systematic testing of concurrent systems, if the goal is to expose

bugs of “small depth,” one only needs to test a hitting family of

schedules. More precisely, in a system given as a partially ordered set

of events, we say a bug has depth $d$ if it is exposed by ordering $d$

specific events in a particular way, irrespective of how the other

events are ordered. A set of schedules is called a $d$-hitting family if

for every admissible ordering of $d$ events, there is a schedule in the

family that schedules these events in this order. We showed previously

that when the partial order forms a tree, we can explicitly construct

hitting families of size polynomial in the height of the tree, and

therefore polylogarithmic in the number of events when the tree is balanced.

In the follow-up work, which I will present in this talk, we consider an

extended setting where an event can be executed correctly or with a

fault. A fault does not necessarily entail a bug, as the developer may

have included fault-handling mechanisms. Faults merely mean that the

space of possible schedules is now much larger. Our preliminary results

show that even with faults, there are hitting families of size

polylogarithmic in the number of events.

In the talk I will also present COFIT—Concurrency and Fault Injection

Testing framework for .NET applications, which incorporates

constructions of hitting families.