52 citations
- Georgia Institute of TechnologyUS3 papers
- United States Air Force Research LaboratoryUS3 papers
- Cornell UniversityUS2 papers
- Purdue University West LafayetteUS2 papers
- University of Colorado BoulderUS2 papers
- Amazon (United States)US1 paper
- Artificial Intelligence in Medicine (Canada)CA1 paper
- Carnegie Mellon UniversityUS1 paper
- City St George's, University of LondonGB1 paper
- Clarkson UniversityUS1 paper
- Dependable Computing (United States)US1 paper
- Film IndependentUS1 paper
21 papers
Lazy Arithmetic using Systolic Arrays for Closing the Verification Gap on Embedded Systems
Taisa Kushner, Ryan McCleeary, Martin Brain
Complex algorithms such as deep neural networks are increasingly being deployed on embedded, resource constrained platforms. However, existing hardware and software schemes for imp…
CNnotator: LLM-Guided Memory Safety Annotation Synthesis
Twain Byrnes, Mike Dodds
Memory safety errors account for a large proportion of security bugs in systems written in C; modern languages such as Java and Rust prevent such bugs because they are memory-safe…
The CoCompiler: DSL Lifting via Relational Compilation
Naomi Spargo, Santiago Cuéllar, Jonathan Daugherty +2
Lifting low-level or legacy code into a domain-specific language (DSL) improves our ability to understand it, enables deeper formal reasoning, and facilitates safe modification. We…
A Physiologically-Constrained Neural Network Digital Twin Framework for Replicating Glucose Dynamics in Type 1 Diabetes
Valentina Roquemen-Echeverri, Taisa Kushner, Peter G. Jacobs +1
Simulating glucose dynamics in individuals with type 1 diabetes (T1D) is critical for developing personalized treatments and supporting data-driven clinical decisions. Existing mod…
Combining AI Control Systems and Human Decision Support via Robustness and Criticality
Walt Woods, Alexander Grushin, Simon Khan +1
AI-enabled capabilities are reaching the requisite level of maturity to be deployed in the real world, yet do not always make correct or safe decisions. One way of addressing these…
KATch: A Fast Symbolic Verifier for NetKAT
Mark Moeller, Jules Jacobs, Olivier Savary Belanger +5
We develop new data structures and algorithms for checking verification queries in NetKAT, a domain-specific language for specifying the behavior of network data planes. Our result…