Seminars

We begin by presenting a very short overview of past and current research carried out by the Safety Critical Avionics Brach (SCAB) at NASA's Langley Research Center (LaRC). We will then discuss several ongoing and new research projects being conducted in the SCAB. In particular, we will survey new research efforts in safety-critical fault-tolerant distributed avionics, verification of numerical software, and run-time verification as well as experiments involving unmanned aerial systems (UAS). We will discuss opportunities for internships in each of these projects as well as areas such as…

In this talk, I will try to make a case for the use of data flow graphs as a suitable notion for abstractions of concurrent programs for the purpose of verification. I will talk about two successful experiences that we have had with these graphs. One is the development of an abstract interpretation framework that constructs annotated data flow graph where the annotations can come from any abstract domain such as intervals or octagons. We demonstrate how by separating the concerns of reasoning about data (computing the data invariants) and control (computing a precise enough pattern of…

There is a growing demand for systems that can detect complex patterns in high-speed streams of events or in large volumes of stored sequences. This demand is driven by so-called complex event processing (CEP) applications whose success depends on their ability to make real-time decisions, such as high-frequency trading, fraud detection, and online advertisement. As a result, several database vendors are providing new SQL extensions to support such applications.

In this talk, we show that these extensions suffer from expressivity limitations that severely impair their generality…

(Joint work with Gethin Norman and David Parker) 

Quantitative verification techniques are able to establish system properties such as "the probability of an airbag failing to deploy on demand'' or "the expected time for a network protocol to successfully send a message packet''. In this paper, we describe a framework for quantitative verification of software that exhibits both real-time and probabilistic behaviour. The complexity of real software, combined with the need to capture precise timing information, necessitates the use of abstraction techniques. We outline a…

A parallel program must execute correctly even in the presence of unpredictable thread interleavings. This interleaving makes it hard to write correct parallel programs, and also makes it hard to find bugs in incorrect parallel programs. A range of tools have been developed to help debug parallel programs, ranging from atomicity-violation and data-race detectors to model-checkers and theorem provers. One technique that has been successful for debugging sequential programs, but less effective for parallel programs, is running the program using assertion predicates provided by the developer…