## Alloy Case Studies

## Sparse Matrices

## Reference

Bounded verification of sparse matrix computations. T. Dyer, A. Aluntas, and J. Baugh.2019 IEEE/ACM 3rd International Workshop on Software Correctness for HPC Applications (Correctness), 36-43 (pdf)

III. Matrix Structure

Basic model for values and matrices in dense, ELL, and CSR formats

structure.als

IV. Matrix Behavior

ELL and CSR abstraction functions, update operations for dense and ELL formats

behavior.als

V.B. ELL to CSR Translation

Translation operations from ELL to CSR formats

translate.als

V.C. CSR Transpose

Transpose operations for dense and CSR formats

transpose.als

V.D. CSR Matrix-Vector Multiplication

Matrix-vector multiplication for dense and CSR formats

mvm.als

## Hurricane Storm Surge

## Reference

Formal methods and finite element analysis of hurricane storm surge: A case study in software verification. J. Baugh and A. Altuntas.Science of Computer Programming, 158: 100-121. 2018 (pdf)

3. Statics: Representing a mesh

Model the topology of meshes that are made up of triangles and vertices

mesh.als

4. Dynamics: Wetting and drying

A model of ADCIRC's wetting and drying algorithm

wetdry.als

5. Full and subdomain runs

Compare full and subdomain runs of the wet-dry algorithm

fullsub.als

5.2. An alternative approach for full and subdomain runs

Compare full and subdomain runs: an alternative approach

fullsub2.als

6. Role in understanding empirical algorithms

Question: why would an element with three wet nodes be dry?

question.als

## Related

Modeling a discrete wet-dry algorithm for hurricane storm surge in Alloy. J. Baugh and A. Altuntas. In Abstract State Machines, Alloy, B, TLA, VDM, and Z: 5th International Conference, ABZ 2016, pages 256-261, Cham, 2016. Springer Lecture Notes in Computer Science 9675 (pdf) An exact reanalysis technique for storm surge and tides in a geographic region of interest. J. Baugh, A. Altuntas, T. Dyer, and J. Simon. Coastal Engineering, 97: 60-77. 2015 (pdf)

## Hardy Cross Method of Moment Distribution

## Reference

Models of scientific software: A state-based approach. J. Baugh, T. Dyer, and A. Altuntas. submitted

III. d. Illustrative Example: Specification in Alloy

Specification of the Hardy Cross method of moment distribution

hcmSpec.als, hcmSpecSim.als

III. e. Illustrative Example: Refinement

A refinement with communicating processes: a process for each joint and communication between them using synchronous message passing

hcmRef.als, hcmRefSim.als

III. e. Illustrative Example: Refinement

An implementation of the Baugh/Liu example in Go using parallel goroutines and message passing, and with guarded select statements that mimic similar capabilities found in CSP

hcm.goAn implementation that includes Dijkstra's ring-based detection algorithm

hcm2.go

## Related

State-based formal methods in scientific computation. Baugh, J.; and Dyer, T. In Abstract State Machines, Alloy, B, TLA, VDM, and Z: 6th International Conference, ABZ 2018, pages 392-396, Cham, 2018. Springer Lecture Notes in Computer Science 10817 (pdf) A general characterization of the Hardy Cross method as sequential and multiprocess algorithms. J. Baugh and S. Liu.Structures,6: 170-181. 2016 (pdf)

Last updated: Tue Apr 7, 2020 by John Baugh at NC State University