Rigorous estimation of maximum floating-point round-off errors is an important capability
central to many formal verification tools. Unfortunately, available techniques for this task …

Formal methods encompass a wide choice of techniques and tools for the specification,
development, analysis, and verification of software and hardware systems. Formal methods …

We describe JDart, a dynamic symbolic analysis framework for Java. A distinguishing
feature of JDart is its modular architecture: the main component that performs dynamic …

A test harness, in automated test generation, defines the set of valid tests for a system, as
well as their correctness properties. The difficulty of writing test harnesses is a major …

This paper describes our work on demonstrating verification technologies on a flight-critical
system of realistic functionality, size, and complexity. Our work targeted a commercial aircraft …

A new approach to testing multi-UAV conflict resolution algorithms is presented. The
problem is formulated as a multi-objective search problem with two objectives: finding air …

The difficulty of writing test harnesses is a major obstacle to the adoption of automated
testing and model checking. Languages designed for harness definition are usually tied to a …

Writing a test harness is a difficult and repetitive program-ming task, and the lack of tool
support for customized auto-mated testing is an obstacle to the adoption of more sophis …

Autonomous vehicles will share the road with human drivers within the next couple of years.
This will revolutionize road traffic and provide a positive benefit for road safety, traffic density …

A recent trend in the analysis of object-oriented programs is the modeling of references as
sets of guarded values, enabling multiple heap shapes to be represented in a single state. A …