Program

Accepted Papers

• Arthur Amorim, Max Taylor, Trevor Kann, William Harrison, Gary Leavens, and Lance Joneckis. Enforcing MAVLink Safety & Security Properties Via Refined Multiparty Session Types
• Ziggy Attala, Fang Yan, Simon Foster, Ana Cavalcanti, and Jim Woodcock. Process-Algebraic Semantics for Verifying Intelligent Robotic Control Software
• Alexis Aurandt, Phillip Jones, and Kristin Yvonne Rozier. Towards a Safe, Verified Runtime Monitor for Embedded Systems: R2U2 in Embedded Rust
• Mauricio Ayala-Rincón, Thaynara Arielly de Lima, Maria Júlia Dias Lima, Mariano Moscato, and Temur Kutsia. Verification of an Anti-Unification Algorithm in PVS
• Max Bannach, Jai Grover, and Markus Hecher. Strong Structural Bounds for MaxSAT: The Fine Details of Using Neuromorphic and Quantum Hardware Accelerators
• Calvin Beck, Hanxi Chen, and Steve Zdancewic. Vellvm: Formalizing the Informal LLVM (Experience Report)
• Andrea Bombarda, Silvia Bonfanti, Angelo Gargantini, and Nico Pellegrinelli. Eliminating Flakiness: Deterministic Control for Validating Nondeterministic Asmeta Specifications
• Matías Brizzio, Felipe Gorostiaga, Cesar Sanchez, and Renzo Degiovanni. Mode-based Reactive Synthesis
• Pranav Ghorpade, Nathalie Bertrand, Sasha Rubin, Bernhard Scholz, and Pavle Subotic. Reusable Formal Verification of DAG-based Consensus Protocols
• Andreas Katis, Anastasia Mavridou, and Thomas Pressburger. A Streamlined, Formal Approach to Requirements-based Testing
• Elias Khalife, Pierre-Loic Garoche, and Mazen Farhood. Formally Proving Invariant Systemic Properties of Control Programs Using Ghost Code and Integral Quadratic Constraints
• Edward Kim, Devan Shanker, Varun Bharadwaj, Hongbeen Park, Jinkyu Kim, Hazem Torfah, Daniel Fremont, and Sanjit Seshia. Querying Labeled Time Series Data with Scenario Programs
• Ignacio D. Lopez-Miguel, Borja Fernández Adiego, Matias Salinas, and Christine Betz. Formal Verification as a Service: A CERN-GSI Case Study
• Sumio Morioka, Satoshi Obana, and Maki Yoshida. Formal Verification of Composite Field Multipliers for Information-Theoretically Secure Radio Communication in Spacecraft Control
• Mathis Niehage, Carina da Silva, Anne Remke, and Arnd Hartmanns. Rare Event Simulation for Stochastic Hybrid Systems using Symbolic Importance Functions
• Carlos Olarte, Daniel Osorio, Carlos Ramirez, and Camilo Rocha. Algorithmic Analysis of Event-B in Rewriting Logic
• Jainta Paul, Stefan Mitsch, and Luis Garcia. HyTwin: A Formal Semantics for Digital Twin Interventions in ICS Based on Time-to-Violation
• Alec Rosentrater, Zili Wang, Katherine Kosaian, and Kristin Yvonne Rozier. Language Partitioning for Mission-time Linear Temporal Logic
• Nafiz Sadman, Nastaran Kianersi, and Sean Kauffman. Visualizing Temporal Interval Hierarchies
• Mohit Tekriwal and Matthew Sottile. Mechanized RS274 semantics for additive manufacturing
• Benjamin Valpey, Xinyi Li, Sreepathi Pai, and Ganesh Gopalakrishnan. An SMT Formalization of Mixed-Precision Matrix Multiplication (Modeling Three Generations of Tensor Cores)
• Sarat Chandra Varanasi, Baoluo Meng, Robert Lorch, Abha Moitra, Kit Siu, Saswata Paul, Michael During, Neha Beniwal, and Nikita Visnevski. TRACE: Toolkit for Requirements Analysis, Capture, and Elicitation
• Jian Xiang and Stephen Chong. Extending Dynamic Logics with First-Class Relational Reasoning
• Michal Šedý and Lukáš Holík. Automata Size Reduction by Procedure Finding

Page last update: September 2024

NASA Official: César Muñoz

LaRC Privacy Statement