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.
Automata learning is a technique that has successfully been applied in verification, with the automaton type
varying depending on the application domain. Adaptations of automata learning algorithms for increasingly
complex types of automata have to be developed from scratch because there was no abstract theory offering
guidelines. This makes it hard to devise such algorithms, and it obscures their correctness proofs.
We introduce a simple category-theoretic formalism that provides an appropriately abstract foundation for
studying automata learning. Furthermore, our framework establishes formal relations between algorithms for
learning, testing, and minimization. We illustrate its generality with two examples: deterministic and weighted
Parity games are deceptively simple two-player games on directed graphs
labeled with numbers.
Parity games have important practical applications in formal
verification and synthesis, especially to solve the model-checking problem
of the modal mu-calculus. They are also interesting from the theory
perspective, because they are widely believed to admit a polynomial
solution, but so far no such algorithm is known. In recent years, a number
of new algorithms and improvements to existing algorithms have been
In this talk, we introduce parity games in an accessible way and discuss
why they are so interesting. We present various solutions that have been
proposed over the years. We also present a comprehensive empirical evaluation
of modern parity game algorithms and solvers, both on real world benchmarks
and randomly generated games.
Symbolic executions (and their recent variants called dynamic symbolic
executions) are an important technique in automated testing. Instead
of analysing only concrete executions of a program, one could treat
such executions symbolically (i.e. with some variables that are not
bound to concrete values) and use constraint solvers to determine this
(symbolic) path feasibility so as to guide the path explorations of
the system under test, which in combination with dynamic analysis
gives the best possible path coverage. For string-manipulating
programs, solvers need to be able to handle constraints over the
string domain. This gives rise to the following natural question: what
is an ideal decidable logic over strings for reasoning about path
feasibility in a program with strings? This is a question that is
connected to a number of difficult results in theoretical computer
science (decidability of the theory of strings with concatenations,
a.k.a., word equations) and long-standing open problems (e.g.
decidability of word equations with length constraints). Worse yet,
recent examples from cross-site scripting vulnerabilities suggest that
more powerful string operations (e.g. finite-state transducers) might
be required as first class citizens in string constraints. Even though
putting all these string operations in a string logic leads to
undecidability, recent results show that there might be a way to
recover decidability while retaining expressivity for applications in
symbolic execution. In this talk, I will present one such result from
my POPL’16 paper (with P. Barcelo). The string logic admits
concatenations, regular constraints, finite-state transductions,
letter-counting and length constraints (which can consequently express
charAt operator, and string disequality). I will provide a number of
examples from the cross-site scripting literature that shows how a
string logic can, for the first time, be used to discover a bug in or
prove correctness of the programs. I will conclude by commenting on a
new decision procedure for the logic that leads to an efficient
implementation (POPL’18 with L. Holik, P. Janku, P. Ruemmer, and T.
Vojnar) and a recent attempt to incorporate the fully-fledged
replace-all operator into a string logic (POPL’18 with T. Chen, Y.
Chen, M. Hague, and Z. Wu).
Buggy and insecure software could have serious consequences including
the loss of human lives, financial losses, and confidential
information leakage, to name a few. Program analysis is a field that
concerns the problem of analysing the behaviour of programs especially
with respect to the issue of correctness. Over the years computational
logic has played an important role in program analysis particularly in
the development of precise automatic methods for verifying the
correctness and optimising the performance of programs. In this talk I
will illustrate how logic can help program analysis, drawing examples
from my own research inspired by challenges in web security (e.g. how
to detect/prevent cross-site scripting vulnerabilities), web
performance optimisation (e.g. how to remove code redundancies in web
pages), and verification of distributed protocols. A theme that will
emerge during the talk is that there is often a tight connection
between logic and automata that can be exploited when designing (often
theoretically optimal) algorithms.
The rapid growth in the size and scope of datasets in science and technology has created a need for novel foundational perspectives on data analysis that blendthe inferential and computational sciences. That classical perspectives from these fields are not adequate to address emerging problems in Data Science is apparent from their sharply divergent nature at an elementary level—in computer science, the growth of the number of data points is a source of “complexity” that must be tamed via algorithms or hardware, whereas in statistics, the growth of the number of data points is a source of “simplicity” in that inferences are generally stronger and asymptotic results can be invoked. On a formal level, the gap is made evident by the lack of a role for computational concepts such as “runtime” in core statistical theory and the lack of a role for statistical concepts such as “risk” in core computational theory. I present several research vignettes aimed at bridging computation and statistics, including the problem of inference under privacy and communication constraints, and including a surprising cameo role for symplectic geometry.