{"text_format":"2","workbook":"xls","n_sheets":1,"sheets":["report2"],"not_rendered":{"charts":0,"images":0,"macros":0,"external_links":1,"defined_names":2,"comments":0,"pivot_tables":0},"unopened":[],"bounds":{"document_bytes":16777216,"sheet_cells":100000,"run_cost":"one","rows_first":2000,"rows_last":500,"rows_between":2000,"halvings":0,"cell_chars":16384,"cell_head_chars":4096},"cells_cut":0,"cells_raw":0,"read":"whole","date_system":"1900","formulas":"cached_only"}

{"sheet":"report2","index":0,"n_rows":41,"n_cols":5,"rows_kept":41,"cut":false,"hidden":false,"merged":[[0,2,0,3],[0,4,0,5],[1,2,1,3],[1,4,1,5],[2,2,2,3],[2,4,2,5],[3,2,3,3],[4,2,4,3],[5,2,5,3],[6,2,6,3],[7,2,7,3],[9,2,9,3],[12,2,12,3],[16,2,16,3],[18,2,18,3],[20,2,20,3],[20,4,20,5],[21,2,21,3],[21,4,21,5],[22,2,22,3],[22,4,22,5],[23,2,23,3],[25,2,25,3],[26,2,26,3],[27,2,27,3],[28,2,28,3],[29,2,29,3],[30,2,30,3],[32,2,32,3]],"flags":["formulas_cached_only"]}
[null,"1.","Record Nr.",null,"UNINA990001737140403321"]
[null,null,"Autore",null,"Plinius Secundus, Gaius <23-70>"]
[null,null,"Titolo",null,"Della storia naturale : libri XXXVII / di C. Plinio Secondo ; traduzione di Lodovico Domenichi emendata per la prima volta secondo il testo latino con l'aggiunta di un nuovo indice generale"]
[null,null,"Pubbl/distr/stampa",null,"Venezia, : Antonelli, 1844"]
[null,null,"Titolo uniforme",null,"Historiae mundi <in italiano e in latino>"]
[null,null,"Descrizione fisica",null,"2 v. (XXX p., 1806 col.; 1824 col.) ; 26 cm"]
[null,null,"Collana",null,"Biblioteca degli scrittori latini con traduzione e note"]
[null,null,"Disciplina",null,"500.9"]
[{"$nulls":4},"878"]
[null,null,"Locazione",null,"BAT"]
[{"$nulls":4},"DBV"]
[{"$nulls":4},"FAGBC"]
[null,null,"Collocazione",null,"BIB. BAT.1482(1)"]
[{"$nulls":4},"P I 8"]
[{"$nulls":4},"P I 9"]
[{"$nulls":4},"60 870 B 1"]
[null,null,"Lingua di pubblicazione",null,"Italiano"]
[{"$nulls":4},"Latino"]
[null,null,"Formato",null,"Materiale a stampa"]
[null,null,null,"Livello bibliografico","Monografia"]
[null,"2.","Record Nr.",null,"UNISA996587866703316"]
[null,null,"Autore",null,"Hermanns Holger"]
[null,null,"Titolo",null,"Dependable Software Engineering. Theories, Tools, and Applications : 9th International Symposium, SETTA 2023, Nanjing, China, November 27-29, 2023, Proceedings"]
[null,null,"Pubbl/distr/stampa",null,"Singapore : , : Springer, , 2024"]
[{"$nulls":4},"©2024"]
[null,null,"ISBN",null,"981-9986-64-8"]
[null,null,"Edizione",null,"[1st ed.]"]
[null,null,"Descrizione fisica",null,"1 online resource (448 pages)"]
[null,null,"Collana",null,"Lecture Notes in Computer Science Series ; ; v.14464"]
[null,null,"Lingua di pubblicazione",null,"Inglese"]
[null,null,"Formato",null,"Materiale a stampa"]
[null,null,null,"Livello bibliografico","Monografia"]
[null,null,"Nota di contenuto",null,"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 "]
[{"$nulls":4},"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."]
[{"$nulls":4},"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."]
[{"$nulls":4},"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&amp -- 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 "]
[{"$nulls":4},"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."]
[{"$nulls":4},"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."]
[{"$nulls":4},"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 -- "]
[{"$nulls":4},"5.2 Simulation and Expanded Test -- 6 Conclusions -- References."]
[{"$nulls":4},"An Abstract Domain of Linear Templates with Disjunctive Right-Hand-Side Intervals."]