04526nam a22004815i 4500001001800000003000900018005001700027007001500044008004100059020003700100024003500137050001600172072001600188072002300204072001500227245014500242250001800387264006900405300006500474336002600539337002600565338003600591347002400627490005900651505104200710520152701752650002703279650005703306650004903363650003303412700015203445700015003597710003403747773002603781776003603807776003603843830005903879856004603938912001403984912001503998912001404013999001704027978-3-031-66673-5DE-He21320251030112938.0cr nn 008mamaa240904s2024 sz | s |||| 0|eng d a97830316667359978-3-031-66673-57 a10.1007/978-3-031-66673-52doi 4aQA267-268.5 7aUYA2bicssc 7aCOM0140002bisacsh 7aUYA2thema14aThe Practice of Formal Methodsh[electronic resource] :bEssays in Honour of Cliff Jones, Part II /cedited by Ana Cavalcanti, James Baxter. a1st ed. 2024. 1aCham :bSpringer Nature Switzerland :bImprint: Springer,c2024. aXIV, 316 p. 80 illus., 47 illus. in color.bonline resource. atextbtxt2rdacontent acomputerbc2rdamedia aonline resourcebcr2rdacarrier atext filebPDF2rda1 aLecture Notes in Computer Science,x1611-3349 ;v147810 aReasoning about distributive laws in a concurrent refinement algebra -- HayesOn the Formalization of the Notion of an Algorithm -- A Note on Proofs of Earley’s Recognizer -- On the Relational Basis of Early R/G Work -- Model Refinement: Generating Refinements for Algorithm and SystemDesign -- Analysing the safety implications of security risks in cyber-physical systems -- Rely-Guarantee Interpretation of Sequence Diagrams -- Formal Analysis of Interactions between Safety and Security Requirements -- About Trust and Proof: An experimental framework for heterogeneous verification -- Uncertainty and Probabilistic UTP -- Modelling and Verifying Programs under the Total Store OrderMemory Model in an Algebraic Semantics Style -- Case Study: Modeling, Simulation, Verification, and Code Generationof an Automatic Cruise Control System -- Exploring the Boundaries of Rely/Guarantee and Links to Linearisability -- Less is More Revisited: Association with Global Multiparty Session Types -- Validation of Formal Models: A Case Study. aThis Festschrift, dedicated to Cliff Jones, contains papers written by many of his closest collaborators. Cliff has an exceptional international standing for his groundbreaking research and leadership within the practice of formal methods, his career encompasses significant contributions to academia, industry, policy, and service. Cliff is a Fellow of the Royal Academy of Engineering, ACM, BCS, and IET, and in 2015 he was the inaugural Fellow of the Formal Methods Europe association. His career has included industry research in the UK, Austria and Belgium, a PhD at the University of Oxford, and academic and research roles at the University of Cambridge and the University of Manchester, and since 1999 at Newcastle University. Throughout his career, he has championed the essential role of formalism in design processes. His collaboration at IBM in the 1970s led to the creation of the Vienna Development Method (VDM), a seminal contribution that has influenced both practical industry applications and theoretical advancements. Cliff was the founding editor of the ACM journal Formal Aspects of Computing, a founder of the Formal Methods symposium, and he played a pivotal role in the IFIP Working Groups on Programming Methodology and Verified Software. His policy advocacy has been instrumental in fostering public discourse on the reliability of computing systems. The 30 contributions in this volume are a snapshot of the many current scientific developments inspired by or built upon Cliff’s contributions. 0aMachine theory.967305 0aProgramming languages (Electronic computers).96620614aFormal Languages and Automata Theory.96730624aProgramming Language.9662081 aCavalcanti, Ana.eeditor.0(orcid)0000-0002-0831-19761https://orcid.org/0000-0002-0831-19764edt4http://id.loc.gov/vocabulary/relators/edt9837211 aBaxter, James.eeditor.0(orcid)0000-0001-6083-96071https://orcid.org/0000-0001-6083-96074edt4http://id.loc.gov/vocabulary/relators/edt9837222 aSpringerLink (Online service)0 tSpringer Nature eBook08iPrinted edition:z978303166672808iPrinted edition:z9783031666742 0aLecture Notes in Computer Science,x1611-3349 ;v1478140uhttps://doi.org/10.1007/978-3-031-66673-5 aZDB-2-SCS aZDB-2-SXCS aZDB-2-LNC c63113d63113