SOUND PROPAGATION AND SCATTERING IN BUBBLY LIQUIDS

In the ocean, natural and artificial processes generate clouds of bubbles which scatter and attenuate sound. Measurements have shown that at the individual bubble resonance frequency, sound propagation in this medium is highly attenuated and dispersive. Theory to explain this behavior exists in the literature, and is adequate away from resonance. However, due to excessive attenuation near resonance, little experimental data exists for comparison. An impedance tube was developed specifically for exploring this regime. Using the instrument, unique phase speed and attenuation measurements were made for void fractions ranging from 6.2 × 10^−5 to 2.7 × 10^−3 and bubble sizes centered around 0.62 mm in radius. Improved measurement speed, accuracy and precision is possible with the new instrument, and both instantaneous and time-averaged measurements were obtained. Behavior at resonance was observed to be sensitive to the bubble population statistics and agreed with existing theory, within the uncertainty of the bubble population parameters. Scattering from acoustically compact bubble clouds can be predicted from classical scattering theory by using an effective medium description of the bubbly fluid interior. Experimental verification was previously obtained up to the lowest resonance frequency. A novel bubble production technique has been employed to obtain unique scattering measurements with a bubbly-liquid-filled latex tube in a large indoor tank. The effective scattering model described these measurements up to three times the lowest resonance frequency of the structure.

Improving the Accessibility of Lightweight Formal Verification Systems

In research areas involving mathematical rigor, there are numerous benefits to adopting a formal representation of models and arguments: reusability, automatic evaluation of examples, and verification of consistency and correctness. However, broad accessibility has not been a priority in the design of formal verification tools that can provide these benefits. We propose a few design criteria to address these issues: a simple, familiar, and conventional concrete syntax that is independent of any environment, application, or verification strategy, and the possibility of reducing workload and entry costs by employing features selectively. We demonstrate the feasibility of satisfying such criteria by presenting our own formal representation and verification system. Our system’s concrete syntax overlaps with English, LATEX and MediaWiki markup wherever possible, and its verifier relies on heuristic search techniques that make the formal authoring process more manageable and consistent with prevailing practices. We employ techniques and algorithms that ensure a simple, uniform, and flexible definition and design for the system, so that it easy to augment, extend, and improve.