Formal methods can increase the quality and reliability of software systems. Unfortunately, developing libraries of formalized mathematics is expensive, time-consuming, and requires significant expertise. Program synthesis can help. This talk will first demonstrate how data-driven synthesis can decrease the amount of time and effort involved in building and verifying models of hybrid-time dynamical systems. The talk will then discuss how we plan to scale these synthesis techniques from domain-specific verification logics to more expressive and general-purpose logics.
*Texto informado pelo autor.
Registre-se com antecedência para este seminário:
Após o registro, você receberá um e-mail de confirmação contendo informações sobre conexão no seminário.
Nathan Fulton is a Research Staff Member in the newly formed MIT-IBM AI Lab, where he works on theory and tooling for building safe autonomous systems. Nathan was a core developer of the KeYmaera X theorem prover for hybrid systems, which he developed together with other members of André Platzer's Logical Systems Lab while earning his Ph.D. at Carnegie Mellon University’s Computer Science Department. KeYmaera X demonstrates how formal methods techniques can improve the safety and trustworthiness of autonomous planes, magnetic control systems, and embedded devices. Nathan also uses hybrid systems verification tooling to build verifiable safety guarantees for reinforcement learning algorithms.