ATx'12/WInG'12: Papers with Abstracts

Abstract. This article shows that theory exploration arises naturally from the need to progressively modify applied formal theories, especially those underpinning deployed systems that change over time or need to be attack-tolerant. Such formal theories require us to explore a problem space with a proof assistant and are naturally dynamic.

The examples in this article are from our on-going decade-long effort to formally synthesize critical components of modern distributed systems. Using the Nuprl proof assistant we created event logic and its protocol theories. I also mention the impact over this period of extensions to the constructive type theory implemented by Nuprl. One of them led to our solution of a long standing open problem in constructive logic.

Proof exchange among theorem provers is promising for improving the "super tactics" that provide domain specific reasoners for our protocol theories. Both theory exploration and proof exchange illustrate the dynamic nature of applied formal theories built using modern proof assistants. These activities dispel the false impression that formal theories are rigid and brittle artifacts that become less relevant over time in a fast moving field like computer science.

Abstract. We present ongoing work on HipSpec, a system for automatically
deriving and proving properties about functional programs. HipSpec uses
a combination of theory formation, counter example testing and
inductive theorem proving to automatically generate a set of
equational theorems about recursive functions in a program, which are later
used as a background theory for proving stated properties about a program.
Initial experiments are encouraging; our initial HipSpec prototype already performs comparably to other, similar systems, even being able to deal with some properties other systems cannot handle.

Abstract. In recent years, diagrammatic languages have been shown to be a powerful and expressive tool for reasoning about physical, logical, and semantic processes represented as morphisms in a monoidal category. In particular, categorical quantum mechanics, or "Quantum Picturalism", aims to turn concrete features of quantum theory into abstract structural properties, expressed in the form of diagrammatic identities. One way we search for these properties is to start with a concrete model (e.g. a set of linear maps or finite relations) and start composing generators into diagrams and looking for graphical identities.

Naively, we could automate this procedure by enumerating all diagrams up to a given size and check for equalities, but this is intractable in practice because it produces far too many equations. Luckily, many of these identities are not primitive, but rather derivable from simpler ones. In 2010, Johansson, Dixon, and Bundy developed a technique called conjecture synthesis for automatically generating conjectured term equations to feed into an inductive theorem prover. In this extended abstract, we adapt this technique to diagrammatic theories, expressed as graph rewrite systems, and demonstrate its application by synthesising a graphical theory for studying entangled quantum states.

Abstract. We present a framework in Isabelle/HOL for formalizing variants of
depth-first search. This framework allows to easily prove non-trivial
properties of these variants. Moreover, verified code in several
programming languages including Haskell, Scala and Standard ML can be
generated.

In this paper, we present an abstract formalization of depth-first search and
demonstrate how it is refined to an efficiently executable version. Further we use the emptiness-problem of Büchi-automata known from model checking as the motivation to present three Nested DFS algorithms. They are formalized, verified and transformed into executable code using our framework.

Abstract. There is an empirical claim that, when exploring a
mathematical theory, after a succession of key results have been
obtained, a point of equilibrium is reached where any query of
interest can be resolved by routine reasoning from the results
already established. Here is suggested some ways of thinking about
the situation, in general. There are at least some situations where
we can establish that all results (of a certain shape) will follow
by routine reasoning from a small number of key properties. An
example is described, and the significance for automated theory
exploration discussed.

Abstract. Computing good specification and invariants is key to effective
and efficient program verification. In this talk, I will describe
our experiences in using machine learning techniques (Bayesian
inference, SVMs) for computing specifications and invariants
useful for program verification. The first project Merlin uses
Bayesian inference in order to automatically infer security
specifications of programs. A novel feature of Merlin is that it
can infer specifications even when the code under analysis gives
rise to conflicting constraints, a situation that typically
occurs when there are bugs. We have used Merlin to infer security
specifications of 10 large business critical web
applications. Furthermore, we show that these specifications can
be used to detect new information flow security vulnerabilities
in these applications.

In the second project Interpol, we show how interpolants can be
viewed as classifiers in supervised machine learning. This view
has several advantages: First, we are able to use off-the-shelf
classification techniques, in particular support vector
machines (SVMs), for interpolation. Second, we show that SVMs can
find relevant predicates for a number of benchmarks. Since
classification algorithms are predictive, the interpolants
computed via classification are likely to be relevant predicates
or invariants. Finally, the machine learning view also enables us
to handle superficial non-linearities. Even if the underlying
problem structure is linear, the symbolic constraints can give an
impression that we are solving a non-linear problem. Since
learning algorithms try to mine the underlying structure
directly, we can discover the linear structure for such
problems. We demonstrate the feasibility of Interpol via
experiments over benchmarks from various papers on program
verification.

Abstract. We present a few lightweight numeric abstract domains to analyze C programs that
exploit the binary representation of numbers in computers, for instance to
perform ``compute-through-overflow'' on machine integers, or to directly
manipulate the exponent and mantissa of floating-point numbers.
On integers, we propose an extension of intervals with a modular component,
as well as a bitfield domain.
On floating-point numbers, we propose a predicate domain to match, infer,
and propagate selected expression patterns.
These domains are simple, efficient, and extensible.
We have included them into the Astree and AstreeA static analyzers to
supplement existing domains. Experimental results show that they can improve
the analysis precision at a reasonable cost.