{"text_format":"2","workbook":"xls","n_sheets":1,"sheets":["report2"],"not_rendered":{"charts":0,"images":0,"macros":0,"external_links":1,"defined_names":1,"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":18,"n_cols":5,"rows_kept":18,"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],[5,2,5,3],[6,2,6,3],[7,2,7,3],[8,2,8,3],[9,2,9,3],[10,2,10,3],[12,2,12,3]],"flags":["formulas_cached_only"]}
[null,"1.","Record Nr.",null,"UNISA996587866003316"]
[null,null,"Autore",null,"Dimitrova Rayna"]
[null,null,"Titolo",null,"Verification, Model Checking, and Abstract Interpretation : 25th International Conference, VMCAI 2024, London, United Kingdom, January 15-16, 2024, Proceedings, Part II"]
[null,null,"Pubbl/distr/stampa",null,"Cham : , : Springer International Publishing AG, , 2024"]
[{"$nulls":4},"©2024"]
[null,null,"ISBN",null,"3-031-50521-2"]
[null,null,"Edizione",null,"[1st ed.]"]
[null,null,"Descrizione fisica",null,"1 online resource (349 pages)"]
[null,null,"Collana",null,"Lecture Notes in Computer Science Series ; ; v.14500"]
[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 -- Invited Keynote Talks -- Two Projects on Human Interaction with AI -- Automating Relational Verification of Infinite-State Programs -- Contents - Part II -- Contents - Part I -- Concurrency -- Petrification: Software Model Checking for Programs with Dynamic Thread Management -- 1 Introduction -- 2 A Language for Dynamic Thread Creation -- 3 Petrification -- 3.1 Petri Programs -- 3.2 Transformation to Petri Programs -- 3.3 Properties of the Petrified Program -- 4 Verifying Programs Through Repeated Petrification -- 5 Application: Verification of C Programs -- 5.1 Translation from Pthreads to Conc Programs -- 5.2 Practical Performance of the Approach -- 6 Conclusion -- References -- A Fully Verified Persistency Library -- 1 Introduction -- 2 Motivation -- 3 Using IOAs to Verify (Durable) Linearizability -- 4 Abstract Persistency Library and Its Correctness -- 5 The Library FliT and Memory Models -- 6 Proving Correctness of FliT -- 6.1 Proof of FliT [wPSC] PLibIR -- 6.2 Proof of FliT [PTSO ] FliT [wPSC] -- 7 Related Work -- 8 Conclusion -- References -- A Navigation Logic for Recursive Programs with Dynamic Thread Creation -- 1 Introduction -- 2 Preliminaries -- 3 Graph Semantics of Dynamic Pushdown Networks -- 4 A Navigation Logic for Dynamic Pushdown Networks -- 5 Example Properties -- 6 From Graph Semantics to Tree Semantics -- 7 Model Checking and Satisfiability -- 8 Conclusion -- References -- Neural Networks -- Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training -- 1 Introduction -- 2 Preliminaries -- 2.1 DNN-Controlled Systems -- 2.2 Reachability Problem of DNN-Controlled Systems -- 3 Motivation "]
[{"$nulls":4},"-- 4 Abstraction-Based Training -- 4.1 Approach Overview -- 4.2 Interval-Based State Abstraction -- 5 Abstraction-Based Reachability Analysis -- 5.1 Approach Overview."]
[{"$nulls":4},"5.2 Key Operations in Algorithm 1 -- 5.3 The Soundness -- 6 Implementation and Experiments -- 6.1 Implementation and Benchmarks -- 6.2 Performance of Trained Neural Networks -- 6.3 Tightness and Efficiency -- 6.4 Differential and Decomposing Analysis -- 7 Related Work -- 8 Conclusion and Future Work -- References -- Verification of Neural Networks' Local Differential Classification Privacy -- 1 Introduction -- 2 Preliminaries -- 3 Local Differential Classification Privacy -- 4 Our Approach -- 5 Sphynx: Safety Privacy Analyzer via Hyper-networks -- 5.1 Prediction of an Interval Hyper-network -- 5.2 Verification of a Hyper-network -- 5.3 Analysis of Sphynx -- 6 Evaluation -- 7 Related Work -- 8 Conclusion -- References -- AGNES: Abstraction-Guided Framework for Deep Neural Networks Security -- 1 Introduction -- 2 Preliminaries -- 2.1 Deep Neural Networks -- 2.2 Abstraction -- 2.3 Stimulation -- 3 Methodology -- 3.1 Identifying Cluster Representatives -- 3.2 Stimulation Techniques -- 4 Tool Architecture -- 5 Experiments -- 5.1 Backdoor Identification and Runtime Reduction -- 5.2 Performance on Various Triggers -- 6 Conclusion -- References -- Probabilistic and Quantum Programs -- Guaranteed Inference for Probabilistic Programs: A Parallelisable, Small-Step Operational Approach -- 1 Introduction -- 2 Preliminaries on Measure Theory -- 3 Probabilistic Programs -- 4 Observable Semantics -- 5 Inference via Vectorized Monte Carlo Sampling -- 6 Implementation and Evaluation -- 6.1 TSI: A TensorFlow Based Implementation -- 6.2 Evaluation of TSI -- 7 Conclusion -- References -- Local Reasoning About Probabilistic Behaviour for Classical-Quantum Programs -- 1 Introduction -- 2 Preliminaries -- 3 A Classical-Quantum Language -- 3.1 Syntax -- 3.2 Denotational Semantics -- 4 Proof System -- 4.1 Assertion Language -- 4.2 Proof System -- 5 Examples."]
[{"$nulls":4},"5.1 HHL Algorithm -- 5.2 Shor's Algorithm -- 6 Conclusion and Future Work -- References -- Program and System Verification -- Deductive Verification of Parameterized Embedded Systems Modeled in SystemC -- 1 Introduction -- 2 Background -- 2.1 SystemC -- 2.2 VerCors -- 3 Encoding the SystemC Semantics in PVL -- 3.1 Assumptions -- 3.2 Encoding of Events and Concurrent Processes -- 3.3 Encoding of SystemC Designs -- 4 Deductive Verification of SystemC Designs -- 4.1 Property Specification and Verification -- 4.2 Reachable Abstract States Invariant -- 4.3 Variables in the Abstract State -- 4.4 RASI Generation and Soundness -- 4.5 Verifying Global Properties with the RASI -- 5 Evaluation -- 5.1 Case Studies -- 5.2 Experimental Results -- 5.3 Scalability -- 5.4 Discussion -- 6 Related Work -- 7 Conclusion -- References -- Automatically Enforcing Rust Trait Properties -- 1 Introduction -- 2 Background and Related Work -- 2.1 Rust Traits -- 2.2 Kani -- 2.3 Related Work -- 3 Verifying Rust Trait Invariants -- 3.1 Workflow for Verifying Trait Invariants -- 3.2 Harnesses for Trait Invariants -- 4 Implementation and Evaluation -- 4.1 Implementation -- 4.2 Evaluation -- 4.3 Results -- 5 Limitations and Future Work -- 6 Conclusion -- References -- Borrowable Fractional Ownership Types for Verification -- 1 Introduction -- 2 Source Language -- 2.1 Syntax -- 2.2 Operational Semantics -- 3 Type System -- 3.1 Syntax of Types -- 3.2 Typing Rules -- 3.3 Type Preservation -- 4 Translation -- 4.1 Target Language -- 4.2 Translation Rules -- 4.3 Soundness -- 5 Preliminary Experiments -- 6 Related Work -- 7 Conclusion and Future Work -- References -- Runtime Verification -- TP-DejaVu: Combining Operational and Declarative Runtime Verification -- 1 Introduction -- 2 "]
[{"$nulls":4},"Combining Operational and Declarative RV."]
[{"$nulls":4},"2.1 Declarative Specification in Past Time First-Order Temporal Logic -- 2.2 RV Monitoring First-Order Past LTL -- 2.3 The Operational RV -- 2.4 Examples from Use Cases of Autonomous Systems -- 3 The TP-DejaVuTool and Experimental Results -- 4 Conclusions and Further Work -- References -- Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic -- 1 Introduction -- 2 Preliminaries -- 3 The Problem Formulation -- 4 Existence of a Solution -- 5 An SMT-Based Algorithm -- 6 Experiments -- 7 Discussion and Conclusion -- References -- Security and Privacy -- Automatic and Incremental Repair for Speculative Information Leaks -- 1 Introduction -- 2 Preliminaries -- 2.1 Model Checking Programs -- 2.2 Standard Program Semantics -- 3 Modeling Speculative Execution Semantics -- 3.1 Threat Models for Speculative Information Leaks -- 3.2 Formal Model of Speculative Execution Semantics -- 3.3 Reducing Speculative Non-interference to a Safety Property -- 4 Automatic Repair Under Speculative Execution -- 4.1 Analyzing the Leaking Execution -- 4.2 Properties of CureSpec (Algorithm 2) -- 4.3 Heuristics and Optimizations -- 5 Implementation and Evaluation -- 6 Related Work -- 7 Conclusions -- References -- Sound Abstract Nonexploitability Analysis -- 1 Introduction -- 2 Motivation -- 3 Syntax and Concrete Semantics -- 4 Nonexploitability -- 5 Taint Concrete Semantics -- 6 Taint Abstract Semantics -- 7 Experimental Evaluation -- 8 Related Work -- 9 Conclusions -- References -- Author Index."]