Education

Research Description

Dr. Baugh's research interests include scientific computing and cyber-physical systems, formal methods for safe and trustworthy software, verification and validation, mathematical optimization and control, and applications across civil engineering including coastal, ocean, transportation, and structural systems. Current and past funding sources include the US Department of Energy, National Science Foundation, Department of Homeland Security, Federal Transit Administration, US Environmental Protection Agency, and North Carolina Supercomputing Center.

Publications

An HPC Practitioner’s Workbench for Formal Refinement Checking

Benavides, J., Baugh, J., & Gopalakrishnan, G. (2023), In Languages and Compilers for Parallel Computing (pp. 64–72). https://doi.org/10.1007/978-3-031-31445-2_5

Automatic modelling and verification of AUTOSAR architectures?

Zhang, M., Teng, Y., Kong, H., Baugh, J., Su, Y., Mi, J., & Du, B. (2023), JOURNAL OF SYSTEMS AND SOFTWARE, 201. https://doi.org/10.1016/j.jss.2023.111675

Formalisation, Abstraction and Refinement of Bond Graphs

Banach, R., & Baugh, J. (2023). , . https://doi.org/10.1007/978-3-031-36709-0_8

Significance of multi-hazard risk in design of buildings under earthquake and wind loads

Kwag, S., Gupta, A., Baugh, J., & Kim, H.-S. (2021), ENGINEERING STRUCTURES, 243. https://doi.org/10.1016/j.engstruct.2021.112623

A simple Hybrid Event-B model of an active control system for earthquake protection

Banach, R., & Baugh, J. (2020), In A. Adamatzky & V. Kendon (Eds.), From Astrophysics to Unconventional Computation (Vol. 35, pp. 157–194). https://doi.org/10.1007/978-3-030-15792-0_7

Bounded Verification of Sparse Matrix Computations

Dyer, T., Altuntas, A., & Baugh, J. (2019), 2019 IEEE/ACM 3rd International Workshop on Software Correctness for HPC Applications (Correctness), 36–43. https://doi.org/10.1109/correctness49594.2019.00010

Formal methods and finite element analysis of hurricane storm surge: A case study in software verification

Baugh, J., & Altuntas, A. (2018), SCIENCE OF COMPUTER PROGRAMMING, 158, 100–121. https://doi.org/10.1016/j.scico.2017.08.012

Hybrid theorem proving as a lightweight method for verifying numerical software

Altuntas, A., & Baugh, J. (2018), PROCEEDINGS OF CORRECTNESS 2018: 2ND IEEE/ACM INTERNATIONAL WORKSHOP ON SOFTWARE CORRECTNESS FOR HPC APPLICATIONS, pp. 1–8. https://doi.org/10.1109/Correctness.2018.00005

Numerical study on factors influencing typhoon-induced storm surge distribution in Zhanjiang Harbor

Liu, X., Jiang, W., Yang, B., & Baugh, J. (2018), Estuarine, Coastal and Shelf Science, 215, 39–51. https://doi.org/10.1016/j.ecss.2018.09.019

State-based formal methods in scientific computation

Baugh, J., & Dyer, T. (2018), In M. Butler, A. Raschke, T. S. Hoang, & K. Reichl (Eds.), Abstract State Machines, Alloy, B, TLA, VDM, and Z (pp. 392–396). https://doi.org/10.1007/978-3-319-91271-4_29

View all publications via NC State Libraries

Grants

Collaborative Research: FMitF: Track-1: Correctness at Both Ends: Rigorous ML Meets Efficient Sparse Implementations

National Science Foundation (NSF)(10/01/21 - 9/30/24)

×

Collaborative Research: FMitF: Track-1: Correctness at Both Ends: Rigorous ML Meets Efficient Sparse Implementations

Sponsor: National Science Foundation (NSF)

Start Date: 10/01/21

End Date: 9/30/24

Abstract

It takes a delicate balancing act plus a significant amount of new research to develop advanced machine learning based systems that are correct at the user level (e.g., fair treatment of the images they classify) and run reliably and efficiently on modern hardware (consume less energy and do not contain software defects). The dependency chain is a balancing act between what exists and what will be researched and developed in this project. First, higher level correctness often calls for advanced network structures such as transformers. There is significant amount of ongoing research one can draw upon. Second, such network structures cannot be implemented as such, and must be suitably sparsified (or compressed to remove unimportant weights). This is because all fully trained "original" networks are, by nature, overparameterized (finding the minima of loss functions is ideally done a higher dimensional space with more weights). Keeping the redundant weights exacerbates FLOP as well as memory requirements, and therefore one must discard unimportant weights before deployment. There are many excellent compression systems—including our own system—one can use or extend. Third, pruning merely to achieve metrics such as top-1% classification accuracy are insufficiently incisive to guarantee semantic goals (e.g., fairness). New research is needed to prune in such a way that higher level semantic goals are also met. Fourth, when sparsified in interesting ways, networks exhibit sparsity patterns that are completely data driven. One cannot find these sparse structures in existing libraries or in familiar forms such as compressed sparse row (CSR), coordinate list (COO), or ELLPACK (ELL) formats. Therefore, new research is needed in mapping these "data driven" sparsity patterns efficiently onto state-of-the-art-and fast-moving software/hardware combinations. Fifth, the sparsity patterns desired (or demanded) by top-down analysis very often does not meet what can be efficiently realized in software/hardware. Finding these efficient patterns is something for which significant expertise is needed. We find that recommendations coming from "bottom-up" analysis are often accepted without question, as ML experts working at higher levels do not have the wherewithal to deviate. So finally, there must be mechanisms to formally describe these patterns either with the view of mapping them onto the best available patterns to available or to provide the starting specifications for correctly and efficiently realizing these patterns (say in custom CUDA code or hardware). By ensuring that the top-down-desired and the bottom-up-provided "meet in the middle," the proposed research will enable the development of advanced machine learning based systems that are correct at the user level and run reliably and efficiently on modern hardware.

Close

Development and Application of a Data-Driven Methodology for Validation of Risk Informed Safety Margin Characterization Models

US Dept. of Energy (DOE)(10/01/16 - 12/30/20)

×

Development and Application of a Data-Driven Methodology for Validation of Risk Informed Safety Margin Characterization Models

Sponsor: US Dept. of Energy (DOE)

Start Date: 10/01/16

End Date: 12/30/20

Abstract

This project will develop methodology for verification and validation of advanced computer models used in Risk-Informed Safety Margin Characterization (RISMC) of nuclear power plants. The project will apply the methodology to selected problems in nuclear reactor safety. The focus is placed on computer codes that simulate external hazards that have impact on plant safety, including severe accident management and emergency response. The project will collect, characterize, archive, and use data from plant measurements, integral-effect and separate-effect tests to support code validation. The methodology will bring to use probabilistic risk assessment (PRA) to guide a risk-informed validation approach implementation.

Close

Engineering for Resilient Civil Infrastructure Systems: A Graduate Research Fellowship Program

US Dept. of Homeland Security (DHS)(9/30/09 - 9/30/13)

×

Engineering for Resilient Civil Infrastructure Systems: A Graduate Research Fellowship Program

Sponsor: US Dept. of Homeland Security (DHS)

Start Date: 9/30/09

End Date: 9/30/13

Abstract

The purpose of this proposal is to establish a graduate research fellowship program to train students to be future leaders in the area of engineering of resilient civil infrastructure systems for coastal regions considering natural hazards. This program will be conducted in coordination with the ongoing DHS Center of Excellence on Natural Disasters, Coastal Infrastructure and Emergency Management.

Close

Engineering the Civil Infrastructure For Enhanced Resiliance of the Built and Natural Environments

US Dept. of Homeland Security (DHS)(7/01/08 - 6/30/15)

×

Engineering the Civil Infrastructure For Enhanced Resiliance of the Built and Natural Environments

Sponsor: US Dept. of Homeland Security (DHS)

Start Date: 7/01/08

End Date: 6/30/15

Abstract

The dynamic evolution of landforms under stress can lead to catastrophic loss of either functionality or of mass itself. This project will examine the dynamics of landforms undergoing a transition from one state to another (e.g., barrier island collapse, wetland loss, dune erosion) in order to determine critical defining features of the resilient natural and developed landforms. This descriptive dynamic will be translated into design parameters for restoration of protective or beneficial landforms (e.g., beaches, dunes, barrier islands, wetlands). In addition, this analysis will be used to provide improved metrics for communicating hazard and risk as well as incorporating hazard and risk into land use plans. This project lies at the interface between Coastal Hazards Science and Planning for Resilience focus areas and has the potential to provide insights to the Hazards, Human Behavior and Economic Resilience focus area.

Close

Modeling and Optimization of Civil Engineering Infrastructure

Blue Ridge Analytics, Inc.(12/01/04 - 4/30/06)

×

Modeling and Optimization of Civil Engineering Infrastructure

Sponsor: Blue Ridge Analytics, Inc.

Start Date: 12/01/04

End Date: 4/30/06

Abstract

The project will develop computer software to implement mathematical models designed to represent civil engineering infrastructure problems. In addition, the software will implement optimization techniques, such as mathematical programming and heuristic search methods. The techniques will be implemented so that alternative solutions, which meet given constraints on modeled objectives, will be obtained and provided to a user of the software.

Close