Runtime Verification of Cognitive Applications



Publication Source: The 10th Annual High Performance Embedded Computing Workshop (HPEC), Lexington, MA, USA

Cognitive systems have been the subject of much research, and are increasingly of interest in embedded systems. However, cognitive applications have unique characteristics that make them challenging to verify, validate, and debug. A cognitive application by definition makes intelligent decisions – if it were possible to formally and precisely express its behavior under all circumstances, the cognitive system would not need to be “cognitive.”
Google Scholar    Article

Salt & Alef: Unlocking the Power of Boolean Satisfiability



Publication Source: The 10th Annual High Performance Embedded Computing Workshop (HPEC), Lexington, MA, USA, 2006

Solvers for the Boolean satisfiability problem (SAT) are an enabling technology for a diverse set of applications relevant to the HPEC community. These applications include formal verification, analysis of numerical precision for embedded pipelines, and cognitive reasoning. However, solver performance, measured in terms of speed and maximum problem size, is a limiting factor to the application of SAT to real-world problems. We are developing a constraint language, translation tool, and parallel SAT solver to significantly mitigate the impact of these limitations.
Google Scholar    Article

Alef Verification and Planning System



Publication Source: The 48th Annual Cray User Group (CUG) Technical Conference, Lugano, Switzerland, 2006

Recently, solvers for the Satisfiability problem (SAT) have become an enabling technology for diverse areas of military and commercial interest. However, solver performance, in terms of speed, maximum problem size, and efficiency, is a limiting factor to the more extensive application of this technology. This paper discusses Reservoir's SAT-based planning and verification system, Alef, which includes a compiler, intermediate language, and parallel solver for HPC hardware. 
Google Scholar    Article

SAT Solvers for Investigation of Architectures for Cognitive Information Processing



Publication Source: The High Performance Embedded Computing Workshop (HPEC), Lexington, MA, USA, September, 2006

Sponsored by DARPA in the ACIP Program, this presentation covers demand for cognitive processing, historical architectures for AI / cognitive processing, SAT solvers as a cognitive application, application specific hardware, parallelizing SAT, current performance, and architectural implications.
Article

R-Stream 3.0: Technologies for High Level Embedded Application Mapping



Publication Source: The 8th Annual High Performance Embedded Computing (HPEC) Workshops, Lexington, MA, USA, 2004

R-Stream is a High Level Compiler being developed as part of the DARPA IPTO Polymorphous Computer Architecture Program. The compiler is targeted at the problem of mapping high performance embedded signal/knowledge processing applications. Our 2.0 version, presented as a poster at HPEC last year, will be performing application mapping via the Streaming Virtual Machine interface to low level compilers (LLC). This presentation will focus on the implementation and architecture of the high level compiler (HLC). In particular, we will present the performance results and insights from our 2.0 version of our Integrated Radar Tracker (IRT) running simulated on the reference Polymorphous Computer Architecture (PCA). The performance results will be accompanied by details of the application transformations that 2.0 will be performing, including granularity selection, high level streaming transformations, and the manner in which we integrate the data parallel front end of IRT with the more task/thread parallel back end. Furthermore, we expect to be able to provide insight into the benefits and limitations of some aspects of the morphware software architecture, in particular the phased HLC/LLC compilation structure, the SVM interface, and the abstraction of architectures into the Streaming Machine Model (SMM) and Hierarchical Machine Model (HMM). We may further be able to accompany this with some performance results for the application mapped to commercial architectures that are emerging with similarities to the PCA architecture class.
Google Scholar    Article

1 18 19 20 21