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.go

An 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


Web
Analytics