Ezio Bartocci Yliès Falcone t Martin Leucker (Eds.) f i r h c s t s e F 5 6 Formal Methods 0 3 1 S in Outer Space C N L Essays Dedicated to Klaus Havelund on the Occasion of His 65th Birthday Lecture Notes in Computer Science 13065 Founding Editors Gerhard Goos Karlsruhe Institute of Technology, Karlsruhe, Germany Juris Hartmanis Cornell University, Ithaca, NY, USA Editorial Board Members Elisa Bertino Purdue University, West Lafayette, IN, USA Wen Gao Peking University, Beijing, China Bernhard Steffen TU Dortmund University, Dortmund, Germany Gerhard Woeginger RWTH Aachen, Aachen, Germany Moti Yung Columbia University, New York, NY, USA More information about this subseries at http://www.springer.com/series/7408 è Ezio Bartocci Yli s Falcone (cid:129) (cid:129) Martin Leucker (Eds.) Formal Methods in Outer Space Essays Dedicated to Klaus Havelund on the Occasion of His 65th Birthday 123 Editors EzioBartocci Yliès Falcone TU Wien Univ. Grenoble Alpes, Inria,CNRS, Vienna,Austria Grenoble INP,LIG Grenoble,France Martin Leucker University of Lübeck Lübeck,Germany ISSN 0302-9743 ISSN 1611-3349 (electronic) Lecture Notesin Computer Science ISBN 978-3-030-87347-9 ISBN978-3-030-87348-6 (eBook) https://doi.org/10.1007/978-3-030-87348-6 LNCSSublibrary:SL2–ProgrammingandSoftwareEngineering ©SpringerNatureSwitzerlandAG2021 Thisworkissubjecttocopyright.AllrightsarereservedbythePublisher,whetherthewholeorpartofthe material is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation, broadcasting, reproduction on microfilms or in any other physical way, and transmission or information storageandretrieval,electronicadaptation,computersoftware,orbysimilarordissimilarmethodologynow knownorhereafterdeveloped. Theuseofgeneraldescriptivenames,registerednames,trademarks,servicemarks,etc.inthispublication doesnotimply,evenintheabsenceofaspecificstatement,thatsuchnamesareexemptfromtherelevant protectivelawsandregulationsandthereforefreeforgeneraluse. Thepublisher,theauthorsandtheeditorsaresafetoassumethattheadviceandinformationinthisbookare believedtobetrueandaccurateatthedateofpublication.Neitherthepublishernortheauthorsortheeditors give a warranty, expressed or implied, with respect to the material contained herein or for any errors or omissionsthatmayhavebeenmade.Thepublisherremainsneutralwithregardtojurisdictionalclaimsin publishedmapsandinstitutionalaffiliations. ThisSpringerimprintispublishedbytheregisteredcompanySpringerNatureSwitzerlandAG Theregisteredcompanyaddressis:Gewerbestrasse11,6330Cham,Switzerland Klaus Havelund (PicturebyGerardHolzmann) Preface We would have started this Preface as follows: This Festschrift is dedicated to Klaus Havelund on the occasion of his 65th birthday that was celebrated on October 17, 2020. However, due to the COVID-19 pandemic, basically all scientific events were cancelled, held digitally, or postponed in 2020. Klaus’ Festschrift and its accompa- nying symposium, which is part of the ISoLA conference series, were postponed to 2021 and currently, August 2021, a physical symposium is planned, though a rising, fourthwaveofthepandemicmayrequireanadaptionofthecurrentplans.Sowehave adaptedthebeginningofourprefaceandareoptimisticaboutholdingthesymposium: ThisFestschriftisdedicatedtoKlausHavelundontheoccasionofhis66thbirthday thatwascelebratedonOctober17,2021.Thisbookcontainsthepaperswrittenbyhis closest friends and collaborators. These papers were presented during a one-day workshop organized in his honor that was held on October 24, 2021, at Rhodes, Greece,duringthe9thInternationalSymposiumonLeveragingApplicationsofFormal Methods, Verification and Validation. Klaus started his career during his university studies as a software programmer in various Danish companies. From 1984, he held several research positions at different institutessuchastheDanishDatamaticsCenter,theÉcolePolytechnique,LIP6Labin Paris, the Computer Science Department at Aalborg University and NASA Ames. Since 2006hehasbeenworkingwithNASA’sJet Propulsion Laboratory(JPL) where hewasappointedSeniorResearchScientistin2009.JPLisafederallyfundedresearch and development center (FFRDC), managed by California Institute of Technology (Caltech), with the primary function to construct and operate planetary robotic spacecrafts. Klaus has received numerous research awards attesting to the excellence of his work. He received the Turning Goals Into Reality Engineering Innovation Award for theJavaPathFindertoolin2003,aContributionAwardforaNASAtecharticleabout innovation in 2006, an Outstanding Technology Development Award for Java PathFinderin2009,theJPLMarinerAwardforLogScope,theJPLRangerAwardfor the development of a Java coding standard, the JPL Voyager Award in recognition of his researchcontributions, andthe JPL Magellan Award for his excellence inresearch and contribution in the field of runtime verification of software systems. Along with the JPL awards, he has received several best paper awards such as: (cid:129) 2020 SIGSOFT Impact Paper Award (cid:129) RV 2018 Test of Time Award (cid:129) ASE 2016 Most Influential Paper Award (cid:129) ASE 2014 Most Influential Paper Award His research activities have generated more than 100 publications with more than 100collaborators.Hisworkhasgeneratedmorethan12,000citations.Hispublications have received several best paper and most influential awards. viii Preface Klaushasprovidedconstantandgenerousservicetotheformalmethodscommunity andtheJetPropulsionLaboratorybyorganizing,participating,andchairingnumerous committees. ThetitleofthisvolumeisFormalMethodsinOuterSpace.ItreflectsKlaus’smain research focus throughout his career: formal methods, often applied at NASA. The contributions,whichwentthroughapeer-reviewprocess,coverawidespectrumofthe topics related to Klaus’s scientific research interests, including programming lan- guages,staticanddynamicanalysis.Thepaperscovertopicsonprogramming,ranging over domain analysis, abstract interpretation, foundations of programming language designandanalysis,characterizationsofthesafety-andlivenessproperties,onruntime verification like hardware-assisted data race detection, confidence monitoring, and automata learning like runtime verification and automata learning and reverse engi- neering through automata learning, as well as runtime verification and control. Dear Klaus, on behalf of all your friends and colleagues, we thank you for every- thing and wish you all the best. August 2021 Ezio Bartocci Yliès Falcone Martin Leucker Organization Program Committee Chairs Bartocci, Ezio TU Wien, Austria Falcone, Yliès Univ. Grenoble Alpes, France Leucker, Martin University of Lübeck, Germany Reviewers Bollig, Benedikt CNRS and ENS Paris-Saclay, France Colombo, Christian University of Malta, Malta Holzmann, Gerard Nimble Research, USA Kallwies, Hannes University of Lübeck, Germany Ničković, Dejan Austrian Institute of Technology, Austria Pace, Gordon University of Malta, Malta Schmitz, Malte University of Lübeck, Germany Sokolsky, Oleg University of Pennsylvania, USA Soueidi, Chukri Inria Grenoble, France Stolz, Volker Høgskulen på Vestlandet, Norway Thoma, Daniel University of Lübeck, Germany Contents Foundations The K Vision for the Future of Programming Language Design and Analysis. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 Xiaohong Chen and Grigore Roşu Refining the Safety-Liveness Classification of Temporal Properties According to Realizability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 Manfred Broy Static Analysis Domain Analysis and Description – Sorts, Types, Intents. . . . . . . . . . . . . . . 35 Dines Bjørner Dynamic interval analysis by abstract interpretation. . . . . . . . . . . . . . . . . . . 61 Patrick Cousot Runtime Verification Runtime Verification: Passing on the Baton . . . . . . . . . . . . . . . . . . . . . . . . 89 Christian Colombo, Gordon J. Pace, and Gerardo Schneider Hardware-Assisted Online Data Race Detection . . . . . . . . . . . . . . . . . . . . . 108 Faustin Ahishakiye, José Ignacio Requeno Jarabo, Violet Ka I Pun, and Volker Stolz Comparing Two Methods for Checking Runtime Properties . . . . . . . . . . . . . 127 Gerard J. Holzmann Dynamic Assurance Confidence Monitoring and Composition for Dynamic Assurance of Learning-Enabled Autonomous Systems: Position Paper. . . . . . . . . . . . . . 137 Ivan Ruchkin, Matthew Cleaveland, Oleg Sokolsky, and Insup Lee Collision-Free 3D Flocking Using the Distributed Simplex Architecture. . . . . 147 Usama Mehmood, Scott D. Stoller, Radu Grosu, and Scott A. Smolka