Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
Automated Technology for Verification and Analysis [[electronic resource] ] : 21st International Symposium, ATVA 2023, Singapore, October 24–27, 2023, Proceedings, Part I / / edited by Étienne André, Jun Sun
| Automated Technology for Verification and Analysis [[electronic resource] ] : 21st International Symposium, ATVA 2023, Singapore, October 24–27, 2023, Proceedings, Part I / / edited by Étienne André, Jun Sun |
| Edizione | [1st ed. 2023.] |
| Pubbl/distr/stampa | Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2023 |
| Descrizione fisica | 1 online resource (453 pages) |
| Disciplina | 004.015113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Computer engineering Computer networks Artificial intelligence Computers Computer science Software Engineering Computer Engineering and Networks Artificial Intelligence Computer Hardware Theory of Computation |
| ISBN | 3-031-45329-8 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Temporal logics -- Data structures and heuristics -- Verification of programs and hardware -- Tool papers. |
| Record Nr. | UNISA-996558466403316 |
| Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2023 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated Technology for Verification and Analysis : 21st International Symposium, ATVA 2023, Singapore, October 24–27, 2023, Proceedings, Part I / / edited by Étienne André, Jun Sun
| Automated Technology for Verification and Analysis : 21st International Symposium, ATVA 2023, Singapore, October 24–27, 2023, Proceedings, Part I / / edited by Étienne André, Jun Sun |
| Edizione | [1st ed. 2023.] |
| Pubbl/distr/stampa | Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2023 |
| Descrizione fisica | 1 online resource (453 pages) |
| Disciplina | 004.015113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Computer engineering Computer networks Artificial intelligence Computers Computer science Software Engineering Computer Engineering and Networks Artificial Intelligence Computer Hardware Theory of Computation |
| ISBN | 3-031-45329-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Temporal logics -- Data structures and heuristics -- Verification of programs and hardware -- Tool papers. |
| Record Nr. | UNINA-9910754096303321 |
| Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2023 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Bioinformatic and Statistical Analysis of Microbiome Data [[electronic resource] ] : From Raw Sequences to Advanced Modeling with QIIME 2 and R / / by Yinglin Xia, Jun Sun
| Bioinformatic and Statistical Analysis of Microbiome Data [[electronic resource] ] : From Raw Sequences to Advanced Modeling with QIIME 2 and R / / by Yinglin Xia, Jun Sun |
| Autore | Xia Yinglin |
| Edizione | [1st ed. 2023.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2023 |
| Descrizione fisica | 1 online resource (716 pages) |
| Disciplina | 576 |
| Soggetto topico |
Bioinformatics
Biometry Big data Mathematical statistics - Data processing Biotechnology Biomedical engineering Biostatistics Big Data Statistics and Computing Biomedical Engineering and Bioengineering |
| Soggetto non controllato |
Microbiology
Science |
| ISBN |
9783031213915
9783031213908 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Chapter 1. Introduction to Linux and Unix -- Chapter 2. Introduction to R, Rstudio -- Chapter 3. Bioinformatic Analysis of Next-Generation Sequencing -- Chapter 4. Bioinformatic Analysis of Metagenomics -- Chapter 5. Alpha Diversity -- Chapter 6. Beta Diversity -- Chapter 7. Differential Abundance Analysis -- Chapter 8. Analyzing Zero-Inflated Microbiome Data -- Chapter 9. Compositional Analysis of Microbiome Data -- Chapter 10. Longitudinal Data Analysis of Microbiome -- Chapter 11. Meta-analysis of Microbiome Data (optional). |
| Record Nr. | UNISA-996547956503316 |
Xia Yinglin
|
||
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2023 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Bioinformatic and Statistical Analysis of Microbiome Data : From Raw Sequences to Advanced Modeling with QIIME 2 and R / / by Yinglin Xia, Jun Sun
| Bioinformatic and Statistical Analysis of Microbiome Data : From Raw Sequences to Advanced Modeling with QIIME 2 and R / / by Yinglin Xia, Jun Sun |
| Autore | Xia Yinglin |
| Edizione | [1st ed. 2023.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2023 |
| Descrizione fisica | 1 online resource (716 pages) |
| Disciplina |
576
579.17 |
| Soggetto topico |
Bioinformatics
Biometry Big data Mathematical statistics - Data processing Biotechnology Biomedical engineering Biostatistics Big Data Statistics and Computing Biomedical Engineering and Bioengineering |
| Soggetto non controllato |
Microbiology
Science |
| ISBN |
9783031213915
9783031213908 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Chapter 1. Introduction to Linux and Unix -- Chapter 2. Introduction to R, Rstudio -- Chapter 3. Bioinformatic Analysis of Next-Generation Sequencing -- Chapter 4. Bioinformatic Analysis of Metagenomics -- Chapter 5. Alpha Diversity -- Chapter 6. Beta Diversity -- Chapter 7. Differential Abundance Analysis -- Chapter 8. Analyzing Zero-Inflated Microbiome Data -- Chapter 9. Compositional Analysis of Microbiome Data -- Chapter 10. Longitudinal Data Analysis of Microbiome -- Chapter 11. Meta-analysis of Microbiome Data (optional). |
| Record Nr. | UNINA-9910725100103321 |
|
Xia Yinglin
|
||
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2023 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Dependable Software Engineering. Theories, Tools, and Applications : 9th International Symposium, SETTA 2023, Nanjing, China, November 27-29, 2023, Proceedings
| Dependable Software Engineering. Theories, Tools, and Applications : 9th International Symposium, SETTA 2023, Nanjing, China, November 27-29, 2023, Proceedings |
| Autore | Hermanns Holger |
| Edizione | [1st ed.] |
| Pubbl/distr/stampa | Singapore : , : Springer, , 2024 |
| Descrizione fisica | 1 online resource (448 pages) |
| Altri autori (Persone) |
SunJun
BuLei |
| Collana | Lecture Notes in Computer Science Series |
| ISBN | 981-9986-64-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Contents -- String Constraints with Regex-Counting and String-Length Solved More Efficiently -- 1 Introduction -- 2 Overview -- 3 Preliminaries -- 4 String Constraints with Regex-Counting and String-Length -- 5 Cost-Enriched Finite Automata -- 6 Solving RECL Constraints -- 6.1 From SATRECL to NELIA(CEFA) -- 6.2 Solving NELIA(CEFA) -- 7 Experiments -- 7.1 Benchmark Suites and Experiment Setup -- 7.2 Performance Evaluation -- 7.3 Evaluation on Problem Instances with Large Bounds -- 7.4 Empirical Justification of the Technical Choices Made in the Decision Procedure -- 8 Conclusion -- References -- Reachability Based Uniform Controllability to Target Set with Evolution Function -- 1 Introduction -- 2 Problem Formulation -- 3 Reachability Based Theoretical Foundation -- 3.1 Approximation of Reachable Set -- 3.2 Hausdorff Semi-distance Based Control Synthesis -- 3.3 Reachability Verification -- 4 Reachability Based Heuristic Framework -- 5 Improvements of Reachability Based Framework -- 5.1 K-Arm Bandit Model Based Improvement -- 5.2 Reference Trajectory Based Further Improvement -- 6 Examples and Discussions -- 7 Conclusion -- References -- Enhancing Branch and Bound for Robustness Verification of Neural Networks via an Effective Branching Strategy -- 1 Introduction -- 2 Preliminaries -- 2.1 Neural Network Verification -- 2.2 Branch and Bound -- 3 Enhancing BaB with a Better Branching Strategy -- 3.1 Improvement to Lower Bound by Splitting -- 3.2 Better Splitting Decision -- 4 Experimental Evaluation -- 4.1 Benchmarks -- 4.2 Experiment Results -- 5 Conclusion -- References -- Graph-Based Log Anomaly Detection via Adversarial Training -- 1 Introduction -- 2 Related Work -- 2.1 Log-Based Anomaly Detection -- 2.2 Generative Adversarial Network for Anomaly Detection -- 3 Framework -- 3.1 Problem Statement.
3.2 Log Preprocessing -- 3.3 Graph Construction -- 3.4 Graph Representation Learning -- 3.5 Adversarial Training Model -- 3.6 Anomaly Detection -- 4 Experiments and Results -- 4.1 Datasets and Evaluation Metrics -- 4.2 Baselines and Implementation Details -- 4.3 RQ1: Comparison with Baseline Models -- 4.4 RQ2: Robustness w.r.t. Data Contamination -- 4.5 RQ3: Ablation Study -- 5 Conclusion -- References -- Formal Verification Based Synthesis for Behavior Trees -- 1 Introduction -- 2 Background -- 2.1 Behavior Trees -- 2.2 Linear Temporal Logic -- 2.3 Communicating Sequential Processes -- 3 Problem Formulation -- 4 Proposed Approach -- 4.1 CSP Modelling and Verification -- 4.2 Grammar-Based MCTS -- 5 Demonstration -- 5.1 Experimental Setup -- 5.2 Comparison Experiment -- 5.3 Ablation Experiment -- 5.4 Discussion -- 6 Related Work -- 7 Conclusion -- References -- SeHBPL: Behavioral Semantics-Based Patch Presence Test for Binaries -- 1 Introduction -- 2 Overview -- 2.1 Challenges -- 2.2 Behavioral Semantics -- 2.3 Insights -- 2.4 Running Example -- 3 Approach Design -- 3.1 Source Code Parsing -- 3.2 Behavioral Semantics Extracting -- 3.3 Behavioral Semantics Matching -- 4 Evaluation -- 4.1 Testing Data Setup -- 4.2 Evaluation Setup -- 4.3 Evaluation on Effectiveness -- 4.4 Evaluation of Efficiency -- 4.5 Performance of Behavioral Semantics -- 5 Discussion -- 6 Related Work -- 7 Conclusion -- References -- Session Types with Multiple Senders Single Receiver -- 1 Introduction -- 1.1 Related Work -- 2 A Motivating Example -- 3 MSSR Session Types -- 3.1 Session -Calculus -- 3.2 Global and Local Session Types -- 3.3 Projection and Well-Formed Global Types -- 3.4 Consistency of Global Types and Local Types -- 4 Type System -- 5 A Communication Type System for Progress -- 5.1 Typing Rules -- 6 Modelling Rust Multi-threads in MSSR Session Types. 7 Conclusion and Future Work -- References -- Understanding the Reproducibility Issues of Monkey for GUI Testing -- 1 Introduction -- 2 Empirical Study Methodology -- 2.1 Notations and Definitions -- 2.2 Experimental Method -- 2.3 Experimental Setup -- 3 Experimental Results Analysis -- 3.1 RQ1: REPRODUCIBILITY RATE -- 3.2 RQ2: ROOT CAUSE -- 4 Discussions and Implications -- 4.1 How Does Throttle Affect Monkey's Reproducibility Rate? -- 4.2 Can R& -- R Tools Improve Monkey's Reproducibility Rate? -- 4.3 Threats to Validity -- 5 Related Work -- 6 Conclusion and Future Work -- References -- Multi-dimensional Abstraction and Decomposition for Separation of Concerns -- 1 Introduction -- 2 Linking Formal Methods -- 2.1 Formal Theories of Different Aspects -- 2.2 UTP for Linking Formal Theories -- 3 rCOS Theory for Component-Based Architecture -- 3.1 rCOS Theory of Semantics and Refinement of OO Programming -- 3.2 Model of Interface Contracts of Components -- 4 rCOS Support to Separation of Concerns in MDE -- 4.1 Use Case Driven Requirements Model Building -- 4.2 Component Development Process -- 4.3 System Development -- 5 Conclusions -- References -- Solving SMT over Non-linear Real Arithmetic via Numerical Sampling and Symbolic Verification -- 1 Introduction -- 2 Preliminaries -- 2.1 Real Arithmetic Formula -- 2.2 Zero-Dimensional Systems and Real Zeros -- 3 Numeric Sampling via Random Global Optimization -- 4 The Main Algorithm -- 4.1 Using Numeric Samples to Simplify the Formula -- 4.2 DPLL-Based Splitting Procedure -- 4.3 Model Generation and Verification -- 4.4 Reducing the Equation Set to Zero-Dimensional System -- 4.5 Determine Satisfiability of Inequality -- 5 Experiment -- 5.1 Experiment Preparation -- 5.2 Instances -- 5.3 Comparison to Symbolic Computation Tools -- 5.4 Comparison to State-of-the-Art SMT Solvers -- 6 Conclusion and Future Work. References -- Leveraging TLA+ Specifications to Improve the Reliability of the ZooKeeperCoordination Service -- 1 Introduction -- 2 ZooKeeper and TLA+ -- 2.1 ZooKeeper and Zab -- 2.2 TLA+ Basics -- 3 Protocol Specification -- 3.1 Development of Protocol Specification -- 3.2 Ensuring Quality of Protocol Specification -- 4 System Specification -- 4.1 Essentials of a Super-Doc in TLA+ -- 4.2 Development of the Super-Doc -- 4.3 Ensuring Quality of the Super-Doc -- 5 Test Specification -- 5.1 Obtaining the Test Specification -- 5.2 Improving the Accuracy of Specification -- 5.3 Test Specification in Action -- 6 Related Work -- 7 Conclusion and Future Work -- References -- Modeling Regex Operators for Solving Regex Crossword Puzzles -- 1 Introduction -- 2 Preliminaries -- 3 Modeling Regex Operators -- 3.1 The Function (r,p,l) -- 3.2 Refinement -- 4 Solving Regex Crossword Puzzles -- 4.1 The Definitions -- 4.2 Rcps: Regex Crossword Puzzle Solver -- 5 Experiments -- 5.1 Experiment Setup -- 5.2 Effectiveness and Efficiency of Rcps -- 6 Related Work -- 7 Conclusion -- References -- Software Vulnerability Detection Using an Enhanced Generalization Strategy -- 1 Introduction -- 2 Related Works -- 2.1 In-Domain Vulnerability Detection Methods -- 2.2 Cross-Domain Vulnerability Detection Methods -- 3 Approach -- 3.1 Data Preparation -- 3.2 Meta Learning Model -- 3.3 Detection Model -- 4 Evaluation -- 4.1 Experimental Setup -- 4.2 Experiment Results -- 5 Conclusion -- References -- HeatC: A Variable-Grained Coverage Criterion for Deep Learning Systems -- 1 Introduction -- 2 Class Activation Mapping -- 3 HeatC Coverage Criterion -- 3.1 Generation of Heat Feature Buckets -- 3.2 Test Adequacy Evaluation and Test Sample Selection -- 4 Evaluation -- 4.1 Experiment Design -- 4.2 Experiment Results -- 5 Conclusion -- References. Formalization of Lambda Calculus with Explicit Names as a Nominal Reasoning Framework -- 1 Introduction -- 1.1 Related Work -- 1.2 Our Contributions -- 2 Syntax and Alpha-Equivalence -- 2.1 Names -- 2.2 The Syntax of Lambda Calculus -- 2.3 Alpha Equivalence -- 2.4 Substitution -- 2.5 An Alpha-Structural Induction Principle -- 3 The Church-Rosser Theorem -- 3.1 Rule Induction Principles -- 3.2 Proof of Church-Rosser -- 4 Application: First-Order Logic Extended with Dynamically-Defined Predicates -- 5 Conclusions -- References -- Vulnerability Report Analysis and Vulnerability Reproduction for Web Applications -- 1 Introduction -- 2 Basic Concepts and Related Techniques -- 2.1 Vulnerability Report -- 2.2 Natural Language Processing -- 2.3 Test Scripts and Testing Framework of Web Applications -- 3 Vulnerability Report Analysis and Vulnerability Reproduction Approach for Web Applications -- 3.1 Overview -- 3.2 Syntactic Dependency Patterns Summarising from Vulnerability Reports -- 3.3 Automated Parsing of Vulnerability Reports -- 3.4 Automatic Vulnerability Reproduction Based on Semantic Similarity Between CIS and Event of Web Application -- 4 Experiment -- 4.1 Experimental Subjects and Environment -- 4.2 Analysis of Experimental Results -- 5 Conclusion -- References -- Run-Time Assured Reinforcement Learning for Safe Spacecraft Rendezvous with Obstacle Avoidance -- 1 Introduction and Related Work -- 2 Background -- 2.1 Reinforcement Learning -- 2.2 Run-Time Assurance -- 3 Safe Spacecraft Rendezvous -- 3.1 Relative Motion Dynamics -- 3.2 Safety Constraints -- 3.3 Run-Time Assured RL Algorithm -- 4 Experiments -- 4.1 Spacecraft Rendezvous Environment -- 4.2 Reward Shaping -- 4.3 Hyperparameters -- 5 Results -- 5.1 Training Performance Analysis -- 5.2 Simulation and Expanded Test -- 6 Conclusions -- References. An Abstract Domain of Linear Templates with Disjunctive Right-Hand-Side Intervals. |
| Record Nr. | UNINA-9910770247103321 |
|
Hermanns Holger
|
||
| Singapore : , : Springer, , 2024 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Dependable Software Engineering. Theories, Tools, and Applications : 9th International Symposium, SETTA 2023, Nanjing, China, November 27-29, 2023, Proceedings
| Dependable Software Engineering. Theories, Tools, and Applications : 9th International Symposium, SETTA 2023, Nanjing, China, November 27-29, 2023, Proceedings |
| Autore | Hermanns Holger |
| Edizione | [1st ed.] |
| Pubbl/distr/stampa | Singapore : , : Springer, , 2024 |
| Descrizione fisica | 1 online resource (448 pages) |
| Altri autori (Persone) |
SunJun
BuLei |
| Collana | Lecture Notes in Computer Science Series |
| ISBN | 981-9986-64-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Contents -- String Constraints with Regex-Counting and String-Length Solved More Efficiently -- 1 Introduction -- 2 Overview -- 3 Preliminaries -- 4 String Constraints with Regex-Counting and String-Length -- 5 Cost-Enriched Finite Automata -- 6 Solving RECL Constraints -- 6.1 From SATRECL to NELIA(CEFA) -- 6.2 Solving NELIA(CEFA) -- 7 Experiments -- 7.1 Benchmark Suites and Experiment Setup -- 7.2 Performance Evaluation -- 7.3 Evaluation on Problem Instances with Large Bounds -- 7.4 Empirical Justification of the Technical Choices Made in the Decision Procedure -- 8 Conclusion -- References -- Reachability Based Uniform Controllability to Target Set with Evolution Function -- 1 Introduction -- 2 Problem Formulation -- 3 Reachability Based Theoretical Foundation -- 3.1 Approximation of Reachable Set -- 3.2 Hausdorff Semi-distance Based Control Synthesis -- 3.3 Reachability Verification -- 4 Reachability Based Heuristic Framework -- 5 Improvements of Reachability Based Framework -- 5.1 K-Arm Bandit Model Based Improvement -- 5.2 Reference Trajectory Based Further Improvement -- 6 Examples and Discussions -- 7 Conclusion -- References -- Enhancing Branch and Bound for Robustness Verification of Neural Networks via an Effective Branching Strategy -- 1 Introduction -- 2 Preliminaries -- 2.1 Neural Network Verification -- 2.2 Branch and Bound -- 3 Enhancing BaB with a Better Branching Strategy -- 3.1 Improvement to Lower Bound by Splitting -- 3.2 Better Splitting Decision -- 4 Experimental Evaluation -- 4.1 Benchmarks -- 4.2 Experiment Results -- 5 Conclusion -- References -- Graph-Based Log Anomaly Detection via Adversarial Training -- 1 Introduction -- 2 Related Work -- 2.1 Log-Based Anomaly Detection -- 2.2 Generative Adversarial Network for Anomaly Detection -- 3 Framework -- 3.1 Problem Statement.
3.2 Log Preprocessing -- 3.3 Graph Construction -- 3.4 Graph Representation Learning -- 3.5 Adversarial Training Model -- 3.6 Anomaly Detection -- 4 Experiments and Results -- 4.1 Datasets and Evaluation Metrics -- 4.2 Baselines and Implementation Details -- 4.3 RQ1: Comparison with Baseline Models -- 4.4 RQ2: Robustness w.r.t. Data Contamination -- 4.5 RQ3: Ablation Study -- 5 Conclusion -- References -- Formal Verification Based Synthesis for Behavior Trees -- 1 Introduction -- 2 Background -- 2.1 Behavior Trees -- 2.2 Linear Temporal Logic -- 2.3 Communicating Sequential Processes -- 3 Problem Formulation -- 4 Proposed Approach -- 4.1 CSP Modelling and Verification -- 4.2 Grammar-Based MCTS -- 5 Demonstration -- 5.1 Experimental Setup -- 5.2 Comparison Experiment -- 5.3 Ablation Experiment -- 5.4 Discussion -- 6 Related Work -- 7 Conclusion -- References -- SeHBPL: Behavioral Semantics-Based Patch Presence Test for Binaries -- 1 Introduction -- 2 Overview -- 2.1 Challenges -- 2.2 Behavioral Semantics -- 2.3 Insights -- 2.4 Running Example -- 3 Approach Design -- 3.1 Source Code Parsing -- 3.2 Behavioral Semantics Extracting -- 3.3 Behavioral Semantics Matching -- 4 Evaluation -- 4.1 Testing Data Setup -- 4.2 Evaluation Setup -- 4.3 Evaluation on Effectiveness -- 4.4 Evaluation of Efficiency -- 4.5 Performance of Behavioral Semantics -- 5 Discussion -- 6 Related Work -- 7 Conclusion -- References -- Session Types with Multiple Senders Single Receiver -- 1 Introduction -- 1.1 Related Work -- 2 A Motivating Example -- 3 MSSR Session Types -- 3.1 Session -Calculus -- 3.2 Global and Local Session Types -- 3.3 Projection and Well-Formed Global Types -- 3.4 Consistency of Global Types and Local Types -- 4 Type System -- 5 A Communication Type System for Progress -- 5.1 Typing Rules -- 6 Modelling Rust Multi-threads in MSSR Session Types. 7 Conclusion and Future Work -- References -- Understanding the Reproducibility Issues of Monkey for GUI Testing -- 1 Introduction -- 2 Empirical Study Methodology -- 2.1 Notations and Definitions -- 2.2 Experimental Method -- 2.3 Experimental Setup -- 3 Experimental Results Analysis -- 3.1 RQ1: REPRODUCIBILITY RATE -- 3.2 RQ2: ROOT CAUSE -- 4 Discussions and Implications -- 4.1 How Does Throttle Affect Monkey's Reproducibility Rate? -- 4.2 Can R& -- R Tools Improve Monkey's Reproducibility Rate? -- 4.3 Threats to Validity -- 5 Related Work -- 6 Conclusion and Future Work -- References -- Multi-dimensional Abstraction and Decomposition for Separation of Concerns -- 1 Introduction -- 2 Linking Formal Methods -- 2.1 Formal Theories of Different Aspects -- 2.2 UTP for Linking Formal Theories -- 3 rCOS Theory for Component-Based Architecture -- 3.1 rCOS Theory of Semantics and Refinement of OO Programming -- 3.2 Model of Interface Contracts of Components -- 4 rCOS Support to Separation of Concerns in MDE -- 4.1 Use Case Driven Requirements Model Building -- 4.2 Component Development Process -- 4.3 System Development -- 5 Conclusions -- References -- Solving SMT over Non-linear Real Arithmetic via Numerical Sampling and Symbolic Verification -- 1 Introduction -- 2 Preliminaries -- 2.1 Real Arithmetic Formula -- 2.2 Zero-Dimensional Systems and Real Zeros -- 3 Numeric Sampling via Random Global Optimization -- 4 The Main Algorithm -- 4.1 Using Numeric Samples to Simplify the Formula -- 4.2 DPLL-Based Splitting Procedure -- 4.3 Model Generation and Verification -- 4.4 Reducing the Equation Set to Zero-Dimensional System -- 4.5 Determine Satisfiability of Inequality -- 5 Experiment -- 5.1 Experiment Preparation -- 5.2 Instances -- 5.3 Comparison to Symbolic Computation Tools -- 5.4 Comparison to State-of-the-Art SMT Solvers -- 6 Conclusion and Future Work. References -- Leveraging TLA+ Specifications to Improve the Reliability of the ZooKeeperCoordination Service -- 1 Introduction -- 2 ZooKeeper and TLA+ -- 2.1 ZooKeeper and Zab -- 2.2 TLA+ Basics -- 3 Protocol Specification -- 3.1 Development of Protocol Specification -- 3.2 Ensuring Quality of Protocol Specification -- 4 System Specification -- 4.1 Essentials of a Super-Doc in TLA+ -- 4.2 Development of the Super-Doc -- 4.3 Ensuring Quality of the Super-Doc -- 5 Test Specification -- 5.1 Obtaining the Test Specification -- 5.2 Improving the Accuracy of Specification -- 5.3 Test Specification in Action -- 6 Related Work -- 7 Conclusion and Future Work -- References -- Modeling Regex Operators for Solving Regex Crossword Puzzles -- 1 Introduction -- 2 Preliminaries -- 3 Modeling Regex Operators -- 3.1 The Function (r,p,l) -- 3.2 Refinement -- 4 Solving Regex Crossword Puzzles -- 4.1 The Definitions -- 4.2 Rcps: Regex Crossword Puzzle Solver -- 5 Experiments -- 5.1 Experiment Setup -- 5.2 Effectiveness and Efficiency of Rcps -- 6 Related Work -- 7 Conclusion -- References -- Software Vulnerability Detection Using an Enhanced Generalization Strategy -- 1 Introduction -- 2 Related Works -- 2.1 In-Domain Vulnerability Detection Methods -- 2.2 Cross-Domain Vulnerability Detection Methods -- 3 Approach -- 3.1 Data Preparation -- 3.2 Meta Learning Model -- 3.3 Detection Model -- 4 Evaluation -- 4.1 Experimental Setup -- 4.2 Experiment Results -- 5 Conclusion -- References -- HeatC: A Variable-Grained Coverage Criterion for Deep Learning Systems -- 1 Introduction -- 2 Class Activation Mapping -- 3 HeatC Coverage Criterion -- 3.1 Generation of Heat Feature Buckets -- 3.2 Test Adequacy Evaluation and Test Sample Selection -- 4 Evaluation -- 4.1 Experiment Design -- 4.2 Experiment Results -- 5 Conclusion -- References. Formalization of Lambda Calculus with Explicit Names as a Nominal Reasoning Framework -- 1 Introduction -- 1.1 Related Work -- 1.2 Our Contributions -- 2 Syntax and Alpha-Equivalence -- 2.1 Names -- 2.2 The Syntax of Lambda Calculus -- 2.3 Alpha Equivalence -- 2.4 Substitution -- 2.5 An Alpha-Structural Induction Principle -- 3 The Church-Rosser Theorem -- 3.1 Rule Induction Principles -- 3.2 Proof of Church-Rosser -- 4 Application: First-Order Logic Extended with Dynamically-Defined Predicates -- 5 Conclusions -- References -- Vulnerability Report Analysis and Vulnerability Reproduction for Web Applications -- 1 Introduction -- 2 Basic Concepts and Related Techniques -- 2.1 Vulnerability Report -- 2.2 Natural Language Processing -- 2.3 Test Scripts and Testing Framework of Web Applications -- 3 Vulnerability Report Analysis and Vulnerability Reproduction Approach for Web Applications -- 3.1 Overview -- 3.2 Syntactic Dependency Patterns Summarising from Vulnerability Reports -- 3.3 Automated Parsing of Vulnerability Reports -- 3.4 Automatic Vulnerability Reproduction Based on Semantic Similarity Between CIS and Event of Web Application -- 4 Experiment -- 4.1 Experimental Subjects and Environment -- 4.2 Analysis of Experimental Results -- 5 Conclusion -- References -- Run-Time Assured Reinforcement Learning for Safe Spacecraft Rendezvous with Obstacle Avoidance -- 1 Introduction and Related Work -- 2 Background -- 2.1 Reinforcement Learning -- 2.2 Run-Time Assurance -- 3 Safe Spacecraft Rendezvous -- 3.1 Relative Motion Dynamics -- 3.2 Safety Constraints -- 3.3 Run-Time Assured RL Algorithm -- 4 Experiments -- 4.1 Spacecraft Rendezvous Environment -- 4.2 Reward Shaping -- 4.3 Hyperparameters -- 5 Results -- 5.1 Training Performance Analysis -- 5.2 Simulation and Expanded Test -- 6 Conclusions -- References. An Abstract Domain of Linear Templates with Disjunctive Right-Hand-Side Intervals. |
| Record Nr. | UNISA-996587866703316 |
|
Hermanns Holger
|
||
| Singapore : , : Springer, , 2024 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Dependable Software Engineering. Theories, Tools, and Applications [[electronic resource] ] : 5th International Symposium, SETTA 2019, Shanghai, China, November 27–29, 2019, Proceedings / / edited by Nan Guan, Joost-Pieter Katoen, Jun Sun
| Dependable Software Engineering. Theories, Tools, and Applications [[electronic resource] ] : 5th International Symposium, SETTA 2019, Shanghai, China, November 27–29, 2019, Proceedings / / edited by Nan Guan, Joost-Pieter Katoen, Jun Sun |
| Edizione | [1st ed. 2019.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
| Descrizione fisica | 1 online resource (XIII, 139 p. 135 illus., 23 illus. in color.) |
| Disciplina | 005.1 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Computer organization Microprogramming Computer simulation Computer logic Mathematical logic Software Engineering Computer Systems Organization and Communication Networks Control Structures and Microprogramming Simulation and Modeling Logics and Meanings of Programs Mathematical Logic and Formal Languages |
| ISBN | 3-030-35540-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISA-996466424603316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Dependable Software Engineering. Theories, Tools, and Applications : 5th International Symposium, SETTA 2019, Shanghai, China, November 27–29, 2019, Proceedings / / edited by Nan Guan, Joost-Pieter Katoen, Jun Sun
| Dependable Software Engineering. Theories, Tools, and Applications : 5th International Symposium, SETTA 2019, Shanghai, China, November 27–29, 2019, Proceedings / / edited by Nan Guan, Joost-Pieter Katoen, Jun Sun |
| Edizione | [1st ed. 2019.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
| Descrizione fisica | 1 online resource (XIII, 139 p. 135 illus., 23 illus. in color.) |
| Disciplina | 005.1 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Computer engineering Computer networks Microprogramming Computer simulation Computer science Machine theory Software Engineering Computer Engineering and Networks Control Structures and Microprogramming Computer Modelling Computer Science Logic and Foundations of Programming Formal Languages and Automata Theory |
| ISBN | 3-030-35540-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910357848903321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
FM 2014: Formal Methods [[electronic resource] ] : 19th International Symposium, Singapore, May 12-16, 2014. Proceedings / / edited by Cliff Jones, Pekka Pihlajasaari, Jun Sun
| FM 2014: Formal Methods [[electronic resource] ] : 19th International Symposium, Singapore, May 12-16, 2014. Proceedings / / edited by Cliff Jones, Pekka Pihlajasaari, Jun Sun |
| Edizione | [1st ed. 2014.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 |
| Descrizione fisica | 1 online resource (XVIII, 750 p. 185 illus.) |
| Disciplina | 005.1 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Mathematical logic Computer logic Management information systems Computer science Computers Software Engineering Mathematical Logic and Formal Languages Logics and Meanings of Programs Management of Computing and Information Systems Computation by Abstract Devices |
| ISBN | 3-319-06410-X |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Validity Checking of Put back Transformations in Bidirectional Programming -- Proof Engineering Considered Essential -- Engineering UToPiA: Formal Semantics for CML -- 40 Years of Formal Methods: Some Obstacles and Some Possibilities? -- A Refinement Based Strategy for Local Deadlock Analysis of Networks of CSP Processes -- Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools -- Definition, Semantics and Analysis of Multi rate Synchronous AADL -- Trust Found: Towards a Formal Foundation for Model Checking Trusted Computing Platforms -- The VerCors Tool for Verification of Concurrent Programs -- Knowledge-Based Automated Repair of Authentication Protocols -- A Simplified Z Semantics for Presentation Interaction Models -- Log Analysis for Data Protection Accountability -- Automatic Compositional Synthesis of Distributed Systems -- Automated Real Proving in PVS via MetiTarski -- Quiescent Consistency: Defining and Verifying Relaxed Linearizability -- Temporal Precedence Checking for Switched Models and Its Application to a Parallel Landing Protocol -- Contracts in Practice -- When Equivalence and Bisimulation Join Forces in Probabilistic Automata -- Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs -- Proof Patterns for Formal Methods -- Efficient Runtime Monitoring with Metric Temporal Logic: A Case Study in the Android Operating System -- IscasMc: A Web-Based Probabilistic Model Checker -- Invariants, Well-Founded Statements and Real-Time Program Algebra -- Checking Liveness Properties of Presburger Counter Systems Using Reachability Analysis -- A Symbolic Algorithm for the Analysis of Robust Timed Automata -- Revisiting Compatibility of Input-Output Modal Transition Systems -- Co-induction Simply: Automatic Co-inductive Proofs in a Program Verifier -- Management of Time Requirements in Component-Based Systems -- Compositional Synthesis of Concurrent Systems through Causal Model Checking and Learning -- Formal Verification of Operational Transformation -- Verification of a Transactional Memory Manager under Hardware Failures and Restarts -- SCJ: Memory-Safety Checking without Annotations -- Refactoring, Refinement and Reasoning: A Logical Characterization for Hybrid Systems -- Object Propositions -- Flexible Invariants through Semantic Collaboration -- Efficient Tight Field Bounds Computation Based on Shape Predicates -- A Graph-Based Transformation Reduction to Reach UPPAAL States Faster -- Computing Quadratic Invariants with Min- and Max-Policy Iterations: A Practical Comparison -- Efficient Self-composition for Weakest Precondition Calculi -- Towards a Formal Analysis of Information Leakage for Signature Attacks in Preferential Elections -- Analyzing Clinical Practice Guidelines Using a Decidable Metric Interval-Based Temporal Logic -- A Modular Theory of Object Orientation in Higher-Order UTP -- Formalizing and Verifying a Modern Build Language -- The Wireless Fire Alarm System: Ensuring Conformance to Industrial Standards through Formal Verification -- Formally Verifying Graphics FPU: An Intel® Experience -- MDP-Based Reliability Analysis of an Ambient Assisted Living System -- Diagnosing Industrial Business Processes: Early Experiences -- Formal Verification of Lunar Rover Control Software Using UPPAAL -- Formal Verification of a Descent Guidance Control Program of a Lunar Lander. |
| Record Nr. | UNISA-996203620803316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
FM 2014: Formal Methods : 19th International Symposium, Singapore, May 12-16, 2014. Proceedings / / edited by Cliff Jones, Pekka Pihlajasaari, Jun Sun
| FM 2014: Formal Methods : 19th International Symposium, Singapore, May 12-16, 2014. Proceedings / / edited by Cliff Jones, Pekka Pihlajasaari, Jun Sun |
| Edizione | [1st ed. 2014.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 |
| Descrizione fisica | 1 online resource (XVIII, 750 p. 185 illus.) |
| Disciplina | 005.1 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Mathematical logic Computer logic Management information systems Computer science Computers Software Engineering Mathematical Logic and Formal Languages Logics and Meanings of Programs Management of Computing and Information Systems Computation by Abstract Devices |
| ISBN | 3-319-06410-X |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Validity Checking of Put back Transformations in Bidirectional Programming -- Proof Engineering Considered Essential -- Engineering UToPiA: Formal Semantics for CML -- 40 Years of Formal Methods: Some Obstacles and Some Possibilities? -- A Refinement Based Strategy for Local Deadlock Analysis of Networks of CSP Processes -- Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools -- Definition, Semantics and Analysis of Multi rate Synchronous AADL -- Trust Found: Towards a Formal Foundation for Model Checking Trusted Computing Platforms -- The VerCors Tool for Verification of Concurrent Programs -- Knowledge-Based Automated Repair of Authentication Protocols -- A Simplified Z Semantics for Presentation Interaction Models -- Log Analysis for Data Protection Accountability -- Automatic Compositional Synthesis of Distributed Systems -- Automated Real Proving in PVS via MetiTarski -- Quiescent Consistency: Defining and Verifying Relaxed Linearizability -- Temporal Precedence Checking for Switched Models and Its Application to a Parallel Landing Protocol -- Contracts in Practice -- When Equivalence and Bisimulation Join Forces in Probabilistic Automata -- Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs -- Proof Patterns for Formal Methods -- Efficient Runtime Monitoring with Metric Temporal Logic: A Case Study in the Android Operating System -- IscasMc: A Web-Based Probabilistic Model Checker -- Invariants, Well-Founded Statements and Real-Time Program Algebra -- Checking Liveness Properties of Presburger Counter Systems Using Reachability Analysis -- A Symbolic Algorithm for the Analysis of Robust Timed Automata -- Revisiting Compatibility of Input-Output Modal Transition Systems -- Co-induction Simply: Automatic Co-inductive Proofs in a Program Verifier -- Management of Time Requirements in Component-Based Systems -- Compositional Synthesis of Concurrent Systems through Causal Model Checking and Learning -- Formal Verification of Operational Transformation -- Verification of a Transactional Memory Manager under Hardware Failures and Restarts -- SCJ: Memory-Safety Checking without Annotations -- Refactoring, Refinement and Reasoning: A Logical Characterization for Hybrid Systems -- Object Propositions -- Flexible Invariants through Semantic Collaboration -- Efficient Tight Field Bounds Computation Based on Shape Predicates -- A Graph-Based Transformation Reduction to Reach UPPAAL States Faster -- Computing Quadratic Invariants with Min- and Max-Policy Iterations: A Practical Comparison -- Efficient Self-composition for Weakest Precondition Calculi -- Towards a Formal Analysis of Information Leakage for Signature Attacks in Preferential Elections -- Analyzing Clinical Practice Guidelines Using a Decidable Metric Interval-Based Temporal Logic -- A Modular Theory of Object Orientation in Higher-Order UTP -- Formalizing and Verifying a Modern Build Language -- The Wireless Fire Alarm System: Ensuring Conformance to Industrial Standards through Formal Verification -- Formally Verifying Graphics FPU: An Intel® Experience -- MDP-Based Reliability Analysis of an Ambient Assisted Living System -- Diagnosing Industrial Business Processes: Early Experiences -- Formal Verification of Lunar Rover Control Software Using UPPAAL -- Formal Verification of a Descent Guidance Control Program of a Lunar Lander. |
| Record Nr. | UNINA-9910483145503321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
