001484003 000__ 06218cam\\2200709\i\4500 001484003 001__ 1484003 001484003 003__ OCoLC 001484003 005__ 20240117003310.0 001484003 006__ m\\\\\o\\d\\\\\\\\ 001484003 007__ cr\un\nnnunnun 001484003 008__ 231115s2023\\\\si\a\\\\o\\\\\101\0\eng\d 001484003 019__ $$a1409027827 001484003 020__ $$a9789819975846$$q(electronic bk.) 001484003 020__ $$a9819975840$$q(electronic bk.) 001484003 020__ $$z9819975832 001484003 020__ $$z9789819975839 001484003 0247_ $$a10.1007/978-981-99-7584-6$$2doi 001484003 035__ $$aSP(OCoLC)1409202159 001484003 040__ $$aYDX$$beng$$erda$$epn$$cYDX$$dGW5XE$$dEBLCP$$dOCLCQ$$dOCLCO 001484003 049__ $$aISEA 001484003 050_4 $$aQA76.9.F67 001484003 08204 $$a004.01/51$$223/eng/20231117 001484003 1112_ $$aInternational Conference on Formal Engineering Methods$$n(24th :$$d2022 :$$cBrisbane, Qld.). 001484003 24510 $$aFormal methods and software engineering :$$b24th International Conference on Formal Engineering Methods, ICFEM 2022, Brisbane, QLD, Australia, November 21-24, 2023 : proceedings /$$cYi Li, Sofiène Tahar, editors. 001484003 24630 $$aICFEM 2022 001484003 264_1 $$aSingapore :$$bSpringer,$$c[2023] 001484003 264_4 $$c©2023 001484003 300__ $$a1 online resource (xxviii, 300 pages) :$$billustrations (some color). 001484003 336__ $$atext$$btxt$$2rdacontent 001484003 337__ $$acomputer$$bc$$2rdamedia 001484003 338__ $$aonline resource$$bcr$$2rdacarrier 001484003 4901_ $$aLecture notes in computer science ;$$v14308 001484003 500__ $$aInternational conference proceedings. 001484003 500__ $$aIncludes author index. 001484003 5050_ $$aIntro -- Preface -- Organization -- Abstracts of Invited Talks -- Compositional Reasoning at The Software/Hardware Interface -- Separation of Concerns for Complexity Mitigation in System and Domain Formal Modelling - A Dive into Algebraic Event-B Theories -- A Foundation for Interaction -- Practical Verified Concurrent Program Security -- On Analysing Weak Memory Concurrency -- Certified Proof and Non-Provability -- Verifying Compiler Optimisations -- Contents -- Invited Paper -- Verifying Compiler Optimisations -- 1 Introduction -- 2 Data-Flow Sub-graphs -- 3 Term Rewriting Rules 001484003 5058_ $$a4 Verifying Term Rewriting Rules -- 5 Generating Code for Optimisations -- 6 Conclusions -- References -- Regular Papers -- An Idealist's Approach for Smart Contract Correctness -- 1 Introduction -- 2 Overview -- 2.1 Smart Contracts -- 2.2 Vulnerability and Correctness -- 2.3 An Illustrative Example -- 3 Specification Language -- 3.1 High-Level Overview -- 3.2 Formalization -- 4 Verification -- 4.1 Function Validation -- 4.2 Generating Proof Obligations -- 5 Implementation and Evaluation -- 5.1 Implementation -- 5.2 Experimental Evaluation -- 6 Related Work and Conclusion -- References 001484003 5058_ $$aActive Inference of EFSMs Without Reset -- 1 Introduction -- 2 Background and Related Work -- 2.1 Running Example -- 2.2 Related Work -- 2.3 Definitions -- 2.4 Inferring Functions with Genetic Programming -- 3 The ehW-Inference Algorithm -- 3.1 Assumptions -- 3.2 Homing and Characterizing -- 3.3 Inputs and Data Structures -- 3.4 ehW-Inference Backbone -- 3.5 Generalisation -- 3.6 Oracle Procedure -- 4 Inferring a Vending Machine Controller -- 5 Conclusions and Future Work -- References -- Learning Mealy Machines with Local Timers -- 1 Introduction -- 2 Related Work -- 3 Preliminaries 001484003 5058_ $$a3.1 Mealy Machines -- 3.2 The Rivest-Schapire Algorithm -- 4 Mealy Machines with Local Timers -- 4.1 Syntax and Semantics -- 4.2 Expanded Forms and Equivalence -- 5 Learning MMLTs Efficiently -- 5.1 Timer Queries -- 5.2 Timed Counterexample Analysis -- 5.3 Hypothesis Refinement -- 5.4 Hypothesis Completion -- 5.5 Output Query Complexity -- 6 Practical Evaluation -- 7 Conclusion and Future Work -- References -- Compositional Vulnerability Detection with Insecurity Separation Logic -- 1 Introduction -- 2 Motivation -- 3 Attacker Model -- 4 Insecurity Separation Logic (InsecSL) 001484003 5058_ $$a5 Symbolic Execution -- 6 Implementation -- 7 Evaluation -- 8 Related Work and Conclusion -- References -- Dynamic Extrapolation in Extended Timed Automata -- 1 Introduction -- 2 Preliminary -- 2.1 Extended Timed Automata -- 2.2 Symbolic Semantics -- 2.3 M-Extrapolation in XTA -- 3 Dynamic Extrapolation -- 3.1 Reducing Relevant Paths -- 3.2 Dynamic LU-Extrapolation -- 3.3 A Note on Timed Automata Networks -- 4 Experiments and Results -- 5 Conclusion -- References -- Formalizing Robustness Against Character-Level Perturbations for Neural Network Language Models -- 1 Introduction -- 2 Related Work 001484003 506__ $$aAccess limited to authorized users. 001484003 520__ $$aThis book constitutes the proceedings of the 24th International Conference on Formal Methods and Software Engineering, ICFEM 2023, held in Brisbane, QLD, Australia, during November 2124, 2023. The 13 full papers presented together with 8 doctoral symposium papers in this volume were carefully reviewed and selected from 34 submissions, the volume also contains one invited paper. The conference focuses on applying formal methods to practical applications and presents papers for research in all areas related to formal engineering methods. 001484003 588__ $$aOnline resource; title from PDF title page (SpringerLink, viewed November 17, 2023). 001484003 650_6 $$aMéthodes formelles (Informatique)$$vCongrès. 001484003 650_6 $$aGénie logiciel$$vCongrès. 001484003 650_0 $$aFormal methods (Computer science)$$vCongresses.$$vCongresses$$0(DLC)sh2008104061 001484003 650_0 $$aSoftware engineering$$vCongresses.$$vCongresses$$0(DLC)sh2008111658 001484003 655_7 $$aproceedings (reports)$$2aat 001484003 655_7 $$aConference papers and proceedings.$$2lcgft 001484003 655_7 $$aActes de congrès.$$2rvmgf 001484003 655_0 $$aElectronic books. 001484003 7001_ $$aLi, Yi,$$eeditor.$$d1915-$$0(OCoLC)oca00673361 001484003 7001_ $$aTahar, Sofiène,$$d1966-$$eeditor. 001484003 77608 $$iPrint version: $$z9819975832$$z9789819975839$$w(OCoLC)1398463578 001484003 830_0 $$aLecture notes in computer science ;$$v14308. 001484003 852__ $$bebk 001484003 85640 $$3Springer Nature$$uhttps://univsouthin.idm.oclc.org/login?url=https://link.springer.com/10.1007/978-981-99-7584-6$$zOnline Access$$91397441.1 001484003 909CO $$ooai:library.usi.edu:1484003$$pGLOBAL_SET 001484003 980__ $$aBIB 001484003 980__ $$aEBOOK 001484003 982__ $$aEbook 001484003 983__ $$aOnline 001484003 994__ $$a92$$bISE