Alloy Case Studies

Laplace Equation Solver in Coarray Fortran

An HPC practitioner's workbench for formal refinement checking. J. Benavides, J. Baugh, and G. Gopalakrishnan. In LCPC 2022: 35th International Workshop on Languages and Compilers for Parallel Computing (to appear, pdf)

Base Model – abstract and concrete models and an abstraction function that relates them
jacobi.als
Adequacy – show that every abstract state has a concrete counterpart
adequacy.als
Functional – show that the abstraction function alpha is functional
functional.als
Total – show that the abstraction function alpha is total
total.als
Correct – show that the refinement is correct (a safety check)
correct.als
Progress – show that the concrete operator (JacobiStep) is total
progress.als

Sparse Matrices

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

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

Models of scientific software: A state-based approach. T. Dyer. In Lightweight Formal Methods in Scientific Computing, Chapter 2, Ph.D. Dissertation, NCSU (pdf)

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: Fri Dec 16, 2022