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 : 20th International Symposium, ATVA 2022, Beijing, China, October 25-28, 2022, proceedings / / edited by Ahmed Bouajjani, Lukás Holík, and Zhilin Wu
| Automated technology for verification and analysis : 20th International Symposium, ATVA 2022, Beijing, China, October 25-28, 2022, proceedings / / edited by Ahmed Bouajjani, Lukás Holík, and Zhilin Wu |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2022] |
| Descrizione fisica | 1 online resource (442 pages) |
| Disciplina | 511.3 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico | Automatic theorem proving |
| ISBN | 3-031-19992-8 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Abstracts of Invited Talks -- Compositional Reasoning about Concurrent Randomized Programs (Extended Abstract) -- Flattening String Constraints -- Runtime Assurance for Verified AI-Based Autonomy -- The Civl Verifier -- Subgame Perfect Equilibrium with an Algorithmic Perspective -- Contents -- Invited Paper -- Learning Monitorable Operational Design Domains for Assured Autonomy -- 1 Introduction -- 2 Motivating Example: Autonomous Lane Keeping -- 3 Optimal Monitors for Operational Design Domains -- 3.1 Learning Monitors for ODDs -- 3.2 Challenges in Learning Monitorable ODDs -- 3.3 Quantitative Monitor Learning -- 3.4 Black-Box vs. White-Box Settings -- 4 Framework -- 4.1 Main Workflow -- 4.2 Simulation-Based Analysis Using VerifAI and Scenic -- 4.3 Data Generation -- 4.4 Conformance Testing -- 5 Experiments -- 5.1 Experimental Setup -- 5.2 Results -- 6 Related Work -- 7 Conclusion -- References -- Reinforcement Learning -- Dynamic Shielding for Reinforcement Learning in Black-Box Environments -- 1 Introduction -- 1.1 Related Works -- 2 Preliminaries -- 2.1 Automata and Games for System Modeling -- 2.2 Safety Automata for Specifications -- 2.3 Shielding for Safe Reinforcement Learning -- 2.4 The RPNI Algorithm for Passive Automata Learning -- 3 Dynamic Shielding with Online Automata Inference -- 3.1 Dynamic Shielding Scheme -- 3.2 Challenge 1: Incompleteness of the Learned FSRS -- 3.3 Challenge 2: Precision in Automata Learning -- 3.4 Theoretical Validity of Our Dynamic Shielding -- 4 Experimental Evaluation -- 4.1 Implementation and Experiments -- 4.2 Benchmarks -- 4.3 RQ1: Safety by Dynamic Shielding in the Training Phase -- 4.4 RQ2: Performance of the Resulting Controller -- 4.5 RQ3: Time Efficiency of Dynamic Shielding -- 5 Conclusions and Perspectives -- References.
An Impossibility Result in Automata-Theoretic Reinforcement Learning -- 1 Introduction -- 2 Omega-Automata -- 3 Closure Properties of Acceptance Conditions -- 4 Markov Decision Processes -- 4.1 Optimal Strategies Against Omega-Automata -- 4.2 Optimal Strategies Against Scalar Rewards -- 5 Memoryless Reward Translations for RL -- 5.1 Memoryless Reward Translation -- 5.2 Conditions for Memoryless Reductions -- 6 Conclusion -- References -- Reusable Contracts for Safe Integration of Reinforcement Learning in Hybrid Systems -- 1 Introduction -- 2 Preliminaries -- 2.1 Reinforcement Learning -- 2.2 Simulink and the RL Toolbox -- 2.3 Deductive Verification with the Differential Dynamic Logic -- 2.4 Transformation from Simulink to dL -- 3 Related Work -- 4 Reusable Hybrid Contracts -- 4.1 Illustrating Examples -- 4.2 Recurring Elements -- 4.3 Threshold Pattern -- 4.4 Range Pattern -- 4.5 Range Recovery Pattern -- 4.6 Resilience Contracts -- 4.7 Deductive Verification in KeYmaera X -- 5 Conclusion -- References -- Program Analysis and Verification -- SISL: Concolic Testing of Structured Binary Input Formats via Partial Specification -- 1 Introduction -- 2 Scheme-Based Input Specification Language -- 3 Overview and Implementation -- 4 Experiments and Conclusion -- References -- Fence Synthesis Under the C11 Memory Model -- 1 Introduction -- 2 Overview of FenSying and fFenSying -- 3 Preliminaries -- 4 Background: C11 Memory Model -- 5 Invalidating Buggy Traces with C11 Fences -- 6 Methodology -- 7 Implementation and Results -- 8 Related Work -- 9 Conclusion and Future Work -- References -- Checking Scheduling-Induced Violations of Control Safety Properties -- 1 Introduction -- 2 System Model and Encoding -- 2.1 Control System Model and Evolution -- 2.2 Task Specification -- 2.3 An Abstraction for Task Runs -- 2.4 Control Action Update Modeling. 2.5 Composing Control and Scheduling Models -- 3 Refining the Abstraction -- 3.1 Overlapping Jobs -- 3.2 Schedule Violation -- 3.3 Work Conservation Violation -- 3.4 Unconstrained Control Updates -- 3.5 Correctness of Refinement -- 4 Tool Design -- 5 Case Study 1: DC Motor Control Model -- 6 Case Study 2: RC Network Control Model -- 7 Case Study 3: F1Tenth Car Model -- 8 Conclusions and Future Work -- References -- Symbolic Runtime Verification for Monitoring Under Uncertainties and Assumptions -- 1 Introduction -- 2 Preliminaries -- 3 A Framework for Symbolic Runtime Verification -- 3.1 Symbolic Expressions -- 3.2 Symbolic Monitor Semantics -- 3.3 A Symbolic Runtime Verification Algorithm -- 4 Symbolic Runtime Verification at Work -- 4.1 Application to Lola Fragments -- 4.2 Temporal Assumptions -- 5 Implementation and Empirical Evaluation -- 6 Conclusion -- References -- SMT and Verification -- Handling Polynomial and Transcendental Functions in SMT via Unconstrained Optimisation and Topological Degree Test -- 1 Introduction -- 2 Background -- 2.1 Unconstrained Global Optimisation -- 2.2 Interval Arithmetic -- 2.3 Robustness and Quasi-decidability -- 2.4 Topological Degree Test -- 3 Local Search Using Unconstrained Global Optimisation -- 4 Solving Bounded Instances with the Topological Degree Test and Interval Arithmetic -- 4.1 Quasi-decidability Procedure -- 4.2 From a Formula with nm to Quasi-dec -- 4.3 A General Procedure -- 5 From Constraint Sets to Formulas -- 5.1 An Eager Approach -- 5.2 A Lazy Approach -- 6 Experimental Evaluation -- 7 Conclusions and Future Work -- References -- Verification of SMT Systems with Quantifiers -- 1 Introduction -- 2 Preliminaries -- 3 Verification of Quantified SMT Systems -- 3.1 Symbolic Formalism -- 3.2 Overview -- 3.3 Ground Instances -- 3.4 Generalizing Invariants from Instances -- 3.5 Invariant Checking. 3.6 Termination -- 4 Related Work -- 5 Experimental Evaluation -- 6 Conclusions and Future Work -- References -- Projected Model Counting: Beyond Independent Support -- 1 Introduction -- 2 Notation and Preliminaries -- 3 Related Work -- 4 Technical Contribution -- 4.1 Extremal Properties of GIS and UBS -- 4.2 Algorithm to Compute Projected Count Using UBS -- 5 Experimental Evaluation -- 6 Conclusion -- References -- Automata and Applications -- Minimization of Automata for Liveness Languages -- 1 Introduction -- 2 Preliminaries -- 2.1 Automata -- 2.2 Liveness Languages -- 2.3 Graphs, Nice Graphs, and the Vertex-Cover Problem -- 3 Live1 Languages -- 3.1 Minimizing Automata for Live1 and Doom1 Languages -- 4 Live2 Languages -- 4.1 Minimizing DBWs and GFG-NBWs for Live2 Languages -- 4.2 Minimizing DCWs and GFG-NCWs for Doom2 Languages -- 4.3 Minimizing Automata with Transition-Based Acceptance for Live2 Languages -- 5 Live3 Languages -- References -- Temporal Causality in Reactive Systems -- 1 Introduction -- 2 Preliminaries -- 3 Motivating Example -- 4 Property Causality -- 4.1 Interventions -- 4.2 Contingencies -- 4.3 Actual Causality for Trace Properties -- 5 Checking -Regular Causality -- 5.1 Interventions -- 5.2 Contingencies -- 5.3 Minimality -- 5.4 Deciding -Regular Causality -- 6 Related Work -- 7 Conclusion -- References -- PDAAAL: A Library for Reachability Analysis of Weighted Pushdown Systems -- 1 Introduction -- 2 Weighted Pushdown Systems and Reachability -- 3 Implemented Algorithms and PDAAAL Architecture -- 4 Comparison with State-of-the-Art -- 5 Applications -- 6 Conclusion -- References -- Active Learning -- Learning Deterministic One-Clock Timed Automata via Mutation Testing -- 1 Introduction -- 2 Preliminaries -- 2.1 Deterministic One-Clock Timed Automata -- 2.2 Active Learning Algorithm for DOTAs -- 2.3 Model-Based Mutation Testing. 3 Mutation-Based Testing for DOTAs -- 3.1 The Process Overview -- 3.2 Heuristic Test-Case Generation -- 3.3 Mutation and Score-Based Test-Case Selection -- 4 Learning-Friendly Mutation Operators for DOTAs -- 4.1 Timed Mutation Operator -- 4.2 Split-Location Mutation Operator -- 5 Implementation and Experiments -- 5.1 Case Studies -- 5.2 Evaluation of Improvements -- 6 Conclusion -- References -- Active Learning of One-Clock Timed Automata Using Constraint Solving -- 1 Introduction -- 2 Preliminaries -- 3 Learning Algorithm -- 3.1 Alignment and Comparison of Timed Words -- 3.2 Timed Observation Table -- 3.3 Encoding of Readiness Constraints -- 3.4 Hypothesis Construction -- 3.5 Main Algorithm and Correctness -- 4 Extension to Deterministic Timed Mealy Machines -- 5 Implementation and Experiments -- 5.1 Experiments on DOTAs -- 5.2 Experiments on TMMs -- 6 Conclusion -- References -- Learning and Characterizing Fully-Ordered Lattice Automata -- 1 Introduction -- 2 Preliminaries -- 3 A Myhill-Nerode Characterization for FOLAs -- 3.1 No Unique Minimal FOLA -- 3.2 Difficulties in Defining f -- 3.3 Defining the Equivalence Relation -- 3.4 The Correspondence Between f and a Minimal FOLA -- 4 The Learning Algorithm -- 5 Empirical Results -- 6 Conclusions -- References -- Probabilistic and Stochastic Systems -- Optimistic and Topological Value Iteration for Simple Stochastic Games -- 1 Introduction -- 2 Preliminaries -- 2.1 Simple Stochastic Games -- 2.2 Value Iteration and Bounded Value Iteration -- 3 Optimistic Value Iteration -- 4 Precise Topological Value Iteration -- 5 Random Generation of Simple Stochastic Games -- 6 Experiments -- 6.1 Experimental Setup -- 6.2 Overview -- 6.3 Detailed Analysis of Precise Algorithms -- 6.4 Detailed Analysis of Approximate (-Precise) Algorithms -- 7 Conclusion -- References -- Alternating Good-for-MDPs Automata. 1 Introduction. |
| Record Nr. | UNISA-996495567803316 |
| Cham, Switzerland : , : Springer, , [2022] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated Technology for Verification and Analysis : 20th International Symposium, ATVA 2022, Virtual Event, October 25–28, 2022, Proceedings / / edited by Ahmed Bouajjani, Lukáš Holík, Zhilin Wu
| Automated Technology for Verification and Analysis : 20th International Symposium, ATVA 2022, Virtual Event, October 25–28, 2022, Proceedings / / edited by Ahmed Bouajjani, Lukáš Holík, Zhilin Wu |
| Edizione | [1st ed. 2022.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2022 |
| Descrizione fisica | 1 online resource (442 pages) |
| Disciplina | 511.3 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Computer engineering Computer networks Computers Computer science Artificial intelligence Software Engineering Computer Engineering and Networks Computer Hardware Theory of Computation Artificial Intelligence |
| ISBN |
9783031199929
3031199928 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Paper -- Learning Monitorable Operational Design Domains for Assured Autonomy -- Reinforcement Learning -- Dynamic Shielding for Reinforcement Learning in Black-Box Environments -- An Impossibility Result in Automata-Theoretic Reinforcement Learning -- Reusable Contracts for Safe Integration of Reinforcement Learning in Hybrid Systems -- Program Analysis and Verification -- SISL: Concolic Testing of Structured Binary Input Formats via Partial Specification -- Fence Synthesis under the C11 Memory Model -- Checking Scheduling-induced Violations of Control Safety Properties -- Symbolic Runtime Verification for Monitoring under Uncertainties and Assumptions -- SMT and Verification -- Handling Polynomial and Transcendental Functions in SMT via Unconstrained Optimisation and Topological Degree Test -- Verification of SMT Systems with Quantifiers -- Projected Model Counting: Beyond Independent Support -- Automata and Applications -- Minimization of Automata for Liveness Languages -- Temporal Causality in Reactive Systems -- PDAAAL: A Library for Reachability Analysis of Weighted Pushdown Systems -- Active Learning -- Learning Deterministic One-Clock Timed Automata via Mutation Testing -- Active Learning of One-Clock Timed Automata using Constraint Solving -- Learning and Characterizing Fully-Ordered Lattice Automata -- Probabilistic and Stochastic Systems -- Optimistic and Topological Value Iteration for Simple Stochastic Games -- Alternating Good-for-MDPs Automata -- PET - A Partial Exploration Tool for Probabilistic Verification -- STOMPC: Stochastic Model-Predictive Control with Uppaal Stratego -- Synthesis and Repair -- Synthesis of Parametric Hybrid Automata from Time Series -- Optimal Repair For Omega-regular Properties -- Repairing Real-Time Requirements -- Verification of Neural Networks -- An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks -- Prioritizing Corners in OoD Detectors via Symbolic String Manipulation -- POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems. |
| Record Nr. | UNINA-9910620200703321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2022 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Microwave Chemistry / / Giancarlo Cravotto, Diego Carnaroglio
| Microwave Chemistry / / Giancarlo Cravotto, Diego Carnaroglio |
| Pubbl/distr/stampa | Berlin ; ; Boston : , : De Gruyter, , [2017] |
| Descrizione fisica | 1 online resource (530 pages) : illustrations (some color), photographs |
| Disciplina | 541/.38 |
| Altri autori (Persone) |
BarinJuliano S
BizziCezar Augusto BogdalDariusz ChematFarid CintasPedro; Veronesi, Paolo; Leonelli, Cristina; Keglevich, György; Mucsi, Zoltán; Radoiu, Marilena; de la Hoz, Antonio; Prieto, Pilar; Wada, Yuji; Mochizuki, Dai; Ano, Taishi; Maitani, Masato M.; Tsubaki, Shuntaro; Haneishi, Naoto; Horikoshi, Satoshi; Serpone, Nick; Delbecq, Frédéric; Luque, Rafael; Len, Christophe; Díaz-Ortiz, Angél; Sharma, Abhishek; van der Eycken, Erick; Wojnarowicz, Jacek; Chudoba, Tadeusz; Majcher, Andrzej; Łojkowski, Witold; González-Prieto, Rodrigo CoimbraManuel CollinaSimona Della VolpeSerena DuarteFabio A EngenKarin FloresÉrico M. M Foster MeskoMárcia HerreroSantiago Jiménez-AparicioReyes LarhedMats Luque de CastroMaría D MorrisonRichard MoránEmilio OdellLuke PassosCláudia PerinoSandrine PetitcolasEmmanuel Prado-GonjalJésus Priego-BermejoJosé Luis SchmidtRainer SävmarkerJonas TabassoSilvia WuZhilin de Azevedo MelloPaola de Moraes FloresÉder L del Mar Delgado PovedanoMaría |
| Collana | De Gruyter Textbook |
| Soggetto topico |
Radiation chemistry
Microwaves Chemistry, Physical and theoretical |
| ISBN |
3-11-048002-6
3-11-047993-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Frontmatter -- Preface / Cravotto, Giancarlo -- Contents -- List of contributors -- 1. Microwave chemistry: history, development and legacy / Cravotto, Giancarlo / Cintas, Pedro -- 2. An Introduction to dielectric heating / Veronesi, Paolo -- 3. Microwave generators, transmission, and interaction with different materials / Leonelli, Cristina -- 4. Interpretation of the rate enhancing effect of microwaves / Keglevich, György / Mucsi, Zoltán -- 5. Industrial microwave reactors: components and set up / Radoiu, Marilena -- 6. The impact of microwaves in organic synthesis / Hoz, Antonio de la / Prieto, Pilar -- 7. Chemical reactions on the interfaces of solids under microwaves / Wada, Yuji / Mochizuki, Dai / Ano, Taishi / Maitani, Masato M. / Tsubaki, Shuntaro / Haneishi, Naoto -- 8. Some aspects of catalysis with microwaves / Horikoshi, Satoshi / Serpone, Nick -- 9. Microwaves in flow chemistry / Delbecq, Frédéric / Luque, Rafael / Len, Christophe -- 10. Microwaves in green and sustainable chemistry / Díaz-Ortiz, Ángel / Carrillo, José R. -- 11. Synthesis of medium-sized heterocycles under microwave irradiation / Sharma, Abhishek / Eycken, Erik Van der -- 12. Microwaves applied to hydrothermal synthesis of nanoparticles / Wojnarowicz, Jacek / Chudoba, Tadeusz / Majcher, Andrzej / Łojkowski, Witold -- 13. Microwave-assisted solvothermal synthesis of inorganic compounds (molecular and non molecular) / González-Prieto, Rodrigo / Herrero, Santiago / Jiménez-Aparicio, Reyes / Morán, Emilio / Prado-Gonjal, Jesús / Priego, José Luis / Schmidt, Rainer -- 14. Microwave-assisted synthesis of nanoparticles / Horikoshi, Satoshi / Serpone, Nick -- 15. Microwaves in polymer chemistry / Bogdal, Dariusz -- 16. Microwave extraction of natural products in the teaching laboratory: fundamentals of essential oils green extraction / Perino, Sandrine / Petitcolas, Emmanuel / Chemat, Farid -- 17. Microwave extraction of bioactive compounds from industrial by-products / Passos, Cláudia P. / Coimbra, Manuel A. -- 18. The Use of microwaves in drug discovery / Collina, Simona / Volpe, Serena Della -- 19. Microwave heating in medicinal chemistry / Engen, Karin / Sävmarker, Jonas / Odell, Luke R. / Larhed, Mats -- 20. Microwave-assisted biomass conversion / Tabasso, Silvia -- 21. Microwave technology for environmental remediation / Wu, Zhilin / Cravotto, Giancarlo -- 22. Microwaves in the omics field / Delgado-Povedano, María M. / Castro, María D. Luque de -- 23. Microwaves in sample preparation for elemental determination / Bizzi, Cezar Augusto / Flores, Erico Marlon de Moraes / Mesko, Marcia Foster -- 24. Microwave-assisted sample preparation for organic analysis / Barin, Juliano Smanioto / Duarte, Fábio Andrei / Mello, Paola de Azevedo / Flores, Éder Lisandro de Moraes -- 25. Microwave chemistry in the organic instructional laboratory / Morrison, Richard -- A snapshot of more common commercial microwave reactors |
| Record Nr. | UNINA-9910554867103321 |
| Berlin ; ; Boston : , : De Gruyter, , [2017] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Theoretical Aspects of Software Engineering : 19th International Symposium, TASE 2025, Limassol, Cyprus, July 14–16, 2025, Proceedings / / edited by Philipp Rümmer, Zhilin Wu
| Theoretical Aspects of Software Engineering : 19th International Symposium, TASE 2025, Limassol, Cyprus, July 14–16, 2025, Proceedings / / edited by Philipp Rümmer, Zhilin Wu |
| Autore | Rümmer Philipp |
| Edizione | [1st ed. 2026.] |
| Pubbl/distr/stampa | Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2026 |
| Descrizione fisica | 1 online resource (628 pages) |
| Disciplina | 005.1 |
| Altri autori (Persone) | WuZhilin |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Software Engineering |
| ISBN |
9783031982088
9783031982071 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | -- Program Verification. -- Safeguarding Neural Network-Controlled Systems via Formal Methods: From Safety-by-Design to Runtime Assurance (Invited Talk) . -- Testing-Based Formal Verification with Program Slicing on Functional Soundness and Completeness. -- Dependent Assertion Logic for Modular Software Verification. -- A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms. -- Machine-Checked Compositional Specification and Proofs for Embedded Systems. -- Verification and Concurrency. -- Failure divergence refinement for Event-B -- Mining Diamonds in labeled Transition Systems. -- Portability of Optimizations from SC to TSO. -- SAT and SMT Solving. -- Adaptive Clause Management in SMT Solvers: A Dynamic Weighting Framework for Formal Verification. -- SNRWLS: Improve (W)PMS Solver with Weighting Strategies Related to Number of Soft Clauses. -- Trustworthy AI and System Software. -- Robust Deep Reinforcement Learning Using Formal Verification. -- A Formally Verified Neural Network Converter for the Interactive Theorem Prover Coq. -- COMPASS: An Agent for MLIR Compilation Pass Pipeline Generation. -- Stable Ranges: Shared Dichotomy in Large Version-Controlled Repositories. -- Program Analysis using Machine Learning. -- CASTLE: Benchmarking Dataset for Static Code Analyzers and LLMs towards CWE Detection. -- FAMiT: Mitigating False Alarms for Program Analysis Using Large Language Models. -- Security. -- A Cross-domain Data Sharing Scheme Based on Federated Blockchain. -- Operational Semantics for Crystality: A Smart Contract Language for Parallel EVMs. -- Detecting speculative data flow vulnerabilities using weakest precondition reasoning. -- Dynamic Analysis. -- Random Testing of Model Checkers for Timed Automata with Automated Oracle Generation. -- State Significance-Guided Fuzzing for Stateful Protocol Program. -- Unleash the Hidden Power of CAR-based Model Checking through Dynamic Traversal. |
| Record Nr. | UNISA-996668471803316 |
Rümmer Philipp
|
||
| Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2026 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||