This program is tentative and subject to change.
Cyber-Physical Systems (CPS) consist of software interacting with the physical world, such as robots, vehicles, and industrial processes. CPS are frequently responsible for the safety of lives, property, or the environment, and so software correctness must be determined with a high degree of certainty. To that end, simply testing a CPS is insufficient, as its interactions with the physical world may be difficult to predict, and unsafe conditions may not be immediately obvious. Formal verification can provide stronger safety guarantees but relies on the accuracy of the verified system in representing the real system. Bringing together verification and implementation can be challenging, as languages that are typically used to implement CPS are not easy to formally verify, and languages that lend themselves well to verification often abstract away low-level implementation details. Translation between verification and implementation languages is possible, but requires additional assurances in the translation process and increases software complexity; having both in a single language is desirable. This paper presents a formalization of MARVeLus, a CPS language which combines verification and implementation. We develop a metatheory for its synchronous refinement type system and demonstrate verified synchronous programs executing on real systems.
This program is tentative and subject to change.
Thu 5 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:00 | Refinement Types, Type InferenceICFP Papers and Events / JFP First Papers | ||
10:30 18mTalk | The Long Way to Deforestation: A Type Inference and Elaboration Technique for Removing Intermediate Data Structures ICFP Papers and Events | ||
10:48 18mTalk | Contextual Typing ICFP Papers and Events | ||
11:06 18mTalk | Synchronous Programming with Refinement Types ICFP Papers and Events Jiawei Chen University of Michigan - Ann Arbor, José Luiz Vargas de Mendonça University of Michigan at Ann Arbor, Bereket Shimels Ayele Addis Ababa Institute of Technology, Bereket Ngussie Bekele Addis Ababa Institute of Technology, Shayan Jalili University of Michigan at Ann Arbor, Pranjal Sharma University of Michigan at Ann Arbor, Nicholas Wohlfeil University of Michigan - Ann Arbor, Yicheng Zhang University of Michigan at Ann Arbor, Jean-Baptiste Jeannin University of Michigan at Ann Arbor | ||
11:24 18mTalk | Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System ICFP Papers and Events | ||
11:42 18mTalk | Trace contractsJFP First Paper JFP First Papers DOI |