Probabilistic programming is a fascinating new direction in programming.
FaceBook, Google and Microsoft, to mention a few, are investing lots of
research efforts in probabilistic programming. Nearly every programming
Prolog, C, Python, you name it, and — yes — even Excel has been
extended with features for randomness. These languages aim to make
probabilistic modeling and machine learning accessible to any
programmer, any user.
Probabilistic programs describe recipes on how to infer conclusions
about big data from a mixture of uncertain data and real-world
observations. Bayesian networks, a key model in decision making, are
simple instances of such programs. Probabilistic programs steer
autonomous robots and self-driving cars, are key to describe security
mechanisms, naturally encode randomised algorithms, and are rapidly
encroaching AI and machine learning.
In this talk, I will explain what probabilistic programming is, give a
historical perspective, describe its applications, and indicate what
formal methods can mean for probabilistic programs.
First-order logic with quantifiers is undecidable in general, but some expressive fragments have complete instantiation. This means, it is sufficient to instantiate the quantified formulas with a finite set of ground terms computed from the formula, and then solve the resulting quantifier-free conjunction with an SMT solver. A challenge is to select the relevant instances in order to avoid producing too many new formulas that slow down the solver.
In this talk we will present a new approach that treats quantified formulas in SMT solvers in the style of a theory solver in the DPLL(T) framework. This comprises methods to detect instances of quantified formulas that are in conflict with the current boolean assignment of the ground literals or lead to a ground propagation. In particular, we will discuss how E-matching, the most common heuristic method for quantifier instantiation in SMT solvers, can be used to find these specific instances.
The presented approach is work in progress. Future work encompasses combining the approach with model-based quantifier instantiation in order to get completeness for decidable fragments.
In traditional complexity theory, the complexity of computational problems is
measured as a function of the size of the input. Nevertheless, in many situations
of practical relevance, analyzing the complexity of a problem only taking the size
of the input into consideration may not reflect the difficulty of solving that particular
problem on practical instances. Indeed, there are plenty of examples where a problem
is NP-hard but which can be solved efficiently by standard algorithms on empirically
inspired benchmarks. In parameterized complexity theory, the complexity of a problem
is measured not only in terms of the size of the input but also in terms of additional parameters that try to capture structural properties of the problem in question. In some cases, parameterized complexity theory offers a reasonable explanation of why such problems are solvable efficiently in practice: very often on practical instances, the parameters of relevance have small magnitude.
Most work in parameterized complexity theory deals with showing that certain NP-complete problems can be solved efficiently when certain relevant parameters are fixed. Nevertheless, not much has been done in classifying the parameterized complexity of problems that extremely hard from the perspective of classical complexity. In this talk, I will discuss a framework that allows
one to bring traditional tools of parameterized complexity theory to the realm of proof theory. In particular, we will define a suitable notion of width for proofs and will show how to construct proofs of small width in polynomial time.
We present an algorithm for the automatic synthesis of polynomial invariants for probabilistic transition systems.
Our approach is based on martingale theory.
We construct invariants in the form of polynomials over program variables, which give rise to martingales.
These polynomials are program invariants in the sense that their expected value upon termination is the same as their value at the start of the computation.
By exploiting geometric persistence properties of the system,
we show that suitable polynomials can be automatically inferred using sum-of-squares optimisation techniques.
Verification of concurrent software is a notoriously difficult
subject, whose complexities stem from the inability of the
existing verification methods to modularize, and thus divide and
conquer the verification problem.
Dependent types are a formal method well-known for its ability to
modularize and scale complex mathematical proofs. But, when it
comes to programming, dependent types are considered limited to
the purely functional programming model.
In this talk I will present my recent work towards reconciling
dependent types with shared memory concurrency, with the goal of
achieving modular verification for the latter. Applying the
type-theoretic paradigm to concurrency have lead to interesting
reformulations of some classical verification ideas, and to the
discovery of novel and useful abstractions for modularizing the
In this talk, I will give a perspective on inference in Bayes’ networks
(BNs) using program verification. I will argue how weakest precondition
reasoning a la Dijkstra can be used for exact inference (and more). As
exact inference is NP-complete, inference is typically done by means of
simulation. I will show how by means of wp-reasoning exact expected
sampling times of BNs can be obtained in a fully automated fashion. An
experimental evaluation on BN benchmarks demonstrates that very large
expected sampling times (in the magnitude of millions of years) can be
inferred within less than a second. This provides a means to decide
whether sampling-based methods are appropriate for a given BN. The key
ingredients are to reason at program code in a compositional manner.
Automated invariant generation is a fundamental challenge in program analysis and verification, going back many decades, and remains a topic of active research. In this talk I’ll present a select overview and survey of work on this problem, and discuss unexpected connections to other fields including quantum computing, group theory, and algebraic geometry. (No previous knowledge of these fields will be assumed.)
The operation of traditional computer networks is known to be a difficult manual and error-prone task. Over the last years, even tech-savvy companies have reported major issues with their network, due to misconfigurations, leading to disruptive downtimes. As a response to the difficulty of maintaining policy compliance, and given the critical role that computer networks (including the Internet, datacenter networks, enterprise networks) play today, researchers have started developing more principled approaches to networking and specification. Over the last years, we have witnessed great advances in the development of mathematical foundations for computer networks and the emergence of high-level network programming languages such as NetKAT. While powerful, however, existing formal frameworks often come with potentially high (super-polynomial) running times — even without considering failure scenarios.
This talk first gives an overview of the “softwarization” trends in communicaiton networks and motivates why formal methods are currently the “hot topic” in this area. I will then present a what-if analysis framework which allows us to verify important properties such as policy compliance and reachability in communication networks in polynomial time, even in the presence of (multiple) failures. Our framework relies on an automata-theoretic approach, and applies both to the widely deployed MPLS networks as well as to the emerging Segment Routing networks. In addition to the theory underlying our approach (presented at INFOCOM 2018 together with Jiri Srba, patent pending), I will also report on our query language, the tool we develop at Aalborg University, as well as on our first evaluation results.
I would also like to use the opportunity of this talk to provide a brief overview of our other research activities, especially the ones related to network security and the design of demand-aware and self-adjusting networks. We are currently eager to establish connections and collaborations within Vienna and Austria in general, related to all the presented topics and beyond. More details about our research activities can also be found at https://net.t-labs.tu-berlin.de/~stefan/
The ACL2 theorem-proving system has seen sustained industrial use since
the mid 1990s. Companies that have and are using ACL2 include AMD, ARM,
Centaur Technology, General Electric, IBM, Intel, Kestrel Institute,
Motorola/Freescale, Oracle, and Rockwell Collins. ACL2 has been
accepted for industrial application because it is an integrated
programming/proof environment supporting a subset of the ANSI standard
Common Lisp programming language. Software and hardware systems have
been modeled and analyzed with the ACL2 theorem-proving system.
The ACL2 programming language can be used to develop efficient and
robust programs. The ACL2 analysis machinery provides many features
permitting domain-specific, human-supplied guidance at various levels
of abstraction. ACL2 specifications often serve as efficient execution
engines for the modeled artifacts while permitting formal analysis and
proof of properties. ACL2 provides support for the development and
verification of other formal analysis tools. ACL2 did not find its way
into industrial use merely because of its technical features. The ACL2
user/development community has a shared vision of making formal
specification and mechanized verification routine — we have been
committed to this vision for the quarter century since the Computational
Logic, Inc., Verified Stack.
Recursive algebraic data types (term algebras, ADTs) are one of the
most well-studied theories in logic, and find application in
contexts including functional programming, modelling languages,
proof assistants, and verification. At this point, several
state-of-the-art theorem provers and SMT solvers include tailor-made
decision procedures for ADTs, and version 2.6 of the SMT-LIB
standard includes support for ADTs. We study a relatively simple
approach to decide satisfiability of ADT constraints, the reduction
of ADT constraints to equisatisfiable constraints over uninterpreted
functions (EUF) and linear integer arithmetic (LIA). We show that
the reduction approach gives rise to both decision and Craig
interpolation procedures in ADTs. As an extension, we then consider
ADTs with size constraints, and give a precise characterisation of
the ADTs for which reduction combined with incremental unfolding is
a decision procedure.