TACPS 2025 (July) was held successfully

🎉🎉🎉 Congratulations! The third TACPS was successfully held in conjunction with CAV in Zagreb, Croatia!

The 3rd TACPS: Neurosymbolic and Foundation Models for AI verification in Autonomous CPS

The integration of machine learning (ML) into cyber-physical systems (CPS) has revolutionized applications such as self-driving cars, delivery drones, service robotics, and automated medical procedures. However, the deployment of these systems has brought safety and reliability concerns to the forefront, with real-world failures resulting in fatalities and economic losses. These incidents underscore the urgent need for robust verification and validation methodologies tailored to ML-driven CPS.

Traditional verification techniques face significant challenges in addressing the complexities of ML components within CPS. These challenges include the reliance on representative training data, susceptibility to out-of-distribution inputs, and the black-box, non-explainable nature of ML models. Existing tools, such as hybrid automata, fall short of adequately modeling and reasoning about these systems, necessitating innovative approaches to ensure their safety and reliability.

Emerging technologies, particularly neurosymbolic methods and foundation models like Large Language Models (LLMs), offer transformative potential in this domain. By combining symbolic reasoning with data-driven learning, these approaches facilitate the generation of interpretable representations, extraction of formal specifications, and rigorous handling of uncertainty in ML-based systems. Such advancements not only enhance test generation and issue discovery but also pave the way for extending formal verification to learning-enabled CPS. These contributions are critical for addressing the probabilistic behaviors and transparency challenges inherent in AI components, making them pivotal for the verification and reliability of autonomous CPS.

This workshop aims to bring together researchers and practitioners from the verification, ML, and CPS communities to explore the integration of neurosymbolic approaches and foundation models into the formal verification landscape. Through interdisciplinary discussions, the workshop seeks to advance the state-of-the-art in verifying learning-enabled CPS and ensuring the safety and reliability of AI-driven autonomous systems.

Program

• 08:30 – 09:00 | Breakfast & Registration
  • Opening Remarks 08:50 – 09:00 (Xi Zheng, Ivan Ruchkin, Ziyang Li)
• 09:00 – 10:30 | Keynote Session I & II (Session Chair: Xi Zheng)
  • Keynote I: Bridging Learning and Reasoning: From Solvers to LLMs — Prof. Vijay Ganesh, Georgia Tech (40 mins talk + 5 mins Q&A)
  • Keynote II: Neuro-Symbolic Verification (Verification Beyond Fairness and Robustness) — Prof. Daniel Neider, TU Dortmund (40 mins talk + 5 mins Q&A)
• 10:30 – 11:00 | Coffee Break
• 11:00 – 12:00 | Paper Presentations (Each paper: 15 min presentation + 5 min Q&A, Session Chair: Ivan Ruchkin)
  • A Vision for Model Checking Counterexample Explainability Via Neurosymbolic Reasoning. Kristin Yvonne Rozier, Iowa State University of Science and Technology, USA
  • Runtime Verification of Prediction. Stefano Tonetta, Fondazione Bruno Kessler, Italy
  • Neurosymbolic Feature Extraction for Identifying Forced Labor in Supply Chains. Zili Wang, Frank Montabon, Kristin Yvonne Rozier, Iowa State University, USA
• 12:00 – 14:00 | Lunch Break
• 14:00 – 15:30 | Verification, Scallop, and NeuroStrata Session (25 minutes for each talk plus 5 minutes Q&A, Session Chair: Ziyang Li)
  • 14:00–14:30: State-Dependent Conformal Perception Bounds for Neuro-Symbolic Verification — Ivan Ruchkin, University of Florida
  • 14:30–15:00: Scallop — Ziyang Li, Johns Hopkins University
  • 15:00–15:30: NeuroStrata — Xi Zheng, Macquarie University
• 15:30 – 16:00 | Coffee Break
• 16:00 – 17:30 | Panel Discussion (Panel Chair: Xi Zheng)
  • Theme: What’s Next for NeuroSymbolic Reasoning: Toward Shonan and Dagstuhl Seminars.
    Panellists: Vijay Ganesh, Daniel Neider, Ivan Ruchkin, Ziyang Li

Technical Program Committee

• Xi Zheng, Macquarie University, Australia
• Ivan Ruchkin, University of Florida, USA
• Ziyang Li, University of Pennsylvania, USA
• Oleg Sokolsky, University of Pennsylvania, USA
• Sanjoy Baruah, Washington University in St. Louis, USA
• Aloysius K. Mok, The University of Texas at Austin, USA
• Lars Lindemann, University of Southern California, USA
• Hang Qiu, University of California, Riverside, USA
• Bryan Donyanavard, San Diego State University, USA
• Shan Lin, Stony Brook University, USA
• Parasara Sridhar Duggirala, The University of North Carolina at Chapel Hill, USA
• Simin Nadjm-Tehrani, Linköping University, Sweden
• Elena Troubitsyna, KTH, Sweden