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.
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.
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.