CSE Technical Reports Sorted by Technical Report Number
| TR Number | Title | Authors | Date | Pages |
| CSE-TR-001-18 | On Cuba, Diplomats, Ultrasound, and Intermodulation Distortion | Chen Yan, Kevin Fu, Wenyuan Xu | March, 2018 | 30 |
| This technical report analyzes how ultrasound could have led to the AP news recordings of metallic sounds reportedly heard by diplomats in Cuba. Beginning with screen shots of the acoustic spectral plots from the AP news, we reverse engineered ultrasonic signals that could lead to those outcomes as a result of intermodulation distortion and non-linearities of the acoustic transmission medium. We created a proof of concept eavesdropping device to exfiltrate information by AM modulation over an inaudible ultrasonic carrier. When a second inaudible ultrasonic source interfered with the primary inaudible ultrasonic source, intermodulation distortion created audible byproducts that share spectral characteristics with audio from the AP news. Our conclusion is that if ultrasound played a role in harming diplomats in Cuba, then a plausible cause is intermodulation distortion between ultrasonic signals that unintentionally synthesize audible tones. In other words, acoustic interference without malicious intent to cause harm could have led to the audible sensations in Cuba. |
| CSE-TR-002-18 | EUForia: Uninterpreted Functions Abstraction with Incremental Induction | Denis Bueno and Karem A. Sakallah | June , 2018 | 29 |
| We investigate a novel algorithm for an IC3-style checker that operates entirely at the level of equality with uninterpreted functions (EUF). EUF abstraction is efficient to compute from a word-level transition system, whereas predicate abstraction typically requires a (possibly exponential) number of calls to a theorem prover. Data operations are treated as uninterpreted functions and relations as uninterpreted predicates. Our checker, called EUForia, checks a transition system for a given safety property and either (1) discovers an inductive strengthening EUF formula or (2) produces an abstract counterexample which corresponds to zero, one, or many concrete counterexamples. We also present a simple method for computing renement lemmas that checks the feasibility of the abstract counterexamples. We formalize the EUF transition system, prove our algorithm correct, and demonstrate our results on a subset of benchmarks from the software verication competition (SV-COMP) 2017. |
Technical Reports Page