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.
Computer Aided Verification [[electronic resource] ] : 35th International Conference, CAV 2023, Paris, France, July 17–22, 2023, Proceedings, Part III / / edited by Constantin Enea, Akash Lal
| Computer Aided Verification [[electronic resource] ] : 35th International Conference, CAV 2023, Paris, France, July 17–22, 2023, Proceedings, Part III / / edited by Constantin Enea, Akash Lal |
| Edizione | [1st ed. 2023.] |
| Pubbl/distr/stampa | Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2023 |
| Descrizione fisica | 1 online resource (XVII, 502 p. 140 illus., 88 illus. in color.) |
| Disciplina | 005.1 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Artificial intelligence Algorithms Computer engineering Computer networks Software Engineering Artificial Intelligence Design and Analysis of Algorithms Computer Engineering and Networks |
| ISBN | 3-031-37709-5 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Contents - Part III -- Probabilistic Systems -- A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties -- 1 Introduction -- 2 Theoretical Background -- 2.1 Solving Rabin Games Symbolically -- 2.2 Computing Symbolic Controllers for Stochastic Dynamical Systems -- 3 Implementation Details -- 3.1 Genie -- 3.2 FairSyn -- 3.3 Mascot-SDS -- 4 Examples -- 4.1 Synthesizing Code-Aware Resource Mangers Using FairSyn -- 4.2 Synthesizing Controllers for Stochastic Dynamical Systems Using Mascot-SDS -- References -- Automated Tail Bound Analysis for Probabilistic Recurrence Relations -- 1 Introduction -- 2 Preliminaries -- 2.1 Probabilistic Recurrence Relations -- 3 Exponential Tail Bounds via Markov's Inequality -- 4 An Algorithmic Approach -- 4.1 The Guess Procedure Guess(f,t) -- 4.2 The Check Procedure CheckCond(cf,ct) -- 5 Experimental Results -- 6 Related Work -- References -- Compositional Probabilistic Model Checking with String Diagrams of MDPs -- 1 Introduction -- 2 String Diagrams of MDPs -- 2.1 Outline -- 2.2 Open MDPs -- 2.3 Rightward Open MDPs and Traced Monoidal String Diagrams -- 2.4 TSMC Equations Between roMDPs -- 2.5 Open MDPs and ``Compact Closed'' String Diagrams -- 3 Decomposition Equalities for Open Markov Chains -- 4 Semantic Categories and Solution Functors -- 4.1 Semantic Category for Rightward Open MCs -- 4.2 Semantic Category of Rightward Open MDPs -- 4.3 Semantic Category of MDPs -- 5 Implementation and Experiments -- References -- Efficient Sensitivity Analysis for Parametric Robust Markov Chains -- 1 Introduction -- 2 Overview -- 3 Formal Problem Statement -- 4 Differentiating Solution Functions for pMCs -- 4.1 Computing Derivatives Explicitly -- 4.2 Computing k-Highest Derivatives -- 5 Differentiating Solution Functions for prMCs.
5.1 Computing Derivatives via pMCs (and When It Does Not Work) -- 5.2 Computing Derivatives Explicitly -- 5.3 Computing k-Highest Derivatives -- 6 Numerical Experiments -- 7 Related Work -- 8 Concluding Remarks -- References -- MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives -- 1 Introduction -- 1.1 Related Work -- 2 Preliminaries -- 2.1 Markov Systems -- 2.2 MDPs as Distribution Transformers -- 3 Problem Statement and Examples -- 4 Proving Safety by Invariants -- 4.1 Distribution Strategies -- 4.2 Distributional Invariants for MDP Safety -- 5 Algorithms for Distributional Invariant Synthesis -- 5.1 Synthesis of Affine Invariants and Memoryless Strategies -- 5.2 Synthesis of Affine Invariants and General Strategies -- 6 Discussion, Extensions, and Variants -- 7 Implementation and Evaluation -- 8 Conclusion -- References -- Search and Explore: Symbiotic Policy Synthesis in POMDPs -- 1 Introduction -- 2 Motivating Examples -- 3 Preliminaries and Problem Statement -- 4 FSCs for and from Belief Exploration -- 4.1 Belief Exploration with Explicit FSC Construction -- 4.2 Using FSCs for Cut-Off Values -- 4.3 Extracting FSC from Belief Exploration -- 5 Accelerated Inductive Synthesis -- 5.1 Inductive Synthesis with k-FSCs -- 5.2 Using Reference Policies to Accelerate Inductive Synthesis -- 5.3 Inductive Synthesis with Adequate FSCs -- 6 Integrating Belief Exploration with Inductive Synthesis -- 7 Experiments -- 8 Conclusion and Future Work -- References -- Security and Quantum Systems -- AutoQ: An Automata-Based Quantum Circuit Verifier -- 1 Introduction -- 2 Tree Automata-Based Verification of Quantum Circuits -- 2.1 High-Level Specification Language -- 2.2 Complex Number Representation -- 2.3 Precise Semantics of the Specification -- 3 Entailment Checking -- 4 Architecture -- 5 Use Cases. 5.1 Hadamard Square is Identity -- 5.2 Zero Imaginary Part of Amplitudes -- 5.3 Probability of Measuring the Correct Answer -- 5.4 Increasing Amplitude of the Correct Answer -- 6 Conclusion -- References -- Bounded Verification for Finite-Field-Blasting -- 1 Introduction -- 1.1 Related Work -- 2 Background -- 2.1 Logic -- 2.2 Zero Knowledge Proofs -- 2.3 Compilation Targeting Zero Knowledge Proofs -- 3 Overview and Example -- 3.1 An Example of Field-Blasting -- 3.2 Key Ideas -- 4 Architecture -- 4.1 Encodings -- 4.2 Encoding Rules -- 4.3 Calculus -- 5 Verification Conditions -- 5.1 Correctness Definition -- 5.2 Rule VCs -- 5.3 A Correct Field-Blasting Calculus -- 6 Case Study: A Verifiable Field-Blaster for CirC -- 6.1 Verification Evaluation -- 6.2 Performance and Output Quality Evaluation -- 7 Discussion -- A Zero-Knowledge Proofs and Compilers -- B Compiler Correctness Proofs -- C CirC-IR -- D Optimizations to the CirC Field-Blaster -- E Verified Field-Blaster Performance Details -- F Verifier Performance Details -- G Bugs Found in the CirC Field Blaster -- References -- Formally Verified EVM Block-Optimizations -- 1 Introduction -- 2 Background -- 3 EVM Semantics in Coq -- 4 Formal Verification of EVM-Optimizations in Coq -- 4.1 EVM Symbolic Execution in Coq -- 4.2 Simplification Rules -- 4.3 Stacks Equivalence Modulo Commutativity -- 5 Implementation and Experimental Evaluation -- 6 Conclusions, Related and Future Work -- References -- SR-SFLL: Structurally Robust Stripped Functionality Logic Locking -- 1 Introduction -- 2 Background -- 2.1 Stripped Functionality Logic Locking (SFLL) -- 2.2 SFLL Attacks -- 2.3 Analysis of the Structural Attacks on SFLL -- 3 Overview -- 3.1 Preliminaries -- 3.2 Approach -- 4 SR-SFLL -- 4.1 Problem Statement -- 4.2 Intuition: SR-SFLL -- 4.3 Methodology: SR-SFLL -- 5 SyntAk -- 6 Evaluation. 6.1 Robustness of SR-SELL(0) and SR-SELL on Existing Attacks -- 6.2 Robustness of SR-SELL(0) and SR-SELL on SyntAk -- 6.3 Overhead of SR-SELL(0) and SR-SELL -- 7 Related Work -- 8 Conclusions -- References -- Symbolic Quantum Simulation with Quasimodo -- 1 Introduction -- 2 Background on Quantum Simulation -- 3 Quasimodo's Programming and Analysis Interface -- 3.1 Extending Quasimodo -- 4 The Internals of Quasimodo -- 5 Experiments -- 6 Conclusion -- References -- Verifying the Verifier: eBPF Range Analysis Verification -- 1 Introduction -- 2 Background on Abstract Interpretation -- 3 Abstract Interpretation in the Linux Kernel -- 4 Automatic Verification of the Kernel's Algorithms -- 4.1 Soundness Specification for Abstraction/Reduction Operators -- 4.2 Refining Soundness Specification with Input Preconditioning -- 4.3 Automatically Producing Programs Exercising Soundness Bugs -- 5 C to Logic for Kernel's Abstract Operators -- 6 Experimental Evaluation -- 7 Limitations and Caveats -- 8 Related Work -- 9 Conclusion -- References -- Software Verification -- Automated Verification of Correctness for Masked Arithmetic Programs -- 1 Introduction -- 2 Preliminaries -- 3 The Core Language -- 4 Overview of the Approach -- 4.1 Our Approach -- 5 Term Rewriting System -- 6 Algorithmic Verification -- 6.1 Term Normalization Algorithm -- 6.2 Computing Affine Constants -- 6.3 Verification Algorithm -- 6.4 Implementation Remarks -- 7 Evaluation -- 7.1 Evaluation for Computing Affine Constants -- 7.2 Evaluation for Correctness Verification -- 7.3 Scalability of FISCHER -- 7.4 Evaluation for More Boolean Masking Schemes -- 7.5 Evaluation for Arithmetic/Boolean Masking Conversions -- 8 Conclusion -- References -- Automatic Program Instrumentation for Automatic Verification -- 1 Introduction -- 2 Instrumentation Framework -- 2.1 The Core Language. 2.2 Instrumentation Operators -- 2.3 Instrumentation Correctness -- 3 Instrumentation Application Strategies -- 4 Instrumentation Operators for Arrays -- 4.1 Instrumentation Operators for Quantification over Arrays -- 4.2 Instrumentation Operators for Aggregation over Arrays -- 5 Evaluation -- 5.1 Implementation -- 5.2 Experiments and Comparisons -- 6 Related Work -- 7 Conclusion -- References -- Boolean Abstractions for Realizability Modulo Theories -- 1 Introduction -- 2 Preliminaries -- 3 Boolean Abstraction -- 3.1 Notation -- 3.2 The Boolean Abstraction Algorithm -- 3.3 From Local Simulation to Equi-Realizability -- 4 Efficient Algorithms for Boolean Abstraction -- 4.1 Quasi-reactions -- 4.2 Quasi-reaction-based Optimizations -- 4.3 A Single Model-Loop Algorithm (Algorithm 2) -- 4.4 A Nested-SAT Algorithm (Algorithm 3) -- 5 Empirical Evaluation -- 6 Related Work and Conclusions -- References -- Certified Verification for Algebraic Abstraction -- 1 Introduction -- 2 Preliminaries -- 3 ToyLang -- 3.1 Syntax and Semantics -- 4 Algebraic Abstraction -- 4.1 Soundness Conditions -- 4.2 Polynomial Program Verification -- 5 Certified Verification -- 5.1 Verified Abstraction Algorithm -- 5.2 Verification through Certification -- 5.3 Optimization -- 6 Evaluation -- 6.1 Field and Group Operation in Elliptic Curves -- 6.2 Number-Theoretic Transform in Kyber -- 7 Conclusion -- References -- Complete Multiparty Session Type Projection with Automata -- 1 Introduction -- 2 Motivation and Overview -- 3 Preliminaries -- 4 Synthesizing Implementations -- 5 Checking Implementability -- 6 Soundness -- 7 Completeness -- 8 Complexity -- 9 Evaluation -- 10 Discussion -- 11 Related Work -- References -- Early Verification of Legal Compliance via Bounded Satisfiability Checking -- 1 Introduction -- 2 Preliminaries -- 3 Bounded Satisfiability Checking Problem. 4 Checking Bounded Satisfiability. |
| Record Nr. | UNISA-996542663403316 |
| Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2023 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Computer Aided Verification [[electronic resource] ] : 35th International Conference, CAV 2023, Paris, France, July 17–22, 2023, Proceedings, Part I / / edited by Constantin Enea, Akash Lal
| Computer Aided Verification [[electronic resource] ] : 35th International Conference, CAV 2023, Paris, France, July 17–22, 2023, Proceedings, Part I / / edited by Constantin Enea, Akash Lal |
| Edizione | [1st ed. 2023.] |
| Pubbl/distr/stampa | Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2023 |
| Descrizione fisica | 1 online resource (XXXI, 488 p. 160 illus., 121 illus. in color.) |
| Disciplina | 005.1 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Artificial intelligence Algorithms Computer engineering Computer networks Software Engineering Artificial Intelligence Design and Analysis of Algorithms Computer Engineering and Networks |
| ISBN | 3-031-37706-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Invited Talks -- Privacy-Preserving Automated Reasoning -- Enhancing Programming Experiences Using AI: Leveraging LLMs as Analogical Reasoning Engines and Beyond -- Verified Software Security Down to Gates -- Contents - Part I -- Contents - Part II -- Contents - Part III -- Automata and Logic -- Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization -- 1 Introduction -- 2 Preliminaries -- 2.1 Timed Words and Timed Automata -- 2.2 Recognizable Timed Languages -- 2.3 Distinguishing Extensions and Active DFA Learning -- 3 A Myhill-Nerode Style Characterization of Recognizable Timed Languages with Elementary Languages -- 4 Active Learning of Deterministic Timed Automata -- 4.1 Successors of Simple Elementary Languages -- 4.2 Timed Observation Table for Active DTA Learning -- 4.3 Counterexample Analysis -- 4.4 L*-Style Learning Algorithm for DTAs -- 4.5 Learning with a Normal Teacher -- 4.6 Complexity Analysis -- 5 Experiments -- 5.1 RQ1: Scalability with Respect to the Language Complexity -- 5.2 RQ2: Performance on Practical Benchmarks -- 6 Conclusions and Future Work -- References -- Automated Analyses of IOT Event Monitoring Systems -- 1 Introduction -- 2 Overview -- 3 Technique -- 3.1 Well-formedness Properties -- 4 Experiments -- 5 Conclusion -- A Common Issues with Detector Models -- References -- Learning Assumptions for Compositional Verification of Timed Automata -- 1 Introduction -- 2 Preliminaries -- 2.1 Timed Automata -- 2.2 Learning Deterministic One-Clock Timed Automata -- 3 Framework for Learning-Based Compositional Verification of Timed Automata -- 3.1 Verification Framework via Assumption Learning -- 3.2 Model Conversion -- 3.3 Membership Queries -- 3.4 Candidate Queries -- 3.5 Correctness and Termination -- 4 Optimization Methods.
4.1 Using Additional Information -- 4.2 Minimizing the Alphabet of the Assumption -- 5 Experimental Results -- 6 Conclusion -- References -- Online Causation Monitoring of Signal Temporal Logic -- 1 Introduction -- 2 Preliminaries -- 2.1 Signal Temporal Logic -- 2.2 Classic Online Monitoring of STL -- 3 Boolean Causation Online Monitor -- 4 Quantitative Causation Online Monitor -- 5 Experimental Evaluation -- 5.1 Experiment Setting -- 5.2 Evaluation -- 6 Related Work -- 7 Conclusion and Future Work -- References -- Process Equivalence Problems as Energy Games -- 1 Introduction -- 2 Distinctions and Equivalences in Transition Systems -- 2.1 Transition Systems and Hennessy-Milner Logic -- 2.2 Price Spectra of Behavioral Equivalences -- 3 An Energy Game of Distinguishing Capabilities -- 3.1 Energy Games -- 3.2 The Spectroscopy Energy Game -- 3.3 Correctness: Tight Distinctions -- 3.4 Becoming More Clever by Looking One Step Ahead -- 4 Computing Equivalences -- 4.1 Computation of Attacker Winning Budgets -- 4.2 Complexity and How to Flatten It -- 4.3 Equivalences and Distinguishing Formulas from Budgets -- 5 Exploring Minimizations -- 6 Conclusion and Related Work -- References -- Concurrency -- Commutativity for Concurrent Program Termination Proofs -- 1 Introduction -- 2 Preliminaries -- 2.1 Concurrent Programs -- 2.2 Termination -- 2.3 Commutativity and Traces -- 3 Closures and Reductions -- 3.1 The Compromise: A New Proof Rule -- 3.2 Omega Prefix Generalization -- 4 Finite-Word Reductions -- 4.1 Efficient Reduction to Safety -- 4.2 Sound Finite Word Reductions -- 5 Omega Regular Reductions -- 6 Experimental Results -- 7 Related Work -- 8 Conclusion -- References -- Fast Termination and Workflow Nets -- 1 Introduction -- 2 Preliminaries -- 2.1 (Integer) Linear Programs -- 2.2 Petri Nets -- 2.3 Workflow Nets -- 2.4 Termination Complexity. 3 A Dichotomy of Termination Time in Workflow Nets -- 4 Refining Termination Time -- 5 Soundness in Terminating Workflow Nets -- 6 Termination Time and Concurrent Semantics -- 7 Experimental Evaluation -- 7.1 Benchmark Suite -- 7.2 Termination and Deadlocks -- 7.3 aN, MinTimeN(1) and MaxTimeN(1) -- 7.4 1-Soundness -- References -- Lincheck: A Practical Framework for Testing Concurrent Data Structures on JVM -- 1 Introduction -- 2 Lincheck Overview -- 2.1 Phase 1: Scenario Generation -- 2.2 Phase 2: Scenario Running -- 2.3 Phase 3: Verification of Outcome Results -- 3 Evaluation -- 4 Related Work -- 5 Discussion -- References -- nekton: A Linearizability Proof Checker -- 1 Introduction -- 2 Input -- 2.1 Proof Outlines -- 3 Case Study -- 4 Correctness and Implementation -- References -- Overcoming Memory Weakness with Unified Fairness -- 1 Introduction -- 2 Modelling Concurrent Programs -- 2.1 Labelled Transition Systems -- 2.2 Concurrent Programs -- 2.3 Concurrent Programs as Labelled Transition Systems -- 3 A Unified Framework for Weak Memory Models -- 3.1 Message Structures -- 3.2 Ensuring Consistency of Executions -- 3.3 Instantiating the Framework -- 4 Fairness Properties -- 4.1 Transition and Memory Fairness -- 4.2 Probabilistic Memory Fairness -- 4.3 Relating Fairness Notions -- 5 Applying Fairness Properties to Decision Problems -- 5.1 Deciding Repeated Control State Reachability -- 5.2 Quantitative Control State Repeated Reachability -- 5.3 Adapting Subroutines to Our Memory Framework -- 6 Related Work -- 7 Conclusion, Future Work, and Perspective -- References -- Rely-Guarantee Reasoning for Causally Consistent Shared Memory -- 1 Introduction -- 2 Motivating Example -- 3 Preliminaries: Syntax and Semantics -- 4 Generic Rely-Guarantee Reasoning -- 5 Potential-Based Memory System for SRA -- 6 Program Logic -- 7 Examples. 8 Discussion, Related and Future Work -- References -- Unblocking Dynamic Partial Order Reduction -- 1 Introduction -- 2 DPOR and Blocked Executions -- 2.1 Dynamic Partial Order Reduction -- 2.2 Assume Statements and DPOR -- 3 Key Ideas -- 3.1 Avoiding Blocking Due to Stale Reads -- 3.2 Handling Await Loops with In-Place Revisits -- 3.3 Handling Confirmation CASes with Speculative Revisits -- 4 Await-Aware Model Checking Algorithm -- 4.1 Execution Graphs -- 4.2 Awamoche -- 5 Correctness and Optimality -- 5.1 Approaches to Correctness -- 5.2 Awamoche: Completeness, Optimality, and Strong Optimality -- 6 Evaluation -- 6.1 Results -- 7 Related Work -- 8 Conclusion -- References -- Cyber-Physical and Hybrid Systems -- 3D Environment Modeling for Falsification and Beyond with Scenic 3.0 -- 1 Introduction -- 2 New Features -- 2.1 3D Geometry -- 2.2 Mesh Shapes and Regions -- 2.3 Precise Visibility Model -- 2.4 Temporal Requirements -- 2.5 Rewritten Parser -- 3 Case Studies -- 3.1 Falsification of a Robot Vacuum -- 3.2 Constrained Data Generation for an Autonomous Vehicle -- 4 Conclusion -- References -- A Unified Model for Real-Time Systems: Symbolic Techniques and Implementation -- 1 Introduction -- 2 Generalized timed automata -- 3 Expressivity of GTA and Examples -- 4 The Reachability Problem for GTA -- 5 Symbolic Enumeration -- 6 Computing with GTA Zones Using Distance Graphs -- 7 Finiteness of the Simulation Relation -- 8 Experimental Evaluation -- 9 Conclusion -- References -- Closed-Loop Analysis of Vision-Based Autonomous Systems: A Case Study -- 1 Introduction -- 2 Autonomous Center-Line Tracking with TaxiNet -- 3 Probabilistic Analysis -- 3.1 Probabilistic Abstractions for Perception -- 3.2 DNN Checks as Run-Time Guards -- 3.3 Confidence Analysis -- 4 Experiments -- 5 Conclusion -- References. Hybrid Controller Synthesis for Nonlinear Systems Subject to Reach-Avoid Constraints -- 1 Introduction -- 1.1 Related Works -- 2 Preliminaries -- 3 Hybrid Polynomial-DNN Controllers Training -- 3.1 Training Well-Performing DNN Controllers Using RL -- 3.2 Polynomial Approximation -- 3.3 Training the Residual Controller -- 4 Reach-Avoid Verification with Lyapunov-Like Functions and Barrier Certificates Generation -- 4.1 Constructing Polynomial Simulations of the Controller Network -- 4.2 Producing Barrier Certificate and Lyapunov-Like Function -- 5 Experiments -- 6 Conclusion -- References -- Safe Environmental Envelopes of Discrete Systems -- 1 Introduction -- 2 Motivating Example -- 3 Modeling Formalism -- 4 Robustness Against Environmental Deviations -- 4.1 Deviations -- 4.2 Comparing Deviations -- 4.3 Robustness -- 4.4 Problem Statement -- 4.5 Comparing Robustness -- 5 Computing Robustness -- 5.1 Brute-Force Algorithm -- 5.2 Controlling the Deviations Without Environmental Constraints -- 5.3 Controlling the Deviations with Environmental Constraints -- 6 Case Studies -- 6.1 Implementation -- 6.2 Therac-25 -- 6.3 Voting -- 6.4 Oyster -- 6.5 PCA Pump -- 6.6 Results and Discussion -- 7 Related Work -- 8 Conclusion -- References -- Verse: A Python Library for Reasoning About Multi-agent Hybrid System Scenarios -- 1 Introduction -- 2 Overview of Verse -- 3 Scenarios in Verse -- 4 Verse Scenario to Hybrid Verification -- 5 Experiments and Use Cases -- 6 Related Work -- 7 Conclusions and Future Directions -- References -- Synthesis -- Counterexample Guided Knowledge Compilation for Boolean Functional Synthesis -- 1 Introduction -- 2 A Motivating Example -- 3 Preliminaries and Notation -- 4 A New Knowledge Representation for Skolem Functions -- 5 Towards Synthesizing the Skolem Basis Vector -- 6 Counterexample-Guided Rectification. 7 Implementation and Experiments. |
| Record Nr. | UNISA-996542663503316 |
| Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2023 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Computer Aided Verification : 35th International Conference, CAV 2023, Paris, France, July 17–22, 2023, Proceedings, Part I / / edited by Constantin Enea, Akash Lal
| Computer Aided Verification : 35th International Conference, CAV 2023, Paris, France, July 17–22, 2023, Proceedings, Part I / / edited by Constantin Enea, Akash Lal |
| Edizione | [1st ed. 2023.] |
| Pubbl/distr/stampa | Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2023 |
| Descrizione fisica | 1 online resource (XXXI, 488 p. 160 illus., 121 illus. in color.) |
| Disciplina | 005.1 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Artificial intelligence Algorithms Computer engineering Computer networks Software Engineering Artificial Intelligence Design and Analysis of Algorithms Computer Engineering and Networks |
| ISBN | 3-031-37706-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Invited Talks -- Privacy-Preserving Automated Reasoning -- Enhancing Programming Experiences Using AI: Leveraging LLMs as Analogical Reasoning Engines and Beyond -- Verified Software Security Down to Gates -- Contents - Part I -- Contents - Part II -- Contents - Part III -- Automata and Logic -- Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization -- 1 Introduction -- 2 Preliminaries -- 2.1 Timed Words and Timed Automata -- 2.2 Recognizable Timed Languages -- 2.3 Distinguishing Extensions and Active DFA Learning -- 3 A Myhill-Nerode Style Characterization of Recognizable Timed Languages with Elementary Languages -- 4 Active Learning of Deterministic Timed Automata -- 4.1 Successors of Simple Elementary Languages -- 4.2 Timed Observation Table for Active DTA Learning -- 4.3 Counterexample Analysis -- 4.4 L*-Style Learning Algorithm for DTAs -- 4.5 Learning with a Normal Teacher -- 4.6 Complexity Analysis -- 5 Experiments -- 5.1 RQ1: Scalability with Respect to the Language Complexity -- 5.2 RQ2: Performance on Practical Benchmarks -- 6 Conclusions and Future Work -- References -- Automated Analyses of IOT Event Monitoring Systems -- 1 Introduction -- 2 Overview -- 3 Technique -- 3.1 Well-formedness Properties -- 4 Experiments -- 5 Conclusion -- A Common Issues with Detector Models -- References -- Learning Assumptions for Compositional Verification of Timed Automata -- 1 Introduction -- 2 Preliminaries -- 2.1 Timed Automata -- 2.2 Learning Deterministic One-Clock Timed Automata -- 3 Framework for Learning-Based Compositional Verification of Timed Automata -- 3.1 Verification Framework via Assumption Learning -- 3.2 Model Conversion -- 3.3 Membership Queries -- 3.4 Candidate Queries -- 3.5 Correctness and Termination -- 4 Optimization Methods.
4.1 Using Additional Information -- 4.2 Minimizing the Alphabet of the Assumption -- 5 Experimental Results -- 6 Conclusion -- References -- Online Causation Monitoring of Signal Temporal Logic -- 1 Introduction -- 2 Preliminaries -- 2.1 Signal Temporal Logic -- 2.2 Classic Online Monitoring of STL -- 3 Boolean Causation Online Monitor -- 4 Quantitative Causation Online Monitor -- 5 Experimental Evaluation -- 5.1 Experiment Setting -- 5.2 Evaluation -- 6 Related Work -- 7 Conclusion and Future Work -- References -- Process Equivalence Problems as Energy Games -- 1 Introduction -- 2 Distinctions and Equivalences in Transition Systems -- 2.1 Transition Systems and Hennessy-Milner Logic -- 2.2 Price Spectra of Behavioral Equivalences -- 3 An Energy Game of Distinguishing Capabilities -- 3.1 Energy Games -- 3.2 The Spectroscopy Energy Game -- 3.3 Correctness: Tight Distinctions -- 3.4 Becoming More Clever by Looking One Step Ahead -- 4 Computing Equivalences -- 4.1 Computation of Attacker Winning Budgets -- 4.2 Complexity and How to Flatten It -- 4.3 Equivalences and Distinguishing Formulas from Budgets -- 5 Exploring Minimizations -- 6 Conclusion and Related Work -- References -- Concurrency -- Commutativity for Concurrent Program Termination Proofs -- 1 Introduction -- 2 Preliminaries -- 2.1 Concurrent Programs -- 2.2 Termination -- 2.3 Commutativity and Traces -- 3 Closures and Reductions -- 3.1 The Compromise: A New Proof Rule -- 3.2 Omega Prefix Generalization -- 4 Finite-Word Reductions -- 4.1 Efficient Reduction to Safety -- 4.2 Sound Finite Word Reductions -- 5 Omega Regular Reductions -- 6 Experimental Results -- 7 Related Work -- 8 Conclusion -- References -- Fast Termination and Workflow Nets -- 1 Introduction -- 2 Preliminaries -- 2.1 (Integer) Linear Programs -- 2.2 Petri Nets -- 2.3 Workflow Nets -- 2.4 Termination Complexity. 3 A Dichotomy of Termination Time in Workflow Nets -- 4 Refining Termination Time -- 5 Soundness in Terminating Workflow Nets -- 6 Termination Time and Concurrent Semantics -- 7 Experimental Evaluation -- 7.1 Benchmark Suite -- 7.2 Termination and Deadlocks -- 7.3 aN, MinTimeN(1) and MaxTimeN(1) -- 7.4 1-Soundness -- References -- Lincheck: A Practical Framework for Testing Concurrent Data Structures on JVM -- 1 Introduction -- 2 Lincheck Overview -- 2.1 Phase 1: Scenario Generation -- 2.2 Phase 2: Scenario Running -- 2.3 Phase 3: Verification of Outcome Results -- 3 Evaluation -- 4 Related Work -- 5 Discussion -- References -- nekton: A Linearizability Proof Checker -- 1 Introduction -- 2 Input -- 2.1 Proof Outlines -- 3 Case Study -- 4 Correctness and Implementation -- References -- Overcoming Memory Weakness with Unified Fairness -- 1 Introduction -- 2 Modelling Concurrent Programs -- 2.1 Labelled Transition Systems -- 2.2 Concurrent Programs -- 2.3 Concurrent Programs as Labelled Transition Systems -- 3 A Unified Framework for Weak Memory Models -- 3.1 Message Structures -- 3.2 Ensuring Consistency of Executions -- 3.3 Instantiating the Framework -- 4 Fairness Properties -- 4.1 Transition and Memory Fairness -- 4.2 Probabilistic Memory Fairness -- 4.3 Relating Fairness Notions -- 5 Applying Fairness Properties to Decision Problems -- 5.1 Deciding Repeated Control State Reachability -- 5.2 Quantitative Control State Repeated Reachability -- 5.3 Adapting Subroutines to Our Memory Framework -- 6 Related Work -- 7 Conclusion, Future Work, and Perspective -- References -- Rely-Guarantee Reasoning for Causally Consistent Shared Memory -- 1 Introduction -- 2 Motivating Example -- 3 Preliminaries: Syntax and Semantics -- 4 Generic Rely-Guarantee Reasoning -- 5 Potential-Based Memory System for SRA -- 6 Program Logic -- 7 Examples. 8 Discussion, Related and Future Work -- References -- Unblocking Dynamic Partial Order Reduction -- 1 Introduction -- 2 DPOR and Blocked Executions -- 2.1 Dynamic Partial Order Reduction -- 2.2 Assume Statements and DPOR -- 3 Key Ideas -- 3.1 Avoiding Blocking Due to Stale Reads -- 3.2 Handling Await Loops with In-Place Revisits -- 3.3 Handling Confirmation CASes with Speculative Revisits -- 4 Await-Aware Model Checking Algorithm -- 4.1 Execution Graphs -- 4.2 Awamoche -- 5 Correctness and Optimality -- 5.1 Approaches to Correctness -- 5.2 Awamoche: Completeness, Optimality, and Strong Optimality -- 6 Evaluation -- 6.1 Results -- 7 Related Work -- 8 Conclusion -- References -- Cyber-Physical and Hybrid Systems -- 3D Environment Modeling for Falsification and Beyond with Scenic 3.0 -- 1 Introduction -- 2 New Features -- 2.1 3D Geometry -- 2.2 Mesh Shapes and Regions -- 2.3 Precise Visibility Model -- 2.4 Temporal Requirements -- 2.5 Rewritten Parser -- 3 Case Studies -- 3.1 Falsification of a Robot Vacuum -- 3.2 Constrained Data Generation for an Autonomous Vehicle -- 4 Conclusion -- References -- A Unified Model for Real-Time Systems: Symbolic Techniques and Implementation -- 1 Introduction -- 2 Generalized timed automata -- 3 Expressivity of GTA and Examples -- 4 The Reachability Problem for GTA -- 5 Symbolic Enumeration -- 6 Computing with GTA Zones Using Distance Graphs -- 7 Finiteness of the Simulation Relation -- 8 Experimental Evaluation -- 9 Conclusion -- References -- Closed-Loop Analysis of Vision-Based Autonomous Systems: A Case Study -- 1 Introduction -- 2 Autonomous Center-Line Tracking with TaxiNet -- 3 Probabilistic Analysis -- 3.1 Probabilistic Abstractions for Perception -- 3.2 DNN Checks as Run-Time Guards -- 3.3 Confidence Analysis -- 4 Experiments -- 5 Conclusion -- References. Hybrid Controller Synthesis for Nonlinear Systems Subject to Reach-Avoid Constraints -- 1 Introduction -- 1.1 Related Works -- 2 Preliminaries -- 3 Hybrid Polynomial-DNN Controllers Training -- 3.1 Training Well-Performing DNN Controllers Using RL -- 3.2 Polynomial Approximation -- 3.3 Training the Residual Controller -- 4 Reach-Avoid Verification with Lyapunov-Like Functions and Barrier Certificates Generation -- 4.1 Constructing Polynomial Simulations of the Controller Network -- 4.2 Producing Barrier Certificate and Lyapunov-Like Function -- 5 Experiments -- 6 Conclusion -- References -- Safe Environmental Envelopes of Discrete Systems -- 1 Introduction -- 2 Motivating Example -- 3 Modeling Formalism -- 4 Robustness Against Environmental Deviations -- 4.1 Deviations -- 4.2 Comparing Deviations -- 4.3 Robustness -- 4.4 Problem Statement -- 4.5 Comparing Robustness -- 5 Computing Robustness -- 5.1 Brute-Force Algorithm -- 5.2 Controlling the Deviations Without Environmental Constraints -- 5.3 Controlling the Deviations with Environmental Constraints -- 6 Case Studies -- 6.1 Implementation -- 6.2 Therac-25 -- 6.3 Voting -- 6.4 Oyster -- 6.5 PCA Pump -- 6.6 Results and Discussion -- 7 Related Work -- 8 Conclusion -- References -- Verse: A Python Library for Reasoning About Multi-agent Hybrid System Scenarios -- 1 Introduction -- 2 Overview of Verse -- 3 Scenarios in Verse -- 4 Verse Scenario to Hybrid Verification -- 5 Experiments and Use Cases -- 6 Related Work -- 7 Conclusions and Future Directions -- References -- Synthesis -- Counterexample Guided Knowledge Compilation for Boolean Functional Synthesis -- 1 Introduction -- 2 A Motivating Example -- 3 Preliminaries and Notation -- 4 A New Knowledge Representation for Skolem Functions -- 5 Towards Synthesizing the Skolem Basis Vector -- 6 Counterexample-Guided Rectification. 7 Implementation and Experiments. |
| Record Nr. | UNINA-9910734886603321 |
| Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2023 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Computer Aided Verification : 35th International Conference, CAV 2023, Paris, France, July 17–22, 2023, Proceedings, Part III / / edited by Constantin Enea, Akash Lal
| Computer Aided Verification : 35th International Conference, CAV 2023, Paris, France, July 17–22, 2023, Proceedings, Part III / / edited by Constantin Enea, Akash Lal |
| Edizione | [1st ed. 2023.] |
| Pubbl/distr/stampa | Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2023 |
| Descrizione fisica | 1 online resource (XVII, 502 p. 140 illus., 88 illus. in color.) |
| Disciplina | 005.1 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Artificial intelligence Algorithms Computer engineering Computer networks Software Engineering Artificial Intelligence Design and Analysis of Algorithms Computer Engineering and Networks |
| ISBN | 3-031-37709-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Contents - Part III -- Probabilistic Systems -- A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties -- 1 Introduction -- 2 Theoretical Background -- 2.1 Solving Rabin Games Symbolically -- 2.2 Computing Symbolic Controllers for Stochastic Dynamical Systems -- 3 Implementation Details -- 3.1 Genie -- 3.2 FairSyn -- 3.3 Mascot-SDS -- 4 Examples -- 4.1 Synthesizing Code-Aware Resource Mangers Using FairSyn -- 4.2 Synthesizing Controllers for Stochastic Dynamical Systems Using Mascot-SDS -- References -- Automated Tail Bound Analysis for Probabilistic Recurrence Relations -- 1 Introduction -- 2 Preliminaries -- 2.1 Probabilistic Recurrence Relations -- 3 Exponential Tail Bounds via Markov's Inequality -- 4 An Algorithmic Approach -- 4.1 The Guess Procedure Guess(f,t) -- 4.2 The Check Procedure CheckCond(cf,ct) -- 5 Experimental Results -- 6 Related Work -- References -- Compositional Probabilistic Model Checking with String Diagrams of MDPs -- 1 Introduction -- 2 String Diagrams of MDPs -- 2.1 Outline -- 2.2 Open MDPs -- 2.3 Rightward Open MDPs and Traced Monoidal String Diagrams -- 2.4 TSMC Equations Between roMDPs -- 2.5 Open MDPs and ``Compact Closed'' String Diagrams -- 3 Decomposition Equalities for Open Markov Chains -- 4 Semantic Categories and Solution Functors -- 4.1 Semantic Category for Rightward Open MCs -- 4.2 Semantic Category of Rightward Open MDPs -- 4.3 Semantic Category of MDPs -- 5 Implementation and Experiments -- References -- Efficient Sensitivity Analysis for Parametric Robust Markov Chains -- 1 Introduction -- 2 Overview -- 3 Formal Problem Statement -- 4 Differentiating Solution Functions for pMCs -- 4.1 Computing Derivatives Explicitly -- 4.2 Computing k-Highest Derivatives -- 5 Differentiating Solution Functions for prMCs.
5.1 Computing Derivatives via pMCs (and When It Does Not Work) -- 5.2 Computing Derivatives Explicitly -- 5.3 Computing k-Highest Derivatives -- 6 Numerical Experiments -- 7 Related Work -- 8 Concluding Remarks -- References -- MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives -- 1 Introduction -- 1.1 Related Work -- 2 Preliminaries -- 2.1 Markov Systems -- 2.2 MDPs as Distribution Transformers -- 3 Problem Statement and Examples -- 4 Proving Safety by Invariants -- 4.1 Distribution Strategies -- 4.2 Distributional Invariants for MDP Safety -- 5 Algorithms for Distributional Invariant Synthesis -- 5.1 Synthesis of Affine Invariants and Memoryless Strategies -- 5.2 Synthesis of Affine Invariants and General Strategies -- 6 Discussion, Extensions, and Variants -- 7 Implementation and Evaluation -- 8 Conclusion -- References -- Search and Explore: Symbiotic Policy Synthesis in POMDPs -- 1 Introduction -- 2 Motivating Examples -- 3 Preliminaries and Problem Statement -- 4 FSCs for and from Belief Exploration -- 4.1 Belief Exploration with Explicit FSC Construction -- 4.2 Using FSCs for Cut-Off Values -- 4.3 Extracting FSC from Belief Exploration -- 5 Accelerated Inductive Synthesis -- 5.1 Inductive Synthesis with k-FSCs -- 5.2 Using Reference Policies to Accelerate Inductive Synthesis -- 5.3 Inductive Synthesis with Adequate FSCs -- 6 Integrating Belief Exploration with Inductive Synthesis -- 7 Experiments -- 8 Conclusion and Future Work -- References -- Security and Quantum Systems -- AutoQ: An Automata-Based Quantum Circuit Verifier -- 1 Introduction -- 2 Tree Automata-Based Verification of Quantum Circuits -- 2.1 High-Level Specification Language -- 2.2 Complex Number Representation -- 2.3 Precise Semantics of the Specification -- 3 Entailment Checking -- 4 Architecture -- 5 Use Cases. 5.1 Hadamard Square is Identity -- 5.2 Zero Imaginary Part of Amplitudes -- 5.3 Probability of Measuring the Correct Answer -- 5.4 Increasing Amplitude of the Correct Answer -- 6 Conclusion -- References -- Bounded Verification for Finite-Field-Blasting -- 1 Introduction -- 1.1 Related Work -- 2 Background -- 2.1 Logic -- 2.2 Zero Knowledge Proofs -- 2.3 Compilation Targeting Zero Knowledge Proofs -- 3 Overview and Example -- 3.1 An Example of Field-Blasting -- 3.2 Key Ideas -- 4 Architecture -- 4.1 Encodings -- 4.2 Encoding Rules -- 4.3 Calculus -- 5 Verification Conditions -- 5.1 Correctness Definition -- 5.2 Rule VCs -- 5.3 A Correct Field-Blasting Calculus -- 6 Case Study: A Verifiable Field-Blaster for CirC -- 6.1 Verification Evaluation -- 6.2 Performance and Output Quality Evaluation -- 7 Discussion -- A Zero-Knowledge Proofs and Compilers -- B Compiler Correctness Proofs -- C CirC-IR -- D Optimizations to the CirC Field-Blaster -- E Verified Field-Blaster Performance Details -- F Verifier Performance Details -- G Bugs Found in the CirC Field Blaster -- References -- Formally Verified EVM Block-Optimizations -- 1 Introduction -- 2 Background -- 3 EVM Semantics in Coq -- 4 Formal Verification of EVM-Optimizations in Coq -- 4.1 EVM Symbolic Execution in Coq -- 4.2 Simplification Rules -- 4.3 Stacks Equivalence Modulo Commutativity -- 5 Implementation and Experimental Evaluation -- 6 Conclusions, Related and Future Work -- References -- SR-SFLL: Structurally Robust Stripped Functionality Logic Locking -- 1 Introduction -- 2 Background -- 2.1 Stripped Functionality Logic Locking (SFLL) -- 2.2 SFLL Attacks -- 2.3 Analysis of the Structural Attacks on SFLL -- 3 Overview -- 3.1 Preliminaries -- 3.2 Approach -- 4 SR-SFLL -- 4.1 Problem Statement -- 4.2 Intuition: SR-SFLL -- 4.3 Methodology: SR-SFLL -- 5 SyntAk -- 6 Evaluation. 6.1 Robustness of SR-SELL(0) and SR-SELL on Existing Attacks -- 6.2 Robustness of SR-SELL(0) and SR-SELL on SyntAk -- 6.3 Overhead of SR-SELL(0) and SR-SELL -- 7 Related Work -- 8 Conclusions -- References -- Symbolic Quantum Simulation with Quasimodo -- 1 Introduction -- 2 Background on Quantum Simulation -- 3 Quasimodo's Programming and Analysis Interface -- 3.1 Extending Quasimodo -- 4 The Internals of Quasimodo -- 5 Experiments -- 6 Conclusion -- References -- Verifying the Verifier: eBPF Range Analysis Verification -- 1 Introduction -- 2 Background on Abstract Interpretation -- 3 Abstract Interpretation in the Linux Kernel -- 4 Automatic Verification of the Kernel's Algorithms -- 4.1 Soundness Specification for Abstraction/Reduction Operators -- 4.2 Refining Soundness Specification with Input Preconditioning -- 4.3 Automatically Producing Programs Exercising Soundness Bugs -- 5 C to Logic for Kernel's Abstract Operators -- 6 Experimental Evaluation -- 7 Limitations and Caveats -- 8 Related Work -- 9 Conclusion -- References -- Software Verification -- Automated Verification of Correctness for Masked Arithmetic Programs -- 1 Introduction -- 2 Preliminaries -- 3 The Core Language -- 4 Overview of the Approach -- 4.1 Our Approach -- 5 Term Rewriting System -- 6 Algorithmic Verification -- 6.1 Term Normalization Algorithm -- 6.2 Computing Affine Constants -- 6.3 Verification Algorithm -- 6.4 Implementation Remarks -- 7 Evaluation -- 7.1 Evaluation for Computing Affine Constants -- 7.2 Evaluation for Correctness Verification -- 7.3 Scalability of FISCHER -- 7.4 Evaluation for More Boolean Masking Schemes -- 7.5 Evaluation for Arithmetic/Boolean Masking Conversions -- 8 Conclusion -- References -- Automatic Program Instrumentation for Automatic Verification -- 1 Introduction -- 2 Instrumentation Framework -- 2.1 The Core Language. 2.2 Instrumentation Operators -- 2.3 Instrumentation Correctness -- 3 Instrumentation Application Strategies -- 4 Instrumentation Operators for Arrays -- 4.1 Instrumentation Operators for Quantification over Arrays -- 4.2 Instrumentation Operators for Aggregation over Arrays -- 5 Evaluation -- 5.1 Implementation -- 5.2 Experiments and Comparisons -- 6 Related Work -- 7 Conclusion -- References -- Boolean Abstractions for Realizability Modulo Theories -- 1 Introduction -- 2 Preliminaries -- 3 Boolean Abstraction -- 3.1 Notation -- 3.2 The Boolean Abstraction Algorithm -- 3.3 From Local Simulation to Equi-Realizability -- 4 Efficient Algorithms for Boolean Abstraction -- 4.1 Quasi-reactions -- 4.2 Quasi-reaction-based Optimizations -- 4.3 A Single Model-Loop Algorithm (Algorithm 2) -- 4.4 A Nested-SAT Algorithm (Algorithm 3) -- 5 Empirical Evaluation -- 6 Related Work and Conclusions -- References -- Certified Verification for Algebraic Abstraction -- 1 Introduction -- 2 Preliminaries -- 3 ToyLang -- 3.1 Syntax and Semantics -- 4 Algebraic Abstraction -- 4.1 Soundness Conditions -- 4.2 Polynomial Program Verification -- 5 Certified Verification -- 5.1 Verified Abstraction Algorithm -- 5.2 Verification through Certification -- 5.3 Optimization -- 6 Evaluation -- 6.1 Field and Group Operation in Elliptic Curves -- 6.2 Number-Theoretic Transform in Kyber -- 7 Conclusion -- References -- Complete Multiparty Session Type Projection with Automata -- 1 Introduction -- 2 Motivation and Overview -- 3 Preliminaries -- 4 Synthesizing Implementations -- 5 Checking Implementability -- 6 Soundness -- 7 Completeness -- 8 Complexity -- 9 Evaluation -- 10 Discussion -- 11 Related Work -- References -- Early Verification of Legal Compliance via Bounded Satisfiability Checking -- 1 Introduction -- 2 Preliminaries -- 3 Bounded Satisfiability Checking Problem. 4 Checking Bounded Satisfiability. |
| Record Nr. | UNINA-9910734891603321 |
| Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2023 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Networked Systems : 12th International Conference, NETYS 2024, Rabat, Morocco, May 29–31, 2024, Proceedings / / edited by Armando Castañeda, Constantin Enea, Nirupam Gupta
| Networked Systems : 12th International Conference, NETYS 2024, Rabat, Morocco, May 29–31, 2024, Proceedings / / edited by Armando Castañeda, Constantin Enea, Nirupam Gupta |
| Autore | Castañeda Armando |
| Edizione | [1st ed. 2024.] |
| Pubbl/distr/stampa | Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2024 |
| Descrizione fisica | 1 online resource (276 pages) |
| Disciplina | 004.6 |
| Altri autori (Persone) |
EneaConstantin
GuptaNirupam |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer networks
Computer Communication Networks |
| ISBN | 3-031-67321-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | -- Sharding in permissionless systems in presence of an adaptive adversary. -- Concurrent Wait-Free Graph Snapshots using Multi-Versioning. -- Blockchain based Massively Multiplayer Online Game Architecture. -- Agent-Driven BFS Tree in Anonymous Graphs with Applications. -- Some new results with k-set agreement. -- A Domain Specific Language for Testing Distributed Protocol Implementations. -- Tool Augmented LLMs for Big Data Analysis. -- Static Data Race Detection via Lazy Sequentialization. -- Algebraic Computations in Anonymous VANET. -- Federated Learning for Enhanced Medical Image Analysis. -- Towards Stronger Blockchains: Security Against Front-Running Attacks. -- Distributed Station Assignment through Learning. -- An Efficient Framework for supporting Nested Transaction in STMs. -- Enhancing Cost and Latency Efficiency through Service Placement in Containerized Fog-Cloud Computing Environments. -- Towards Generating a Dataset for Failure Prediction in Microservices Applications. -- Dynamic Resource Allocation for 5G Device-to-Device Communication Based on Expected SARSA. -- BeRGeR: Byzantine-Robust Geometric Routing. |
| Record Nr. | UNINA-9910882886803321 |
Castañeda Armando
|
||
| Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2024 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Verification, Model Checking, and Abstract Interpretation [[electronic resource] ] : 20th International Conference, VMCAI 2019, Cascais, Portugal, January 13–15, 2019, Proceedings / / edited by Constantin Enea, Ruzica Piskac
| Verification, Model Checking, and Abstract Interpretation [[electronic resource] ] : 20th International Conference, VMCAI 2019, Cascais, Portugal, January 13–15, 2019, Proceedings / / edited by Constantin Enea, Ruzica Piskac |
| Edizione | [1st ed. 2019.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
| Descrizione fisica | 1 online resource (XVII, 602 p. 1329 illus., 69 illus. in color.) |
| Disciplina | 005.14 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Computer networks Computer Science Logic and Foundations of Programming Software Engineering Computer Communication Networks |
| ISBN | 3-030-11245-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Program verification -- Model checking -- Abstract interpretation -- Program synthesis -- Static analysis -- Type systems -- Deductive methods -- Program certification -- Decision procedures -- Theorem proving -- Program certification -- Debugging techniques -- Program transformation -- Optimization -- Hybrid and cyber-physical systems. |
| Record Nr. | UNISA-996466455303316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Verification, Model Checking, and Abstract Interpretation : 20th International Conference, VMCAI 2019, Cascais, Portugal, January 13–15, 2019, Proceedings / / edited by Constantin Enea, Ruzica Piskac
| Verification, Model Checking, and Abstract Interpretation : 20th International Conference, VMCAI 2019, Cascais, Portugal, January 13–15, 2019, Proceedings / / edited by Constantin Enea, Ruzica Piskac |
| Edizione | [1st ed. 2019.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
| Descrizione fisica | 1 online resource (XVII, 602 p. 1329 illus., 69 illus. in color.) |
| Disciplina | 005.14 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Computer networks Computer Science Logic and Foundations of Programming Software Engineering Computer Communication Networks |
| ISBN | 3-030-11245-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Program verification -- Model checking -- Abstract interpretation -- Program synthesis -- Static analysis -- Type systems -- Deductive methods -- Program certification -- Decision procedures -- Theorem proving -- Program certification -- Debugging techniques -- Program transformation -- Optimization -- Hybrid and cyber-physical systems. |
| Record Nr. | UNINA-9910337565903321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||