BS Civil Engineering
MS Civil Engineering
PhD Civil Engineering
In Graph Utilities for Subsets we discuss how to use some of the predicates that ship with the graph utilities in Alloy on a subset of atoms in a relation as opposed to the default behavior, which is to require every atom in the supplied signature to be present in the relation. Here we’ll look at how to use the restriction operators to create subsets of relations that can be used with these utilities.
05 Dec 2018
The graph utilities that ship with Alloy are extremely useful for setting up topologies. However, a few of the predicates enforce properties to hold true over the entire supplied signature. In most cases this is the desired behavior, but occasionally it is useful to enforce the properties over a subset of the signature’s atoms.
03 Dec 2018
Proceedings of the Third International Workshop on Software Correctness for HPC Applications, Correctness '19 (to appear)
We show how to model and reason about the structure and behavior of sparse matrices, which are central to many applications in scientific computation. Our approach is state-based, relying on a formalism called Alloy to show that one model is a refinement of another. We present examples of sparse matrix-vector multiplication, transpose, and translation between formats using ELLPACK and compressed sparse row formats to demonstrate the approach. To model matrix computations in a declarative language like Alloy, a new idiom is presented for bounded iteration with incremental updates. Mechanical verification is performed using SAT solvers built into the tool.
31 Dec 2019
Abstract State Machines, Alloy, B, TLA, VDM, and Z: 6th International Conference, ABZ 2018
Control systems, protocols, and hardware design are among the most common applications of state-based formal methods, and yet the types of modeling and analysis they enable are also well-suited to problems in scientific computation, where quality, reproducibility, and productivity are growing concerns. We survey the challenges faced by developers of scientific software, characterize the nature of the programs they write, and offer some perspective on the role that state-based methods can play in scientific domains.
08 May 2018
Advances in Engineering Software
The devastation wrought by Hurricanes Katrina (2005), Ike (2008), and Sandy (2012) in recent years continues to underscore the need for better prediction and preparation in the face of storm surge and rising sea levels. Simulations of coastal flooding using physically based hydrodynamic codes like ADCIRC, while very accurate, are also computationally expensive, making them impractical for iterative design scenarios that seek to evaluate a range of countermeasures and possible failure points. We present a graphical user interface that supports local analysis of engineering design alternatives based on an exact reanalysis technique called subdomain modeling, an approach that substantially reduces the computational effort required. This interface, called the Subdomain Modeling Tool (SMT), streamlines the pre- and post-processing requirements of subdomain modeling by allowing modelers to extract regions of interest interactively and by organizing project data on the file system. Software design and implementation issues that make the approach practical, such as a novel range search algorithm, are presented. Descriptions of the overall methodology, software architecture, and performance results are given, along with a case study demonstrating its use.
12 Oct 2015
Understanding the effects of storm surge in hurricane-prone regions is necessary for protecting public and lifeline services and improving resilience. While coastal ocean hydrodynamic models like ADCIRC may be used to assess the extent of inundation, the computational cost may be prohibitive since many local changes corresponding to design and failure scenarios would ideally be considered. We present an exact reanalysis technique and corresponding implementation that enable the assessment of local subdomain changes with less computational effort than would be required by a complete resimulation of the full domain. So long as the subdomain is large enough to fully contain the altered hydrodynamics, changes may be made and simulations performed within it without the need to calculate new boundary values. Accurate results are obtained even when subdomain boundary conditions are forced only intermittently, and convergence is demonstrated by progressively increasing the frequency at which they are applied. Descriptions of the overall methodology, performance results, and accuracy, as well as case studies, are presented.
07 Jan 2015