17231423
Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving
Combining theorem proving and model checking offers the tantalizing possibility of efficiently reasoning about large circuits at high levels of abstraction. We have constructed a system that seamlessly integrates symbolic trajectory evaluation based model checking with theorem proving in a higher-order classical logic. The approach is made possible by using the same programming language (fl) as both the meta and object language of theorem proving. This is done by "lifting" fl, essentially deeply embedding fl in itself. The approach is a pragmatic solution that provides an efficient and extensible Verification environment. Our approach is generally applicable to any dialect of the ML programming language and any model-checking algorithm that has practical inference rules for combining results.
16240719
Formal Verification of Out-of-Order Execution Using Incremental Flushing
We present a two-part approach for verifying out-of-order execution. First, the complexity of out-of-order issue and scheduling is handled by creating an in-order abstraction of the out-of-order execution core. Second, incremental flushing addresses the complexity difficulties encountered by automated abstraction functions on very deep pipelines. We illustrate the techniques on a model of a simple out-of-order processor core.
14277112
A Methodology for Large-Scale Hardware Verification
We present a formal verification methodology for datapath-dominated hardware. This provides a systematic but flexible framework within which to organize the activities undertaken in large-scale verification efforts and to structure the associated code and proof-script artifacts. The methodology deploys a combination of model checking and lightweight theorem proving in higher-order logic, tightly integrated within a general-purpose functional programming language that allows the framework to be easily customized and also serves as a specification language. We illustrate the methodology--which has has proved highly effective in large-scale industrial trials--with the verification of an IEEE-compliant, extended precision floating-point adder.
7974229
Efficient validity checking for processor verification
We describe an efficient validity checker for the quantifier-free logic of equality with uninterpreted functions. This logic is well suited for verifying microprocessor control circuitry since it allows the abstraction of datapath values and operations. Our validity checker uses special data structures to speed up case splitting, and powerful heuristics to reduce the number of case splits needed. In addition, we present experimental results and show that this implementation has enabled the automatic verification of an actual high-level microprocessor description.
208909301
Parametric Representations of Boolean Constraints.
85258
Reducing Manual Abstraction in Formal Verification of Out-of-Order Execution
Several methods have recently been proposed for verifying processors with out-of-order execution. These methods use intermediate abstractions to decompose the verification process into smaller steps. Unfortunately, the process of manually creating intermediate abstractions is very laborious. We present an approach that dramatically reduces the need for an intermediate abstraction, so that only the scheduling logic of the implementation is abstracted. After the abstraction, we apply an enhanced incremental-flushing approach to verify the remaining circuitry by comparing the processor description against itself in a slightly simpler configuration. By induction, we demonstrate that any reachable configuration is equivalent to the simplest possible configuration. Finally, we prove correctness on the simplest configuration. The approach is illustrated with a simple example of an out-of-order execution core.
6983154
Benchmarking Implementations of Functional Languages with 'Pseudoknot', a Float-Intensive Benchmark
Over 25 implementations of different functional languages are benchmarked using the same program, a floatingpoint intensive application taken from molecular biology. The principal aspects studied are compile time and execution time for the various implementations that were benchmarked. An important consideration is how the program can be modified and tuned to obtain maximal performance on each language implementation. 
With few exceptions, the compilers take a significant amount of time to compile this program, though most compilers were faster than the then current GNU C compiler (GCC version 2.5.8). Compilers that generate C or Lisp are often slower than those that generate native code directly: the cost of compiling the intermediate form is normally a large fraction of the total compilation time. 
There is no clear distinction between the runtime performance of eager and lazy implementations when appropriate annotations are used: lazy implementations have clearly come of age when it comes to implementing largely strict applications, such as the Pseudoknot program. The speed of C can be approached by some implemtations, but to achieve this performance, special measures such as strictness annotations are required by non-strict implementations. 
The benchmark results have to be interpreted with care. Firstly, a benchmark based on a single program cannot cover a wide spectrum of 'typical' applications.j Secondly, the compilers vary in the kind and level of optimisations offered, so the effort required to obtain an optimal version of the program is similarly varied.
40732361
Meeting Diverse User Needs
Any higher education department must provide a variety of information to several disparate audiences, recognising their diverse needs. Managing these challenges and changes demands flexibility and auditability. Technology can provide the mechanism to meet these information needs and educational challenges, and to manage changing social and political demands. In this paper we offer pointers abstracted and generalised from our experience for organizational change in similar environments. We explain the development of a large web-based information system designed to meet these challenges. Our goal has been not only to improve our site but also to embed it at the heart of the department’s culture. We describe the technical innovations that are required to manage this large-scale site and that permit the flexibility needed to respond to change. Finally, we suggest measures by which the success of enterprises of this kind may be measured. Evidence of changes in student and staff* expectations, behaviour, and study patterns is presented.
11914137
TREC-10 Experiments at University of Maryland CLIR and Video
The University of Maryland Researchers participated in both the Arabic-English Cross Language Information Retrieval (CLIR) and Video tracks of TREC-10. In the CLIR track, our goal was to explore effective monolingual Arabic IR techniques and effective query translation from English to Arabic for cross language IR. For the monolingual part, the use of the different index terms including words, stems, roots, and character n-grams were explored. For the English-Arabic CLIR, the use of MT, wordlist based translation, and non-dictionary words transliteration was explored. In the video track, we participated in the shot boundary detection, and known item search with the primary goals being to evaluate existing technology for shot detection and a new approach to extending simple visual image queries to video sequences. We present a general overview of the approaches, summarize the results in discuss how the algorithms are being extended.
5135848
Using temporal profiles of queries for precision prediction
A key missing component in information retrieval systems is self-diagnostic tests to establish whether the system can provide reasonable results for a given query on a document collection. If we can measure properties of a retrieved set of documents which allow us to predict average precision, we can automate the decision of whether to elicit relevance feedback, or modify the retrieval system in other ways. We use meta-data attached to documents in the form of time stamps to measure the distribution of documents retrieved in response to a query, over the time domain, to create a temporal profile for a query. We define some useful features over this temporal profile. We find that using these temporal features, together with the content of the documents retrieved, we can improve the prediction of average precision for a query.
1946418
A Cyclic Distributed Garbage Collector for Network Objects
This paper presents an algorithm for distributed garbage collection and outlines its implementation within the Network Objects system. The algorithm is based on a reference listing scheme, which is augmented by partial tracing in order to collect distributed garbage cycles. Processes may be dynamically organised into groups, according to appropriate heuristics, to reclaim distributed garbage cycles. The algorithm places no overhead on local collectors and suspends local mutators only briefly. Partial tracing of the distributed graph involves only objects thought to be part of a garbage cycle: no collaboration with other processes is required. The algorithm offers considerable flexibility, allowing expediency and fault-tolerance to be traded against completeness.