Publications/Software Verification

System And Method for Configuration of an Ensemble Solver

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

Read More »

Blackspot: Using Tensor Decompositions to Guide Inspection of Source Code

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

Read More »

Cross-Format Analysis of Software Systems

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

Read More »

Accelerating SCA Compliance Testing with Advanced Development Tools

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

Read More »

Systems, Methods, and Apparatus for Distributed Decision Processing

Methods, apparatus, and computer software product for making a decision based on the semantics of formal logic are provided. In an exemplary embodiment, two custom computing apparatuses are used to resolve the satisfiability of a logical formula and provide an example. In this embodiment, the two custom computing apparatuses operate

Read More »

Bridging the Gap Between Specifications and Compliance Tests

This presentation was given at the 2013 Wireless Innovation Forum (WIF) annual meeting, describing how Reservoir’s R-Check product meets needs of one of the top innovations needed for software radio, specifically that R-Check provides “the ability to certify software implementations of waveforms for use on various radio computing platforms promises

Read More »

The Benefits of Static Compliance Testing for SCA Next

The next generation of the Software Communications Architecture (SCA) specification (SCA Next) introduces several features that will affect the compliance certification process. Among the more significant and high-profile changes are the introduction of multiple supported platform models and support for both CORBA and non-CORBA transport layers. These features, which further abstract

Read More »