USA flag logo/image

An Official Website of the United States Government

Company Information:

Name: Aries Design Automation, LLC
Address: 2705 West Byron Street
Chicago, IL 60618-3745
Located in HUBZone: No
Woman-Owned: No
Minority-Owned: No
URL: N/A
Phone: (773) 856-6633

Award Totals:

Program/Phase Award Amount ($) Number of Awards
SBIR Phase I $1,415,000.00 13
SBIR Phase II $1,800,000.00 3
STTR Phase I $100,000.00 1

Award List:

Formal Methods for Malware Detection

Award Year / Program / Phase: 2006 / SBIR / Phase I
Agency / Branch: DOD / OSD
Principal Investigator: Miroslav N. Velev, President, CEO, CTO
Award Amount: $100,000.00
Abstract:
Our objective is to develop highly automatic and scalable formal methods for malware detection. Existing tools for malware detection operate by searching for pattern matches with respect to signatures of known malware, and can account for only limited variations in the malware. That makes these… More

Formal-Verification-Based Tool for Deobfuscation of Tamper-Proofed Software

Award Year / Program / Phase: 2006 / STTR / Phase I
Agency / Branch: DOD / OSD
Research Institution: UNIV. OF ARIZONA
Principal Investigator: Miroslav N. Velev, President, CEO
Award Amount: $100,000.00
RI Contact: Saumya K. Debray
Abstract:
The rapid increase in the use of the Internet in many aspects of our lives has led to an explosive growth in the spread of malware such as computer worms, viruses, and trojans. Security tools typically examine software for the presence of malware either by looking for specific byte signatures, or… More

SBIR Phase I: Techniques for Analysis of Counterexamples from Formal Verification of High-Level Microprocessor Designs

Award Year / Program / Phase: 2006 / SBIR / Phase I
Agency: NSF
Principal Investigator: Miroslav Velev, Dr
Award Amount: $100,000.00
Abstract:
This Small Business Innovation Research (SBIR) Phase I research proposes to study the feasibility of automatic methods for analysis of counterexamples from formal verification of pipelined and superscalar microprocessors modeled at a high level of abstraction. Aries Design Automation has developed… More

Efficient Techniques for Formal Verification of PowerPC 750 Executables

Award Year / Program / Phase: 2008 / SBIR / Phase I
Agency: NASA
Principal Investigator: Miroslav Velev, Principal Investigator
Award Amount: $100,000.00
Abstract:
We will develop an efficient tool for formal verification of PowerPC 750 executables. The PowerPC 750 architecture is used in the radiation-hardened RAD750 flight-control computers that are utilized in many space missions. The resulting tool will be capable of formally checking: 1) the equivalence… More

Efficient Techniques for Formal Verification of PowerPC 750 Executables

Award Year / Program / Phase: 2009 / SBIR / Phase II
Agency: NASA
Principal Investigator: Miroslav N. Velev, Principal Investigator
Award Amount: $600,000.00
Abstract:
We will develop an efficient tool for formal verification of PowerPC 750 executables. The PowerPC 750 architecture is used in the radiation-hardened RAD750 flight-control computers that are utilized in many space missions. The resulting tool will be capable of formally checking: 1) the equivalence… More

An Efficient Parallel SAT Solver Exploiting Multi-Core Environments

Award Year / Program / Phase: 2009 / SBIR / Phase I
Agency: NASA
Principal Investigator: Miroslav Velev, Principal Investigator
Award Amount: $100,000.00
Abstract:
The hundreds of stream cores in the latest graphics processors (GPUs), and the possibility to execute non-graphics computations on them, open unprecedented levels of parallelism at a very low cost. We will investigate ways to efficiently exploit this parallelism in order to accelerate the execution… More

Insider Threat Detection and Response Using Formal Methods

Award Year / Program / Phase: 2009 / SBIR / Phase I
Agency: DOE
Principal Investigator: Miroslav Velev, Dr.
Award Amount: $100,000.00
Abstract:
This project will extend the Capability Acquisition Graph (CAG) model to a form that can be easily analyzed with formal methods in order to develop countermeasures for cyber attacks arising from within an organization. The extension will be based on an efficient translation of the problem to Boolean… More

Formal Methods for Robustness Checking of Radiation-Hardened-by-Design Microelectronics

Award Year / Program / Phase: 2009 / SBIR / Phase I
Agency: DOE
Principal Investigator: Miroslav Velev, Dr.
Award Amount: $100,000.00
Abstract:
For more than four decades, space-based systems have been used to support the detection of activities associated with the proliferation of weapons of mass destruction. This project will develop efficient and scalable tool to evaluate the robustness of radiation-hardened circuits and to… More

Reconfigurable VLIW Processor for Software Defined Radio

Award Year / Program / Phase: 2010 / SBIR / Phase I
Agency: NASA
Principal Investigator: Miroslav N. Velev, Principal Investigator
Award Amount: $100,000.00
Abstract:
We will design and formally verify a VLIW processor that is radiation-hardened, and where the VLIW instructions consist of predicated RISC instructions from the PowerPC 750 Instruction Set Architecture (ISA). The PowerPC 750 ISA is used in the radiation-hardened RAD750 flight-control computer that… More

An Efficient Parallel SAT Solver Exploiting Multi-Core Environments

Award Year / Program / Phase: 2010 / SBIR / Phase II
Agency: NASA
Principal Investigator: Miroslav N. Velev, Principal Investigator
Award Amount: $600,000.00
Abstract:
The hundreds of stream cores in the latest graphics processors (GPUs), and the possibility to execute non-graphics computations on them, open unprecedented levels of parallelism at a very low cost. In the last 6 years, GPUs had an increasing performance advantage of an order of magnitude relative to… More

SBIR Phase I: Automatic Formal Verification of Chip-Multi-Threaded Multicore Processors

Award Year / Program / Phase: 2010 / SBIR / Phase I
Agency: NSF
Principal Investigator: Miroslav Velev, DPhil
Award Amount: $150,000.00
Abstract:
This Small Business Innovation Research (SBIR) Phase I project will result in an efficient and scalable method for design and formal verification of Chip-Multi-Threaded multicore processors, where the individual cores have hardware support for multi-threading. This method will be developed and… More

Exploiting GPUs for Scalable Network Intrusion Detection

Award Year / Program / Phase: 2010 / SBIR / Phase I
Agency: DOE
Principal Investigator: Miroslav Velev, Dr.
Award Amount: $100,000.00
Abstract:
In this proposed SBIR Phase I project, we will develop a proto

Using Automated Abstractions to Classify System States for Software Health Monitoring

Award Year / Program / Phase: 2011 / SBIR / Phase I
Agency / Branch: DOC / NIST
Principal Investigator: N/A
Award Amount: $90,000.00
Abstract:
In most critical software systems, a state that is partially visible through values passed across interfaces contains information that could determine the health of the software system, and whether a failure is likely in the future. Some of this information behaves in a continuous fashion, e.g., the… More

Reconfigurable VLIW Processor for Software Defined Radio

Award Year / Program / Phase: 2011 / SBIR / Phase II
Agency: NASA
Principal Investigator: Miroslav N. Velev, Principal Investigator
Award Amount: $600,000.00
Abstract:
We will implement an environment for design, formal verification, compilation of code, and performance and power evaluation of Systems on a Chip (SOCs) consisting of heterogeneous processor cores that can be single-issue pipelined, superscalar, or VLIW, and are binary-code compatible with any… More

Scalable Parallel Algorithms for Formal Verification of Software

Award Year / Program / Phase: 2012 / SBIR / Phase I
Agency: NASA
Principal Investigator: Miroslav Velev, Principal Investigator
Award Amount: $125,000.00
Abstract:
We will develop a prototype of a GPU-based parallel Binary Decision Diagram (BDD) software package. BDDs are a data structure that satisfies some simple restrictions, resulting in a unique representation of a Boolean function regardless of its actual implementation. This property of BDDs allows the… More

Scalable Parallel Algorithms for Formal Verification of Software

Award Year / Program / Phase: 2013 / SBIR / Phase I
Agency: NASA
Principal Investigator: Miroslav N. Velev, Principal Investigator
Award Amount: $125,000.00
Abstract:
We will develop an efficient Graphics Processing Unit (GPU) based parallel Binary Decision Diagram (BDD) software package, and will also combine it with our GPU-based parallel SAT solver that we are currently developing in a NASA SBIR Phase II project in order to solve much larger and more complex… More

Formal Verification of Interactions of the RTOS, Memory System, and Application Programs at the PowerPC 750 Binary Code Level

Award Year / Program / Phase: 2013 / SBIR / Phase I
Agency: NASA
Principal Investigator: Miroslav N. Velev, Principal Investigator
Award Amount: $125,000.00
Abstract:
In the proposed project, we will formally verify the correctness of the interaction between a Real-Time Operating System (RTOS) and user processes under various operating scenarios, such as multitasking, interrupt handling, user and kernel mode switching. The formal verification will be done… More