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.

SCI Publications

2009


H. Mirzaee, C. Eskilsson, S.J. Sherwin, R.M. Kirby. “Comparison of Consistent Integration Versus Adaptive Quadrature for Taming Aliasing Errors,” SCI Technical Report, No. UUSCI-2009-008, SCI Institute, University of Utah, 2009.



J.S. Preston, T. Tasdizen, C.M. Terry, A.K. Cheung, R.M. Kirby. “Using the stochastic collocation method for the uncertainty quantification of drug concentration due to depot shape variability,” In IEEE Transactions on Biomedical Engineering, Vol. 56, No. 3, Note: Epub 2008 Dec 2, pp. 609--620. 2009.
PubMed ID: 19272865



A.R. Sanderson, M.D. Meyer, R.M. Kirby, C.R. Johnson. “A Framework for Exploring Numerical Solutions of Advection Reaction Diffusion Equations using a GPU Based Approach,” In Journal of Computing and Visualization in Science, Vol. 12, pp. 155--170. 2009.
DOI: 10.1007/s00791-008-0086-0



A. Vo, S. Vakkalanka, M. Delisi, G. Gopalakrishnan, R.M. Kirby, R. Thakur. “Formal Verification of Practical MPI Programs,” In Proceedings of 14th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP), Raleigh, NC, pp. 261--270. February 14-18, 2009.



D.F. Wang, R.M. Kirby, C.R. Johnson. “Finite Element Discretization Strategies for the Inverse Electrocardiographic (ECG) Problem,” In Proceedings of the 11th World Congress on Medical Physics and Biomedical Engineering, Munich, Germany, Vol. 25/2, pp. 729-732. September, 2009.



D.F. Wang, R.M. Kirby, C.R. Johnson. “Finite Element Refinements for Inverse Electrocardiography: Hybrid-Shaped Elements, High-Order Element Truncation and Variational Gradient Operator,” In Proceeding of Computers in Cardiology 2009, Park City, September, 2009.


2008


S.E. Geneser, R.M. Kirby, R.S. MacLeod. “Application of Stochastic Finite Element Methods to Study the Sensitivity of ECG Forward Modeling to Organ Conductivity,” In IEEE Transations on Biomedical Engineering, Vol. 55, No. 1, pp. 31--40. January, 2008.



C.W. Hamman, J.C. Klewicki, R.M. Kirby. “On the Lamb Vector Divergence in Navier-Stokes Flows,” In Journal of Fluid Mechanics, Vol. 610, pp. 261--284. 2008.



J.S. Hesthaven, R.M. Kirby. “Filtering in Legendre Spectral Methods,” In Mathematics of Computation, Vol. 77, No. 263, pp. 1425--1452. 2008.



R.M. Kirby, C.T. Silva. “The Need For Verifiable Visualization,” In IEEE Computer Graphics and Applications, Vol. 28, No. 5, pp. 78--83. 2008.
DOI: 10.1109/MCG.2008.103

ABSTRACT

Visualization is often employed as part of the simulation science pipeline, it's the window through which scientists examine their data for deriving new science, and the lens used to view modeling and discretization interactions within their simulations. We advocate that as a component of the simulation science pipeline, visualization must be explicitly considered as part of the validation and verification (V&V) process. In this article, the authors define V&V in the context of computational science, discuss the role of V&V in the scientific process, and present arguments for the need for verifiable visualization.



T. Martin, E. Cohen, R.M. Kirby. “Volumetric Parameterization and Trivariate B-spline Fitting using Harmonic Functions,” In Proceedings of ACM Solid and Physical Modeling, Stony Brook, NY, Note: Awarded Best Paper, pp. 269-280. 2008.



M.D. Meyer, R.T. Whitaker, R.M. Kirby, C. Ledergerber, H. Pfister. “Particle-based Sampling and Meshing of Surfaces in Multimaterial Volumes,” In IEEE Transactions on Visualization and Computer Graphics, Vol. 14, No. 6, pp. 1539--1546. 2008.



E.P. Newren, A.L. Fogelson, R.D. Guy, R.M. Kirby. “A Comparison of Implicit Solvers for the Immersed Boundary Equations,” In Computer Methods in Applied Mechanics and Engineering, Vol. 197, No. 25--28, pp. 2290--2304. 2008.
DOI: 10.1016/j.cma.2007.11.030



R. Palmer, M. DeLisi, G. Gopalakrishnan, R.M. Kirby. “An Approach to Formalization and Analysis of Message Passing Libraries,” In Proceedings of the 12th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2007), Berlin, Germany, Vol. 4916/2008, Note: Awarded Best Paper., pp. 164--181. 2008.



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



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

ABSTRACT

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.



M. Steffen, S. Curtis, R.M. Kirby, J.K. Ryan. “Investigation of Smoothness-Increasing Accuracy-Conserving Filters for Improving Streamline Integration Through Discontinuous Fields,” In IEEE Transactions on Visualization and Computer Graphics, Vol. 14, No. 3, pp. 680--692. 2008.



M. Steffen, R.M. Kirby, M. Berzins. “Analysis and Reduction of Quadrature Errors in the Material Point Method (MPM),” In International Journal for Numerical Methods in Engineering, Vol. 76, No. 6, pp. 922--948. 2008.
DOI: 10.1002/nme.2360



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



S. Vakkalanka, M. DeLisi, G. Gopalakrishnan, R.M. Kirby, R. Thakur, W. Gropp. “Implementing Efficient Dynamic Formal Verification Methods for MPI Programs,” 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.

ABSTRACT

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.