Jean-Baptiste JEANNIN from the University of Michigan (Michigan USA), will be giving a talk this Thursday 12th December 2024 about synchronous programming and cyber-physical systems.
Title: Synchronous Programming with Refinement Types
This talk will present MARVeLus, a cyber-physical systems language which combines verification, simulation, and implementation. The language is based on Zélus, a modern version of Lustre, where we add refinement types and associated typing rules. Our refinement types can express temporal-logic-based safety properties and prove them using a rich type system in the style of deductive verification. The language comes with an implementation, and a platform enabling execution on physical robots. Although our current implementation is limited to verifying properties about discrete constructs of Zélus, the talk will also present early efforts extending the proof systems to continuous constructs of Zélus, inspired by differential dynamic logic.
About 68nqrt:
68 Computer Science
N Software
Q Theory of computing
R Discrete mathematics in relation to computer science
T Artificial intelligence