2026-07-25T06:17:24Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5020 2024-03-06T10:35:42Z ddc:004 open_access

Toward a Dependability Case Language and Workflow for a Radiation Therapy System Ernst, Michael D. Grossman, Dan Jacky, Jon Loncaric, Calvin Pernsteiner, Stuart Tatlock, Zachary Torlak, Emina Wang, Xi Synthesis Proof Assistants Verification Dependability Cases Domain Specific Languages Radiation Therapy We present a near-future research agenda for bringing a suite of modern programming-languages verification tools - specifically interactive theorem proving, solver-aided languages, and formally defined domain-specific languages - to the development of a specific safety-critical system, a radiotherapy medical device. We sketch how we believe recent programming-languages research advances can merge with existing best practices for safety-critical systems to increase system assurance and developer productivity. We motivate hypotheses central to our agenda: That we should start with a single specific system and that we need to integrate a variety of complementary verification and synthesis tools into system development. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Michael D. Ernst and Dan Grossman and Jon Jacky and Calvin Loncaric and Stuart Pernsteiner and Zachary Tatlock and Emina Torlak and Xi Wang 2015 Is Part Of LIPIcs, Volume 32, 1st Summit on Advances in Programming Languages (SNAPL 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SNAPL.2015.103 urn:nbn:de:0030-drops-50208 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2015.103 eng https://creativecommons.org/licenses/by/3.0/legalcode