Dependable software engineering : theories, tools, and applications : 8th International Symposium, SETTA 2022, Beijing, China, October 24-28, 2022, proceedings / / edited by Wei Dong, Jean-Pierre Talpin

• Pubblicazione: Cham, Switzerland : , : Springer, , [2022]; ©2022
• Descrizione fisica: 1 online resource (249 pages)
• Disciplina: 910.5
• Soggetto topico: Formal methods (Computer science)
• Persona (resp. second.): DongWei; TalpinJean-Pierre
• Nota di bibliografia: Includes bibliographical references and index.
• Nota di contenuto: Intro -- Preface -- Organization -- Keynotes Speakers -- On SMT Solving for Multi-threaded Program Verification -- Logic-Based Safety of Cyber-Physical Systems: Simultaneous Model Validation and Proof Transfer -- Abstraction-Based Training and Verification of Safe Deep Reinforcement Learning Systems (Extended Abstract) -- Contents -- Verification and Testing for Machine Learning -- HashC: Making DNNs' Coverage Testing Finer and Faster -- 1 Introduction -- 2 Background -- 2.1 Deep Neural Networks -- 2.2 Cryptographic Hash Function -- 2.3 Coverage Criteria -- 3 HashC Coverage Testing Framework -- 4 Evaluation -- 4.1 Experiment Design -- 4.2 Evaluation Results -- 5 Conclusion -- References -- MTUL: Towards Mutation Testing of Unsupervised Learning Systems -- 1 Introduction -- 2 Background -- 2.1 Unsupervised Learning -- 2.2 Mutation Testing -- 3 Mutation Testing Specific to Unsupervised Learning Systems -- 3.1 Mutation Testing Workflow -- 3.2 Mutation Operators -- 3.3 Mutation Scores -- 4 MUAE: The Combination of MTUL and Autoencoder -- 5 Experiment -- 5.1 Datasets -- 5.2 Research Question 1 -- 5.3 Research Question 2 -- 5.4 Research Question 3 -- 6 Related Work -- 7 Conclusion -- References -- COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking -- 1 Introduction -- 2 Core Functionality and Architecture of COOL-MC -- 3 Numerical Experiments -- 4 Conclusion and Future Work -- References -- Dependable Software Development -- VM Migration and Live-Update for Reliable Embedded Hypervisor -- 1 Introduction -- 2 Related Work -- 2.1 Embedded Hypervisor -- 2.2 Virtual Machine Migration -- 2.3 Hypervisor Update -- 3 The Design of Hypervisor -- 3.1 System Structure -- 3.2 Shared Memory -- 3.3 VM Migration -- 3.4 Hypervisor Live-Update -- 4 Evaluation -- 4.1 Environment -- 4.2 Impact on Real-Time Performance -- 4.3 Impact on Networking. ; 4.4 Impact on Memory -- 5 Conclusion -- References -- Mastery: Shifted-Code-Aware Structured Merging -- 1 Introduction -- 2 Preliminary -- 3 Merge Algorithm -- 3.1 Algorithm Overview -- 3.2 Top-Down Pruning Pass -- 3.3 Shifted Code Merging -- 3.4 Unordered Merging -- 3.5 Ordered Merging -- 4 Implementation -- 5 Evaluation -- 5.1 Experimental Setup -- 5.2 Frequency of Shifted Code (RQ1) -- 5.3 Taxonomy of Results -- 5.4 Merge Accuracy (RQ2) -- 5.5 Reported Conflicts (RQ3) -- 5.6 Runtime Performance (RQ4) -- 5.7 Discussions -- 6 Related Work -- 7 Conclusion and Future Directions -- References -- KCL: A Declarative Language for Large-Scale Configuration and Policy Management -- 1 Introduction -- 2 Background and Related Work -- 3 Overview -- 4 Stability -- 5 Engineering -- 5.1 Structure -- 6 Scalability -- 6.1 Configuration Definition -- 6.2 Configuration Substitution -- 6.3 Configuration Merge -- 7 Workflow -- 8 Evaluation -- 8.1 Comparison with Other CLs -- 8.2 Benefits from KCL -- 9 Conclusion and Future Work -- References -- EqFix: Fixing LaTeX Equation Errors by Examples -- 1 Introduction -- 2 EqFix by Examples -- 3 Rules in EqFix -- 3.1 Error Pattern -- 3.2 Equation Pattern -- 3.3 Transformer -- 3.4 Rule Application -- 4 Rule Synthesis -- 4.1 Synthesizing Error Patterns -- 4.2 Synthesizing Transformers -- 4.3 Extension: Pattern Generalization via Lazy Relaxation -- 5 Evaluation -- 5.1 Experimental Setup -- 5.2 Results -- 6 Related Work -- 7 Conclusion and Future Directions -- References -- Dependable CPS and Concurrent Systems -- Translating CPS with Shared-Variable Concurrency in SpaceEx -- 1 Introduction -- 2 Background -- 2.1 SpaceEx -- 2.2 Syntax of Our Modeling Language -- 3 Translation in SpaceEx -- 3.1 Variables -- 3.2 Discrete Behavior -- 3.3 Continous Behavior -- 3.4 Composition -- 4 Conclusion and Future Work -- References. ; A Contract-Based Semantics and Refinement for Simulink -- 1 Introduction -- 2 Related Work -- 3 Syntax of Algebraic Expression of Simulink Diagrams -- 3.1 Signals -- 3.2 Blocks -- 3.3 Algebraic Expressions of Simulink Diagrams -- 4 Contract-Based Semantics of Simulink -- 5 Refinement of Simulink -- 6 Conclusion and Future Work -- References -- Decidability of Liveness for Concurrent Objects on the TSO Memory Model -- 1 Introduction -- 2 Concurrent Systems -- 2.1 Notations -- 2.2 Concurrent Objects and the Most General Client -- 2.3 TSO Operational Semantics -- 3 Liveness -- 4 Perfect/Lossy Channel Machines -- 5 Undecidability of Four Liveness Properties -- 5.1 The Lossy Channel Machine for CPCP of Abdulla et al. ch10DBLP:journalsspsiandcspsAbdullaJ96a -- 5.2 Libraries for Four Liveness Properties -- 5.3 Undecidability of Four Liveness Properties -- 6 Checking Obstruction-Freedom -- 6.1 The Basic TSO Concurrent Systems -- 6.2 Verification of Obstruction-Freedom -- 7 Conclusion -- References -- Theorem Proving and SAT -- Integration of Multiple Formal Matrix Models in Coq -- 1 Introduction -- 2 Different Formal Matrix Models -- 2.1 DepList: Dependent List -- 2.2 DepPair: Dependent Pair -- 2.3 DepRec: Dependent Record -- 2.4 NatFun: Function with Natural Indexing -- 2.5 FinFun: Function with Finite Indexing -- 3 Integrated Matrix Library -- 3.1 Mathematical Properties -- 3.2 Polymorphism and Hierarchy of Matrix Elements -- 3.3 Matrix Interface -- 3.4 Matrix Implementation -- 3.5 Conversion Between Matrix Models -- 3.6 Isomorphism of Matrix Models -- 4 Comparison of Different Matrix Models -- 5 Example of Using the Matrix Library -- 6 Conclusion -- References -- On-The-Fly Bisimilarity Checking for Fresh-Register Automata -- 1 Introduction -- 2 Background -- 3 Symbolic Reasoning -- 4 On-The-Fly Algorithms for Bisimilarity -- 4.1 Base On-the-fly Algorithm. ; 4.2 Generator On-the-fly Algorithm -- 5 Results -- 5.1 Benchmarks for On-the-fly Algorithms, and Existing Approaches -- 5.2 -calculus Results -- 6 Conclusions -- References -- LOGIC: A Coq Library for Logics -- 1 Introduction -- 2 Background: Coq Proof Assistant -- 3 Overview -- 4 Parameterized Definitions and Proofs -- 4.1 Connectives and Judgements -- 4.2 Proof Rules -- 4.3 Semantics and Soundness -- 4.4 Completeness -- 5 Logic Generator -- 5.1 Features of Logic Generator -- 5.2 Design of Logic Generator -- 6 Related Work -- 7 Conclusion -- A Sample Use Cases of Logic Generator -- A.1 Demo1: Intuitionistic Propositional Logic -- A.2 Demo2: A Very Small Logic -- A.3 Demo3: Intuitionistic Propositional Logic -- A.4 Demo4: Separation Logic, Without Separation Conjunction -- A.5 Demo5: Separation Logic, with Separating Conjunction -- A.6 Demo6: Separation Logic, Without Separating Implication -- A.7 Demo7: Separation Logic, Constructed from Model Level -- A.8 Mendelson's Propositional Logic -- A.9 Minimum Separation Logic -- A.10 Demo for Bedrock2's Separation Logic -- References -- Diversifying a Parallel SAT Solver with Bayesian Moment Matching -- 1 Introduction -- 2 Algorithm Description -- 3 Evaluation of slime and bmm Sequential Solvers -- 3.1 Architecture of the p-slime-bmmParallel Portfolio Solver and Results -- 4 Conclusion -- References -- Author Index.
• Titolo autorizzato: Dependable Software Engineering. Theories, Tools, and Applications
• ISBN: 3-031-21213-4
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Lingua di pubblicazione: Inglese
• Record Nr.: 996503470003316
• Lo trovi qui: Univ. di Salerno
• Serie: Lecture Notes in Computer Science