2 papers
cs.LO2025
ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems
Eric Vin, Kyle A. Miller, Inigo Incer +2
Full verification of learning-enabled cyber-physical systems (CPS) has long been intractable due to challenges including black-box components and complex real-world environments. E…
cs.LO2025
LeanLTL: A unifying framework for linear temporal logics in Lean
Eric Vin, Kyle A. Miller, Daniel J. Fremont
We propose LeanLTL, a unifying framework for linear temporal logics in Lean 4. LeanLTL supports reasoning about traces that represent either infinite or finite linear time. The lib…