Topics: Software Architecture
This 2005 report describes the application of the SEI Architecture Tradeoff Analysis Method (ATAM) to the U.S. Army's Warfighter Information Network-Tactical (WIN-T) system.
This note presents technical details of a SAT-based predicate abstraction technique used in ComFoRT (component formal reasoning technology).
This paper proposes to use predicate abstraction for verifying RTL Verilog, a technique successfully used for software verification.
Predicate abstraction is a popular abstraction technique employed in formal software verification. Experiments show that predicate minimization can result in a significant reduction of both verification time and memory usage compared to earlier methods.