Software Verification

System And Method for Configuration of an Ensemble Solver

Publication Source: Patent US9684865B1

In a system for enabling configuration of an ensemble of several solvers, such that the ensemble can efficiently solve a constraint problem, for each one of several candidate configurations, an array of scores is computed. The array corresponds to a statistical parameter related to a problem solution, and the computation is based on, at least in part, a set of features associated with the problem. One candidate configuration is assigned to a solver, and based on the array of scores associated with that candidate configuration the same or a different candidate configuration is assigned to a another solver. A system for dynamically reconfiguring an ensemble of solvers obtains runtime data from several solvers, and a new configuration is determined by applying a machine learning and/or heuristic analysis procedure to the runtime data. The configuration of a solver may be updated according to the new configuration while that solver is running.
Google Scholar    Article

Blackspot: Using Tensor Decompositions to Guide Inspection of Source Code

Publication Source: Wireless Innovation Forum Conference on Wireless Communication Technologies and Software Defined Radio, Reston, VA, USA.

In this paper we introduce Blackspot, an extension to R-Check SCA that uses unsupervised machine learning based on tensor decompositions to organize and highlight sections of source code for more systematic inspection. Using markers identified by R-Check SCA’s Pitchfork rule language, multidimensional decompositions are used to cluster code so as to group similar structures for accelerated manual inspection and, when seeded with examples of known weaknesses, to prioritize code fragments for rigorous review based on similarity derived from latent features. We show how multidimensional analysis provides a precision advantage over matrix SVD-based approaches and enables both accelerated compliance testing and more directed discovery of potentially critical software weaknesses. Utilizing high-performance tensor decomposition techniques provided by Reservoir’s ENSIGN Tensor Toolbox, Blackspot scales to millions of lines of code, making it practical for application to complex, large-scale cyber-physical systems. Using an open SCA radio waveform as a first example, we illustrate how Blackspot can be applied to guide inspection for SCA compliance testing and weakness discovery in the software radio domain.
Google Scholar    Article

A Unified Coq Framework for Verifying C Programs with Floating-Point Computations

Publication Source: The 5th ACM SIGPLAN Conference on Certified Programs and Proofs, ACM SIGLOG, Saint Petersburg, FL, USA.

We provide concrete evidence that floating-point computations in C programs can be verified in a homogeneous verification setting based on Coq only, by evaluating the practicality of the combination of the formal semantics of CompCert Clight and the Flocq formal specification of IEEE 754 floating-point arithmetic for the verification of properties of floating-point computations in C programs. To this end, we develop a framework to automatically compute real number expressions of C floating-point computations with rounding error terms along with their correctness proofs. We apply our framework to the complete analysis of an energy-efficient C implementation of a radar image processing algorithm, for which we provide a certified bound on the total noise introduced by floating-point rounding errors and energy-efficient approximations of square root and sine.
Google Scholar    Article

Cross-Format Analysis of Software Systems

Publication Source: Patent US9134976B1

In various implementations of a software analysis system, compliance checking is facilitated by analyzing different characteristics of a software system to be developed, and by comparing the information extracted from these analysis. Two or more characteristics may be expressed in different formats or languages, and the descriptions of one or more of these characteristic may be incomplete.
Google Scholar    Article

Accelerating SCA Compliance Testing with Advanced Development Tools

Publication Source: The SDR-WInnComm Wireless Innovation Forum 2015

In this paper, we explore the potential for combining model-based development environments supporting automatic code generation with novel static testing technology to accelerate the SCA compliance testing process. Model-based development and automated testing yield higher regularity and predictability, reducing testing complexity and sidestepping some issues for software intended for deployment on multiple hardware platforms.
Google Scholar    Article

1 2 3