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.
Verification, Model Checking, and Abstract Interpretation : 25th International Conference, VMCAI 2024, London, United Kingdom, January 15-16, 2024, Proceedings, Part I
| Verification, Model Checking, and Abstract Interpretation : 25th International Conference, VMCAI 2024, London, United Kingdom, January 15-16, 2024, Proceedings, Part I |
| Autore | Dimitrova Rayna |
| Edizione | [1st ed.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing AG, , 2024 |
| Descrizione fisica | 1 online resource (361 pages) |
| Altri autori (Persone) |
LahavOri
WolffSebastian |
| Collana | Lecture Notes in Computer Science Series |
| ISBN | 3-031-50524-7 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Invited Keynote Talks -- Two Projects on Human Interaction with AI -- Automating Relational Verification of Infinite-State Programs -- Contents - Part I -- Contents - Part II -- Abstract Interpretation -- Formal Runtime Error Detection During Development in the Automotive Industry -- 1 Introduction -- 2 Background -- 3 Module-Level Abstract Interpretation with Contracts -- 3.1 Generating a Verification Harness -- 3.2 Contracts and Their Effects -- 4 Automatically Inferring Contracts -- 4.1 Contracts from Interface Specifications -- 4.2 Contracts from Abstract Interpretation -- 5 Case Study -- 6 Practical Experiences with Large Systems -- 6.1 Embedded Control Software -- 6.2 Embedded Software Library -- 7 Lessons Learned -- 8 Related Work -- 9 Conclusion -- References -- Abstract Interpretation-Based Feature Importance for Support Vector Machines -- 1 Introduction -- 2 Background -- 3 Methodology -- 3.1 Abstract Feature Importance -- 3.2 Abstracting One-Hot Encoding -- 3.3 Individual Fairness -- 3.4 Searching for Counterexamples -- 4 Experimental Evaluation -- 5 Conclusion -- References -- Generation of Violation Witnesses by Under-Approximating Abstract Interpretation -- 1 Introduction -- 2 Semantics -- 2.1 Notation -- 2.2 Background on Sufficient Preconditions Semantic -- 2.3 User Input -- 2.4 Integer Wrapping -- 3 Powerset Domain -- 3.1 Under-Approximated Powerset -- 3.2 Case Study: Polyhedra Refinement -- 4 Implementation and Experiments -- 5 Conclusion -- References -- Correctness Witness Validation by Abstract Interpretation -- 1 Introduction -- 2 Preliminaries -- 2.1 Witnesses -- 2.2 Abstract Interpretation -- 3 Initialization-Based Approaches -- 4 Unassuming -- 4.1 Specification -- 4.2 Naïve Definition -- 4.3 Dual-Narrowing -- 5 Unassuming Indirectly -- 5.1 Propagating Unassume -- 6 Evaluation.
6.1 Precision Evaluation -- 6.2 Performance Evaluation -- 7 Related Work -- 8 Conclusion -- References -- Infinite-State Systems -- Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability -- 1 Introduction -- 2 Petri Nets and Polyhedral Abstraction -- 3 Combining Polyhedral Abstraction with Reachability -- 4 Projecting Formulas Using Token Flow Graphs -- 5 Formal Procedure and Proof of Correctness -- 6 Experimental Results -- 7 Discussion and Related Works -- References -- Parameterized Verification of Disjunctive Timed Networks -- 1 Introduction -- 2 Preliminaries -- 2.1 Parameterized Verification Problems -- 2.2 Symbolic Semantics of Timed Automata -- 3 Minimum-Time Reachability Algorithm for DTN- -- 3.1 Symbolic Semantics for DTN- -- 3.2 An Algorithm for Solving Minreach -- 3.3 Verification of DTNs -- 4 Conditions for Decidability with Location Invariants -- 5 Evaluation -- 6 Conclusion -- References -- Resilience and Home-Space for WSTS -- 1 Introduction -- 2 Well-Structured Transition Systems and VASS -- 3 Resilience for WSTS -- 3.1 Case: Safe="3222378 Safe -- 3.2 Case: Safe="3223379 Safe -- 4 State-Resilience -- 4.1 Case: Safe= "3222378 Safe -- 4.2 Case: Safe= "3223379 Safe -- 5 Resilience for VASS and Variations -- 6 Conclusion and Perspectives -- References -- Model Checking and Synthesis -- Generic Model Checking for Modal Fixpoint Logics in COOL-MC -- 1 Introduction -- 2 Model Checking for the Coalgebraic -Calculus -- 3 Implementation - Model Checking in COOL-MC -- 4 Experimental Evaluation of the Implementation -- 5 Conclusions and Future Work -- References -- Model-Guided Synthesis for LTL over Finite Traces -- 1 Introduction -- 2 Preliminaries -- 2.1 LTL over Finite Traces (LTLf) -- 2.2 Transition-Based DFA -- 2.3 LTLf Realizability, Synthesis, and tdfa Games -- 3 LTLf-to-tdfa via Progression. 4 Guided LTL f Synthesis with Satisfiable Traces -- 4.1 An Example -- 4.2 The Synthesis Algorithm MoGuS -- 4.3 Back to Our Example -- 5 Experimental Evaluation -- 5.1 Experimental Set-Up -- 5.2 Results and Analysis I: Random and Two-player-Games Benchmarks -- 5.3 Results and Analysis II: Ascending Benchmarks -- 6 LTL Synthesis - Related Work -- 7 Concluding Remarks -- References -- Solving Two-Player Games Under Progress Assumptions -- 1 Introduction -- 2 Preliminaries -- 3 Problem Statement -- 4 Strong Transition Fairness Assumptions -- 5 Strong Transition Co-fairness Assumptions -- 6 Group Transition Fairness Assumptions -- 6.1 Live Group Assumptions -- 6.2 Singleton-Source Live Groups -- 6.3 Live Groups in Product Games -- 6.4 A Remark on Co-live Groups -- 7 Persistent Live Group Assumptions -- 7.1 Augmented Reachability Games -- 7.2 Augmented Parity Games -- References -- SAT, SMT, and Automated Reasoning -- Interpolation and Quantifiers in Ortholattices -- 1 Introduction -- 2 Quantified Orthologic: Syntax, Semantics, and a Complete Proof System -- 2.1 Complete Ortholattices -- 2.2 Soundness -- 2.3 Completeness -- 3 No Quantifier Elimination for Orthologic -- 4 Failure of a Refutation-Based Interpolation -- 5 Interpolation for Orthologic Formulas -- 6 Further Related Work -- 7 Conclusion -- References -- Function Synthesis for Maximizing Model Counting -- 1 Introduction -- 2 Problem Statement -- 2.1 Preliminaries -- 2.2 Problem Formulation -- 2.3 Hardness of DQMax#SAT -- 3 Global Method -- 4 Incremental Method -- 5 Local Method -- 5.1 Reducing Common Dependencies -- 5.2 Solving Variables with No Dependencies -- 6 Application to Software Security -- 6.1 Our Model of Security in Presence of an Adaptive Adversary -- 6.2 Security as a Rechability Property -- 6.3 Security as a Lack of Leakage Property. 6.4 Some Remarks About the Applications to Security -- 7 Implementation and Experiments -- 8 Related Work -- 9 Conclusions -- References -- Boosting Constrained Horn Solving by Unsat Core Learning -- 1 Introduction -- 2 Preliminaries -- 2.1 Notations -- 2.2 Constraint Horn Clauses -- 2.3 Graph Neural Networks -- 3 Abstract Symbolic Model Checking for CHCs -- 3.1 Satisfiability Checking for CHCs -- 3.2 CEGAR- And Symbolic Execution-Style Exploration -- 4 Guiding CHC Solvers Using MUSes -- 4.1 Minimal Unsatisfiable Sets -- 4.2 MUS-Based Guidance for CHC Solvers -- 5 Design of Model -- 5.1 Encode CHCs to Graph Representation -- 5.2 Model Structure -- 6 Evaluation -- 6.1 Benchmark -- 6.2 Parameters -- 6.3 Experimental Results -- 7 Related Work -- 8 Conclusion and Future Works -- References -- On the Verification of the Correctness of a Subgraph Construction Algorithm -- 1 Introduction -- 2 The CP-Algorithm -- 2.1 The CP-Algorithm -- Idea of the Correctness Proof -- 3 Modeling Geometric Graphs -- 3.1 Geometric Axioms -- 3.2 Axiomatizing Graph Properties -- 3.3 Axioms for Notions Used in the CP-Algorithm -- 3.4 Axioms for Notions Used in the Correctness Proof -- 4 Automated Reasoning -- 4.1 Analyzing the Axioms -- Decidability -- 4.2 Choosing the Proof Systems -- 4.3 Automated Proof of Properties of Geometric Graphs -- 4.4 Correctness of the CP-Algorithm: Verifying Main Steps -- 4.5 Connection Between the Components X and Y -- 4.6 Proof of Properties for the Convex Hull -- 4.7 Constructing a Counterexample Without Coexistence Property -- 5 Conclusion -- References -- Efficient Local Search for Nonlinear Real Arithmetic -- 1 Introduction -- 1.1 Contributions -- 1.2 Related Work -- 1.3 Structure of the Paper -- 2 Preliminaries -- 3 Incremental Computation of Variable Scores -- 4 Relaxation of Equalities -- 5 Implementation. 5.1 Heuristic Moves Selection and Look-Ahead -- 5.2 Implementation Details -- 6 Evaluation -- 6.1 Overall Result -- 6.2 Comparison with Other Work on Local Search -- 6.3 Effect of Incremental Computation of Variable Scores -- 6.4 Effect of Relaxation of Equalities -- 6.5 Other Techniques -- 7 Conclusion -- References -- Author Index. |
| Record Nr. | UNISA-996587865903316 |
Dimitrova Rayna
|
||
| Cham : , : Springer International Publishing AG, , 2024 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Verification, Model Checking, and Abstract Interpretation : 25th International Conference, VMCAI 2024, London, United Kingdom, January 15-16, 2024, Proceedings, Part II
| Verification, Model Checking, and Abstract Interpretation : 25th International Conference, VMCAI 2024, London, United Kingdom, January 15-16, 2024, Proceedings, Part II |
| Autore | Dimitrova Rayna |
| Edizione | [1st ed.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing AG, , 2024 |
| Descrizione fisica | 1 online resource (349 pages) |
| Altri autori (Persone) |
LahavOri
WolffSebastian |
| Collana | Lecture Notes in Computer Science Series |
| ISBN | 3-031-50521-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
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 -- 4 Abstraction-Based Training -- 4.1 Approach Overview -- 4.2 Interval-Based State Abstraction -- 5 Abstraction-Based Reachability Analysis -- 5.1 Approach Overview.
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. 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 Combining Operational and Declarative RV. 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. |
| Record Nr. | UNISA-996587866003316 |
|
Dimitrova Rayna
|
||
| Cham : , : Springer International Publishing AG, , 2024 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Verification, Model Checking, and Abstract Interpretation : 25th International Conference, VMCAI 2024, London, United Kingdom, January 15–16, 2024, Proceedings, Part I / / edited by Rayna Dimitrova, Ori Lahav, Sebastian Wolff
| Verification, Model Checking, and Abstract Interpretation : 25th International Conference, VMCAI 2024, London, United Kingdom, January 15–16, 2024, Proceedings, Part I / / edited by Rayna Dimitrova, Ori Lahav, Sebastian Wolff |
| Autore | Dimitrova Rayna |
| Edizione | [1st ed. 2024.] |
| Pubbl/distr/stampa | Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2024 |
| Descrizione fisica | 1 online resource (361 pages) |
| Disciplina | 004.0151 |
| Altri autori (Persone) |
LahavOri
WolffSebastian |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer science
Computer science - Mathematics Logic programming Computers, Special purpose Software engineering Microprogramming Theory of Computation Mathematics of Computing Logic in AI Special Purpose and Application-Based Systems Software Engineering Control Structures and Microprogramming |
| ISBN | 3-031-50524-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Abstract Interpretation -- Formal Runtime Error Detection During Development in the Automotive Industry -- Abstract Interpretation-Based Feature Importance for Support Vector Machines -- Generation of Violation Witnesses by Under-Approximating Abstract Interpretation -- Correctness Witness Validation by Abstract Interpretation -- Infinite-State Systems -- Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability -- Parameterized Verification of Disjunctive Timed Networks -- Resilience and Home-Space for WSTS -- Model Checking and Synthesis -- Generic Model Checking for Modal Fixpoint Logics in COOL-MC -- Model-Guided Synthesis for LTL over Finite Traces -- Solving Two-Player Games under Progress Assumptions -- AT, SMT, and Automated Reasoning Interpolation and Quantifiers in Ortholattices -- Function Synthesis for Maximizing Model Counting -- Boosting Constrained Horn Solving by Unsat Core Learning -- On the Verification of a Subgraph Construction Algorithm -- Efficient Local Search for Nonlinear Real Arithmetic. |
| Record Nr. | UNINA-9910799207203321 |
|
Dimitrova Rayna
|
||
| Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2024 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Verification, Model Checking, and Abstract Interpretation : 25th International Conference, VMCAI 2024, London, United Kingdom, January 15–16, 2024, Proceedings, Part II / / edited by Rayna Dimitrova, Ori Lahav, Sebastian Wolff
| Verification, Model Checking, and Abstract Interpretation : 25th International Conference, VMCAI 2024, London, United Kingdom, January 15–16, 2024, Proceedings, Part II / / edited by Rayna Dimitrova, Ori Lahav, Sebastian Wolff |
| Edizione | [1st ed. 2024.] |
| Pubbl/distr/stampa | Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2024 |
| Descrizione fisica | 1 online resource (349 pages) |
| Disciplina | 005.14 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer science
Computer science - Mathematics Logic programming Computers, Special purpose Software engineering Microprogramming Theory of Computation Mathematics of Computing Logic in AI Special Purpose and Application-Based Systems Software Engineering Control Structures and Microprogramming |
| ISBN | 3-031-50521-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Concurrency -- Petrification: Software Model Checking for Programs with Dynamic Thread Management -- A Fully Verified Persistency Library -- A Navigation Logic for Recursive Programs with Dynamic Thread Creation -- Neural Networks -- Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training -- Verification of Neural Networks' Local Differential Classification Privacy -- AGNES: Abstraction-guided Framework for Deep Neural Network Security -- Probabilistic and Quantum Programs Guaranteed inference for probabilistic programs: a parallelisable, small-step operational approach -- Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs -- Program and System Verification -- Deductive Verification of Parameterized Embedded Systems modeled in SystemC -- Automatically Enforcing Rust Trait Properties -- Borrowable Fractional Ownership Types for Verification -- Runtime Verification -- TP-DejaVu: Combining Operational and Declarative Runtime Verification -- Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic -- Security and Privacy -- Automatic and Incremental Repair for Speculative Information Leaks -- Sound Abstract Nonexploitability Analysis. |
| Record Nr. | UNINA-9910799214203321 |
| Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2024 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||