Designed especially for neurobiologists, FluoRender is an interactive tool for multi-channel fluorescence microscopy data visualization and analysis.
Deep brain stimulation
BrainStimulator is a set of networks that are used in SCIRun to perform simulations of brain stimulation such as transcranial direct current stimulation (tDCS) and magnetic transcranial stimulation (TMS).
Developing software tools for science has always been a central vision of the SCI Institute.

Scientific Computing

Numerical simulation of real-world phenomena provides fertile ground for building interdisciplinary relationships. The SCI Institute has a long tradition of building these relationships in a win-win fashion – a win for the theoretical and algorithmic development of numerical modeling and simulation techniques and a win for the discipline-specific science of interest. High-order and adaptive methods, uncertainty quantification, complexity analysis, and parallelization are just some of the topics being investigated by SCI faculty. These areas of computing are being applied to a wide variety of engineering applications ranging from fluid mechanics and solid mechanics to bioelectricity.


Martin Berzins

Parallel Computing

Mike Kirby

Finite Element Methods
Uncertainty Quantification

Valerio Pascucci

Scientific Data Management

Chris Johnson

Problem Solving Environments

Amir Arzani

Scientific machine learning
Data-driven fluid flow modeling

Funded Research Projects:

Publications in Scientific Computing:

Implementing Efficient Dynamic Formal Verification Methods for MPI Programs
S. Vakkalanka, M. DeLisi, G. Gopalakrishnan, R.M. Kirby, R. Thakur, W. Gropp. In Recent Advances in Parallel Virtual Machine and Message Passing Interface Lecture Notes in Computer Science, Dublin, Ireland, Vol. 5205, pp. 248--256. September, 2008.

We examine the problem of formally verifying MPI programs for safety properties through an efficient dynamic (runtime) method in which the processes of a given MPI program are executed under the control of an interleaving scheduler. To ensure full coverage for given input test data, the algorithm must take into consideration MPI’s out-of-order completion semantics. The algorithm must also ensure that nondeterministic constructs (e.g., MPI wildcard receive matches) are executed in all possible ways. Our new algorithm rewrites wildcard receives to specific receives, one for each sender that can potentially match with the receive. It then recursively explores each case of the specific receives. The list of potential senders matching a receive is determined through a runtime algorithm that exploits MPI’s operation ordering semantics. Our verification tool ISP that incorporates this algorithm efficiently verifies several programs and finds bugs missed by existing informal verification tools.

Scheduling Considerations for Building Dynamic Verification Tools for MPI
S. Vakkalanka, M. DeLisi, G. Gopalakrishnan, R.M. Kirby. In Proceedings of the 6th Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging, Seattle, WA, PADTAD '08, Vol. 3, ACM, pp. 1--6. 2008.
ISBN: 978-1-60558-052-4
DOI: 10.1145/1390841.1390844

Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings
S. Vakkalanka, G. Gopalakrishnan, R.M. Kirby. In Computer Aided Verification Lecture Notes in Computer Science , Vol. 5123, pp. 66--79. July, 2008.
DOI: 10.1007/978-3-540-70545-1_9

Dynamic verification methods are the natural choice for debugging real world programs when model extraction and maintenance are expensive. Message passing programs written using the MPI library fall under this category. Partial order reduction can be very effective for MPI programs because for each process, all its local computational steps, as well as many of its MPI calls, commute with the corresponding steps of all other processes. However, when dependencies arise among MPI calls, they are often a function of the runtime state. While this suggests the use of dynamic partial order reduction (DPOR), three aspects of MPI make previous DPOR algorithms inapplicable: (i) many MPI calls are allowed to complete out of program order; (ii) MPI has global synchronization operations (e.g., barrier) that have a special weak semantics; and (iii) the runtime of MPI cannot, without intrusive modifications, be forced to pursue a specific interleaving because of MPI’s liberal message matching rules, especially pertaining to ‘wildcard receives’. We describe our new dynamic verification algorithm ‘POE’ that exploits the out of order completion semantics of MPI by delaying the issuance of MPI calls, issuing them only according to the formation of match-sets, which are ample ‘big-step’ moves. POE guarantees to manifest any feasible interleaving by dynamically rewriting wildcard receives by specific-source receives. This is the first dynamic model-checking algorithm with reductions for (a large subset of) MPI that guarantees to catch all deadlocks and local assertion violations, and is found to work well in practice.

A Formal Approach to Detect Functionally Irrelevant Barriers in MPI Programs
S. Sharma, S. Vakkalanka, G. Gopalakrishnan, R.M. Kirby, R. Thakur, W. Gropp. In Proceedings of EuroPVM-MPI 2008, Dublin, Ireland, Vol. 5205, pp. 265--273. September, 2008.
DOI: 10.1007/978-3-540-87475-1_36

We examine the unsolved problem of automatically and efficiently detecting functionally irrelevant barriers in MPI programs. A functionally irrelevant barrier is a set of MPI_Barrier calls, one per MPI process, such that their removal does not alter the overall MPI communication structure of the program. Static analysis methods are incapable of solving this problem, as MPI programs can compute many quantities at runtime, including send targets, receive sources, tags, and communicators, and also can have data-dependent control flows. We offer an algorithm called Fib to solve this problem based on dynamic (runtime) analysis. Fib applies to MPI programs that employ 24 widely used two-sided MPI operations. We show that it is sufficient to detect barrier calls whose removal causes a wildcard receive statement placed before or after a barrier to now begin matching a send statement with which it did not match before. Fib determines whether a barrier becomes relevant in any interleaving of the MPI processes of a given MPI program. Since the number of interleavings can grow exponentially with the number of processes, Fib employs a sound method to drastically reduce this number, by computing only the relevant interleavings. We show that many MPI programs do not have data dependent control flows, thus making the results of Fib applicable to all the input data the program can accept.

Building Blocks for Computer Vision with Stochastic Partial Differential Equations
T. Preusser, H. Scharr, K. Krajsek, R.M. Kirby. In International Journal of Computer Vision, Vol. 80, No. 3, Springer, pp. 375--405. July, 2008.
DOI: 10.1007/s11263-008-0145-5

Examination and Analysis of Implementation Choices within the Material Point Method (MPM)
M. Steffen, P.C. Wallstedt, J.E. Guilkey, R.M. Kirby, M. Berzins. In Computer Modeling in Engineering & Sciences, Vol. 31, No. 2, pp. 107--127. 2008.

CRA-NIH Computing Research Challenges in Biomedicine Workshop Recommendations
D. Reed, C.R. Johnson. Note: Computing Research Association (CRA), 2007.

Dynamically identifying and tracking contaminants in water bodies
C.C. Douglas, M.J. Cole, P. Dostert, Y. Efendiev, R.E. Ewing, G. Haase, J. Hatcher, M. Iskandarani, C.R. Johnson, R.A. Lodder. In Proceedings of the 7th International Conference on Computational Science (ICCS) 2007, Part I, Beijing, China, Lecture Notes in Computer Science (LNCS), Vol. 4887, Edited by Y. Shi and G.D. van Albada and P.M.A. Sloot and J.J. Dongarra, Springer-Verlag, Berlin Heidelberg, pp. 1002--1009. May, 2007.

Dynamic data-driven application systems for empty houses, contaminat tracking, and wildland fireline prediction
C.C. Douglas, D. Bansal, J.D. Beezley, L.S. Bennethum, S. Chakraborty, J.L. Coen, Y. Efendiev, R.E. Ewing, J. Hatcher, M. Iskandarani, C.R. Johnson, M. Kim, D. Li, R.A. Lodder, J. Mandel, G. Qin, A. Vodacek. In Grid-Based Problem Solving Environments, IFIP series, Edited by P.W. Gaffney and J.C.T. Pool, Springer-Verlag, Berlin, pp. 255-272. 2007.
DOI: 10.1007/978-0-387-73659-4_14

BioMesh3D: A Meshing Pipeline for Biomedical Models
SCI Institute Technical Report, M. Callahan, M.J. Cole, J.F. Shepherd, J.G. Stinstra, C.R. Johnson. No. UUSCI-2007-009, University of Utah, 2007.

Hexahedral Mesh Generation for Biomedical Models in SCIRun
SCI Institute Technical Report, J.F. Shepherd, C.R. Johnson. No. UUSCI-2007-008, University of Utah, 2007.

A Meshing Pipeline for Biomedical Computing
M. Callahan, M.J. Cole, J.F. Shepherd, J.G. Stinstra, C.R. Johnson. In Engineering with Computers, Special Issue on Computational Bioengineering, pp. (in press). 2007.

NSF Blue Ribbon Panel Report on Simulation Based Engineering Science
J.T. Oden, J. Fish, C.R. Johnson, A. Laub, D. Srolovitz, T. Belytschko, T.J.R. Hughes, D. Keys, L. Petzold, S. Yip. Note: NSF Report, 2006.

Purpose: To explore the emerging discipline of Simulation Simulation-Based Engineering Science, its major components, its importance to the nation, the challenges and barriers to its advancement, and to recommend to the NSF and the broader community concerned with science and engineering in the United States, steps that could be taken to advance development in this discipline.

Towards Stable Coupling Methods for High-Order Discretizations of Fluid-Structure Interaction: Algorithms and Observations
R.M. Kirby, Z. Yosibash, G.E. Karniadakis. In Journal of Computational Physics, Vol. 223, No. 2, pp. 489--518. 2006.

A One-Dimensional Model of the Navier-Stokes
SCI Institute Technical Report, H. Marmanis, C.W. Hamman, R.M. Kirby. No. UUSCI-2006-012, University of Utah, 2006.

Biomedical Computing and Visualization
C.R. Johnson, D.M. Weinstein. In Proceedings of the Twenty-Ninth Australasian Computer Science Conference (ACSC2006): Conferences in Research and Practice in Information Technology (CRPIT), Hobart, Australia, Vol. 48, Edited by Vladimir Estivill-Castro and Gill Dobbie, pp. 3-10. 2006.

Advanced Reaction-Diffusion Models for Texture Synthesis
A.R. Sanderson, R.M. Kirby, C.R. Johnson, L. Yang. In Journal of Graphics Tools, Vol. 11, No. 3, pp. 47--71. 2006.

Parallel and Distributed Model Checking in Eddy
I. Melatti, R. Palmer, G. Sawaya, Y. Yang, R.M. Kirby, G. Gopalakrishnan. In Model Checking Software: Proceedings of the 13th International SPIN Workshop (SPIN 2006), Austria, Vol. 3925/2006, pp. 108--125. 2006.

Involving Undergraduates in Computational Science and Engineering Research: Successes and Challenges
R.M. Kirby, C.R. Johnson, M. Berzins. In Proceedings of Computational Science - ICCS 2006: 6th International Conference, Reading, UK, Lecture Notes in Computer Science, Vol. 3992, May 28-31, 2006.

Aliasing Errors Due to Quadratic Non-Linearities On Triangular Spectral/hp Element Discretisations
R.M. Kirby, S.J. Sherwin. In Journal of Engineering Mathematics, Vol. 56, pp. 273--288. 2006.