Cyclist: Verifying Programs using Cyclic Proof (available)

Cyclic proofs are a technique for proving properties inductively, or proving properties about inductively defined objects or processes. They can be used to prove logical statements, or to verify recursive programs. The Cyclist tool [1] has been developed as an automatic verification tool based on cyclic proofs. It can prove termination and verify temporal properties … full description “Cyclist: Verifying Programs using Cyclic Proof (available)”

Machine Learning for Cyber-Physical Systems Monitoring (available)

Hybrid automata (HA) are a formal model for cyber-physical systems, i.e., systems characterised by digital components (discrete) that control and interact with the physical environment (continuous). HAs have been applied to system designs in numerous domains including avionics, automotive, medical devices, and robotics. Formal verification of HAs can establish, with provable correctness guarantees, whether or … full description “Machine Learning for Cyber-Physical Systems Monitoring (available)”