A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic
David Basin, Thibault Dardinier, Lukas Heimes, Srđan Krstić, Martin Raszyk, Joshua Schneider, Dmitriy Traytel
Topics & Concepts
HOLComputer scienceCorrectnessJoinsTemporal logicMetric (unit)Window (computing)Programming languageSliding window protocolLinear temporal logicDynamic logic (digital electronics)Theoretical computer scienceDistributed computingAlgorithmOperating systemQuantum mechanicsPhysicsOperations managementTransistorEconomicsVoltageFormal Methods in VerificationLogic, programming, and type systemsSoftware Testing and Debugging Techniques