| 000 | 04946nam a22005415i 4500 | ||
|---|---|---|---|
| 001 | 978-3-031-67114-2 | ||
| 003 | DE-He213 | ||
| 005 | 20251030112929.0 | ||
| 007 | cr nn 008mamaa | ||
| 008 | 240901s2024 sz | s |||| 0|eng d | ||
| 020 |
_a9783031671142 _9978-3-031-67114-2 |
||
| 024 | 7 |
_a10.1007/978-3-031-67114-2 _2doi |
|
| 050 | 4 | _aQA267-268.5 | |
| 072 | 7 |
_aUYA _2bicssc |
|
| 072 | 7 |
_aCOM014000 _2bisacsh |
|
| 072 | 7 |
_aUYA _2thema |
|
| 245 | 1 | 4 |
_aThe Application of Formal Methods _h[electronic resource] : _bEssays Dedicated to Jim Woodcock on the Occasion of His Retirement / _cedited by Simon Foster, Augusto Sampaio. |
| 250 | _a1st ed. 2024. | ||
| 264 | 1 |
_aCham : _bSpringer Nature Switzerland : _bImprint: Springer, _c2024. |
|
| 300 |
_aXIV, 375 p. 94 illus., 65 illus. in color. _bonline resource. |
||
| 336 |
_atext _btxt _2rdacontent |
||
| 337 |
_acomputer _bc _2rdamedia |
||
| 338 |
_aonline resource _bcr _2rdacarrier |
||
| 347 |
_atext file _bPDF _2rda |
||
| 490 | 1 |
_aLecture Notes in Computer Science, _x1611-3349 ; _v14900 |
|
| 520 | _aThis Festschrift, dedicated to Jim Woodcock, contains papers written by many of his closest collaborators. After a PhD on software verification at the University of Liverpool, Jim has combined a successful career in academia with outstanding industry research, in particular he has been a pioneer in applying mathematical modelling approaches in critical industries. At GEC's Hirst Research Centre he worked on a novel distributed telephone exchange and a service specification of a PABX exchange. In Oxford he collaborated with IBM Hursley Laboratories on modelling of the CICS transaction processing system, one of the most significant software systems ever. As part of the UK government's cybersecurity strategy, he used Z techniques to develop secure office automation systems and a secure version of UNIX. He worked with the Smith Institute and BR Research to verify the safety of railway signalling systems, approaches developed further in safety-critical control systems for the UK Nuclear Installation Inspectorate and British Energy. He provided a technically complete theory of correctness for Z, verifying its soundness from first principles, and completed the verification of Mondex, a smartcard-based electronic cash system, the first application of a general theory of program correctness to an industrial product. He coordinated the experimental work of the Verified Software Initiative, an international grand challenge. More recently he extended the collection of standard Unifying Theories of Programming (UTP) with work on object orientation and hybrid systems. Currently he is working on a UTP theory of probabilistic programs with application to robotics. Jim has been a lecturer, research fellow, reader and professor at the University of Surrey, the University of Oxford, the University of Kent, and since 2004 the University of York, and he is a visiting professor at the Federal University of Pernambuco and Trinity College Dublin. He is a Fellow of the Royal Academy of Engineering, the British Computer Society, and the Formal Methods Europe association, and he was part of the team that won the Queen’s Award for Technological Achievement in 1992. He is the Editor-in-Chief of the ACM journal Formal Aspects of Computing, he has chaired major related academic conferences, and he has contributed to CCITT and Z ISO international standards. Throughout all these activities, Jim has been a guide and inspiration to colleagues and students, and collaborated successfully with researchers in the UK, Brazil, China, France, USA, Ireland, and Singapore. Many of these researchers show in their contributions to this volume the ongoing impact of his work. | ||
| 650 | 0 |
_aMachine theory. _967305 |
|
| 650 | 0 |
_aProgramming languages (Electronic computers). _966206 |
|
| 650 | 0 |
_aSoftware engineering. _933953 |
|
| 650 | 1 | 4 |
_aFormal Languages and Automata Theory. _967306 |
| 650 | 2 | 4 |
_aProgramming Language. _966208 |
| 650 | 2 | 4 |
_aSoftware Engineering. _933953 |
| 700 | 1 |
_aFoster, Simon. _eeditor. _0(orcid)0000-0002-9889-9514 _1https://orcid.org/0000-0002-9889-9514 _4edt _4http://id.loc.gov/vocabulary/relators/edt _983451 |
|
| 700 | 1 |
_aSampaio, Augusto. _eeditor. _0(orcid)0000-0001-6593-577X _1https://orcid.org/0000-0001-6593-577X _4edt _4http://id.loc.gov/vocabulary/relators/edt _983452 |
|
| 710 | 2 | _aSpringerLink (Online service) | |
| 773 | 0 | _tSpringer Nature eBook | |
| 776 | 0 | 8 |
_iPrinted edition: _z9783031671135 |
| 776 | 0 | 8 |
_iPrinted edition: _z9783031671159 |
| 830 | 0 |
_aLecture Notes in Computer Science, _x1611-3349 ; _v14900 |
|
| 856 | 4 | 0 | _uhttps://doi.org/10.1007/978-3-031-67114-2 |
| 912 | _aZDB-2-SCS | ||
| 912 | _aZDB-2-SXCS | ||
| 912 | _aZDB-2-LNC | ||
| 999 |
_c62981 _d62981 |
||