BEGIN:VCALENDAR VERSION:2.0 PRODID:-//Talks.cam//talks.cam.ac.uk// X-WR-CALNAME:Talks.cam BEGIN:VEVENT SUMMARY:Trusted Autonomous Systems: Verification Meets Falsification - Ser giy Bogomolov DTSTART:20220727T130000Z DTEND:20220727T133000Z UID:TALK176951@talks.cam.ac.uk DESCRIPTION:Cyber-physical systems (CPS) are networks of physical and digi tal components and present a next generation of large-scale highly-interco nnected networked embedded systems. On the one hand\, CPS open enormous op portunities as they form the core of emerging smart devices and services w hich are going to revolutionize many traditional industries such as automo tive\, traffic management\, power generation and delivery\, as well as man ufacturing. On the other hand\, highly autonomous systems pose special eng ineering challenges as any unexpected behaviour might lead to large financ ial losses or even human deaths. \;\nIn this talk\, we address this ch allenge and propose automatic techniques to analyze CPS. For this purpose\ , we use the concept of hybrid automata which has proven to be particularl y useful to model CPS. \;\nFalsification algorithms for hybrid automat a aim at finding trajectories that violate a given safety property. This i s a challenging problem\, and the practical applicability of current falsi fication algorithms still suffers from their high time complexity. In cont rast to falsification\, verification algorithms aim at providing guarantee s that no such trajectories exist. Recent symbolic reachability techniques are capable of efficiently computing linear constraints that enclose all trajectories of the system with reasonable precision. \;\nIn this talk \, we present an approach which leverages the power of symbolic reachabili ty algorithms to improve the scalability of falsification techniques. Rece nt approaches to falsification reduce the problem to a nonlinear optimizat ion problem. We propose to reduce the search space of the optimization pro blem by adding linear state constraints computed by a reachability algorit hm. We showcase the efficiency of our approach on a number of standard hyb rid systems benchmarks demonstrating the performance increase in speed and the number of falsifiable instances. \; LOCATION:Discussion Room\, Newton Institute END:VEVENT END:VCALENDAR