ATx'12/WInG'12: Papers with AbstractsPapers 

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 attacktolerant. 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 ongoing decadelong 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 depthfirst search. This framework allows to easily prove nontrivial 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 depthfirst search and demonstrate how it is refined to an efficiently executable version. Further we use the emptinessproblem of Büchiautomata 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 offtheshelf 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 nonlinearities. Even if the underlying problem structure is linear, the symbolic constraints can give an impression that we are solving a nonlinear 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 ``computethroughoverflow'' on machine integers, or to directly manipulate the exponent and mantissa of floatingpoint numbers. On integers, we propose an extension of intervals with a modular component, as well as a bitfield domain. On floatingpoint 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. 

