top

  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.

  Info

  • Utilizzare questo link per rimuovere la selezione effettuata.

Biblioteca

MARC Lista (tabellare)
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
Opac: Controlla la disponibilità qui
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. UNINA-9910620200703321
Cham, Switzerland : , : Springer, , [2022]
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Automated Technology for Verification and Analysis [[electronic resource] ] : 8th International Symposium, ATVA 2010, Singapore, September 21-24, 2010, Proceedings / / edited by Ahmed Bouajjani, Wei-Ngan Chin
Automated Technology for Verification and Analysis [[electronic resource] ] : 8th International Symposium, ATVA 2010, Singapore, September 21-24, 2010, Proceedings / / edited by Ahmed Bouajjani, Wei-Ngan Chin
Edizione [1st ed. 2010.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010
Descrizione fisica 1 online resource (VIII, 404 p. 112 illus.)
Disciplina 511.3/6028563
Collana Programming and Software Engineering
Soggetto topico Software engineering
Computer programming
Computer communication systems
Computer logic
Programming languages (Electronic computers)
Software Engineering/Programming and Operating Systems
Software Engineering
Programming Techniques
Computer Communication Networks
Logics and Meanings of Programs
Programming Languages, Compilers, Interpreters
ISBN 1-280-38884-6
9786613566768
3-642-15643-6
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Invited Talks -- Probabilistic Automata on Infinite Words: Decidability and Undecidability Results -- Abstraction Learning -- Synthesis: Words and Traces -- Regular Papers -- Promptness in ?-Regular Automata -- Using Redundant Constraints for Refinement -- Methods for Knowledge Based Controlling of Distributed Systems -- Composing Reachability Analyses of Hybrid Systems for Safety and Stability -- The Complexity of Codiagnosability for Discrete Event and Timed Systems -- On Scenario Synchronization -- Compositional Algorithms for LTL Synthesis -- What’s Decidable about Sequences? -- A Study of the Convergence of Steady State Probabilities in a Closed Fork-Join Network -- Lattice-Valued Binary Decision Diagrams -- A Specification Logic for Exceptions and Beyond -- Non-monotonic Refinement of Control Abstraction for Concurrent Programs -- An Approach for Class Testing from Class Contracts -- Efficient On-the-Fly Emptiness Check for Timed Büchi Automata -- Reachability as Derivability, Finite Countermodels and Verification -- LTL Can Be More Succinct -- Automatic Generation of History-Based Access Control from Information Flow Specification -- Auxiliary Constructs for Proving Liveness in Compassion Discrete Systems -- Symbolic Unfolding of Parametric Stopwatch Petri Nets -- Recursive Timed Automata -- Probabilistic Contracts for Component-Based Design -- Tool Papers -- Model-Checking Web Applications with Web-TLR -- GAVS: Game Arena Visualization and Synthesis -- CRI: Symbolic Debugger for MCAPI Applications -- MCGP: A Software Synthesis Tool Based on Model Checking and Genetic Programming -- ECDAR: An Environment for Compositional Design and Analysis of Real Time Systems -- Developing Model Checkers Using PAT -- YAGA: Automated Analysis of Quantitative Safety Specifications in Probabilistic B -- COMBINE: A Tool on Combined Formal Methods for Bindingly Verification -- Rbminer: A Tool for Discovering Petri Nets from Transition Systems.
Record Nr. UNISA-996465909103316
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Automated technology for verification and analysis : 8th International Symposium, ATVA 2010, Singapore, September 21-24, 2010 : proceedings / / Ahmed Bouajjani, Wei-Ngan Chin (eds.)
Automated technology for verification and analysis : 8th International Symposium, ATVA 2010, Singapore, September 21-24, 2010 : proceedings / / Ahmed Bouajjani, Wei-Ngan Chin (eds.)
Edizione [1st ed. 2010.]
Pubbl/distr/stampa New York, : Springer, 2010
Descrizione fisica 1 online resource (VIII, 404 p. 112 illus.)
Disciplina 511.3/6028563
Altri autori (Persone) BouajjaniAhmed
ChinWei-Ngan
Collana Lecture notes in computer science
LNCS sublibrary. SL 2, Programming and software engineering
Soggetto topico Automatic theorem proving
ISBN 1-280-38884-6
9786613566768
3-642-15643-6
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Invited Talks -- Probabilistic Automata on Infinite Words: Decidability and Undecidability Results -- Abstraction Learning -- Synthesis: Words and Traces -- Regular Papers -- Promptness in ?-Regular Automata -- Using Redundant Constraints for Refinement -- Methods for Knowledge Based Controlling of Distributed Systems -- Composing Reachability Analyses of Hybrid Systems for Safety and Stability -- The Complexity of Codiagnosability for Discrete Event and Timed Systems -- On Scenario Synchronization -- Compositional Algorithms for LTL Synthesis -- What’s Decidable about Sequences? -- A Study of the Convergence of Steady State Probabilities in a Closed Fork-Join Network -- Lattice-Valued Binary Decision Diagrams -- A Specification Logic for Exceptions and Beyond -- Non-monotonic Refinement of Control Abstraction for Concurrent Programs -- An Approach for Class Testing from Class Contracts -- Efficient On-the-Fly Emptiness Check for Timed Büchi Automata -- Reachability as Derivability, Finite Countermodels and Verification -- LTL Can Be More Succinct -- Automatic Generation of History-Based Access Control from Information Flow Specification -- Auxiliary Constructs for Proving Liveness in Compassion Discrete Systems -- Symbolic Unfolding of Parametric Stopwatch Petri Nets -- Recursive Timed Automata -- Probabilistic Contracts for Component-Based Design -- Tool Papers -- Model-Checking Web Applications with Web-TLR -- GAVS: Game Arena Visualization and Synthesis -- CRI: Symbolic Debugger for MCAPI Applications -- MCGP: A Software Synthesis Tool Based on Model Checking and Genetic Programming -- ECDAR: An Environment for Compositional Design and Analysis of Real Time Systems -- Developing Model Checkers Using PAT -- YAGA: Automated Analysis of Quantitative Safety Specifications in Probabilistic B -- COMBINE: A Tool on Combined Formal Methods for Bindingly Verification -- Rbminer: A Tool for Discovering Petri Nets from Transition Systems.
Record Nr. UNINA-9910485034203321
New York, : Springer, 2010
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Computer Aided Verification [[electronic resource] ] : 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009, Proceedings / / edited by Ahmed Bouajjani, Oded Maler
Computer Aided Verification [[electronic resource] ] : 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009, Proceedings / / edited by Ahmed Bouajjani, Oded Maler
Edizione [1st ed. 2009.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009
Descrizione fisica 1 online resource (XV, 722 p.)
Disciplina 005.11
Collana Theoretical Computer Science and General Issues
Soggetto topico Computer programming
Computer systems
Software engineering
Computer science
Machine theory
Programming Techniques
Computer System Implementation
Software Engineering
Computer Science Logic and Foundations of Programming
Formal Languages and Automata Theory
ISBN 3-642-02658-3
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Invited Tutorials -- Transactional Memory: Glimmer of a Theory -- Mixed-Signal System Verification: A High-Speed Link Example -- Modelling Epigenetic Information Maintenance: A Kappa Tutorial -- Component-Based Construction of Real-Time Systems in BIP -- Invited Talks -- Models and Proofs of Protocol Security: A Progress Report -- Predictability vs. Efficiency in the Multicore Era: Fight of Titans or Happy Ever after? -- SPEED: Symbolic Complexity Bound Analysis -- Regression Verification: Proving the Equivalence of Similar Programs -- Regular Papers -- Symbolic Counter Abstraction for Concurrent Software -- Priority Scheduling of Distributed Systems Based on Model Checking -- Explaining Counterexamples Using Causality -- Size-Change Termination, Monotonicity Constraints and Ranking Functions -- Linear Functional Fixed-points -- Better Quality in Synthesis through Quantitative Objectives -- Automatic Verification of Integer Array Programs -- Automated Analysis of Java Methods for Confidentiality -- Requirements Validation for Hybrid Systems -- Towards Performance Prediction of Compositional Models in Industrial GALS Designs -- Image Computation for Polynomial Dynamical Systems Using the Bernstein Expansion -- Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers -- Meta-analysis for Atomicity Violations under Nested Locking -- An Antichain Algorithm for LTL Realizability -- On Extending Bounded Proofs to Inductive Proofs -- Games through Nested Fixpoints -- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories -- Software Transactional Memory on Relaxed Memory Models -- Sliding Window Abstraction for Infinite Markov Chains -- Centaur Technology Media Unit Verification -- Incremental Instance Generation in Local Reasoning -- Quantifier Elimination via Functional Composition -- Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique -- Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine Validation -- Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models -- A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer Constraints -- Generalizing DPLL to Richer Logics -- Reducing Context-Bounded Concurrent Reachability to Sequential Reachability -- Intra-module Inference -- Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers -- Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints -- Reachability Analysis of Hybrid Systems Using Support Functions -- Reducing Test Inputs Using Information Partitions -- On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure -- Cardinality Abstraction for Declarative Networking Applications -- Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences -- Tool Papers -- D-Finder: A Tool for Compositional Deadlock Detection and Verification -- HybridFluctuat: A Static Analyzer of Numerical Programs within a Continuous Environment -- The Zonotope Abstract Domain Taylor1+ -- InvGen: An Efficient Invariant Generator -- INFAMY: An Infinite-State Markov Model Checker -- Browser-Based Enforcement of Interface Contracts in Web Applications with BeepBeep -- Homer: A Higher-Order Observational Equivalence Model checkER -- Apron: A Library of Numerical Abstract Domains for Static Analysis -- Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic -- CalFuzzer: An Extensible Active Testing Framework for Concurrent Programs -- MCMAS: A Model Checker for the Verification of Multi-Agent Systems -- TASS: Timing Analyzer of Scenario-Based Specifications -- Translation Validation: From Simulink to C -- VS3: SMT Solvers for Program Verification -- PAT: Towards Flexible Verification under Fairness -- A Concurrent Portfolio Approach to SMT Solving.
Record Nr. UNISA-996465423003316
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Computer aided verification : 21st international conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009 ; proceedings / / Ahmed Bouajjani, Oded Maler (eds.)
Computer aided verification : 21st international conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009 ; proceedings / / Ahmed Bouajjani, Oded Maler (eds.)
Edizione [1st ed. 2009.]
Pubbl/distr/stampa Berlin ; ; New York, : Springer, c2009
Descrizione fisica 1 online resource (XV, 722 p.)
Disciplina 005.11
Altri autori (Persone) BouajjaniAhmed
MalerO (Oded)
Collana Lecture notes in computer science
Soggetto topico Computer software - Verification
Integrated circuits - Verification
ISBN 3-642-02658-3
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Invited Tutorials -- Transactional Memory: Glimmer of a Theory -- Mixed-Signal System Verification: A High-Speed Link Example -- Modelling Epigenetic Information Maintenance: A Kappa Tutorial -- Component-Based Construction of Real-Time Systems in BIP -- Invited Talks -- Models and Proofs of Protocol Security: A Progress Report -- Predictability vs. Efficiency in the Multicore Era: Fight of Titans or Happy Ever after? -- SPEED: Symbolic Complexity Bound Analysis -- Regression Verification: Proving the Equivalence of Similar Programs -- Regular Papers -- Symbolic Counter Abstraction for Concurrent Software -- Priority Scheduling of Distributed Systems Based on Model Checking -- Explaining Counterexamples Using Causality -- Size-Change Termination, Monotonicity Constraints and Ranking Functions -- Linear Functional Fixed-points -- Better Quality in Synthesis through Quantitative Objectives -- Automatic Verification of Integer Array Programs -- Automated Analysis of Java Methods for Confidentiality -- Requirements Validation for Hybrid Systems -- Towards Performance Prediction of Compositional Models in Industrial GALS Designs -- Image Computation for Polynomial Dynamical Systems Using the Bernstein Expansion -- Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers -- Meta-analysis for Atomicity Violations under Nested Locking -- An Antichain Algorithm for LTL Realizability -- On Extending Bounded Proofs to Inductive Proofs -- Games through Nested Fixpoints -- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories -- Software Transactional Memory on Relaxed Memory Models -- Sliding Window Abstraction for Infinite Markov Chains -- Centaur Technology Media Unit Verification -- Incremental Instance Generation in Local Reasoning -- Quantifier Elimination via Functional Composition -- Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique -- Replacing Testing with Formal Verification in Intel CoreTM i7 Processor Execution Engine Validation -- Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models -- A Markov Chain Monte Carlo Sampler for Mixed Boolean/Integer Constraints -- Generalizing DPLL to Richer Logics -- Reducing Context-Bounded Concurrent Reachability to Sequential Reachability -- Intra-module Inference -- Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers -- Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints -- Reachability Analysis of Hybrid Systems Using Support Functions -- Reducing Test Inputs Using Information Partitions -- On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure -- Cardinality Abstraction for Declarative Networking Applications -- Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences -- Tool Papers -- D-Finder: A Tool for Compositional Deadlock Detection and Verification -- HybridFluctuat: A Static Analyzer of Numerical Programs within a Continuous Environment -- The Zonotope Abstract Domain Taylor1+ -- InvGen: An Efficient Invariant Generator -- INFAMY: An Infinite-State Markov Model Checker -- Browser-Based Enforcement of Interface Contracts in Web Applications with BeepBeep -- Homer: A Higher-Order Observational Equivalence Model checkER -- Apron: A Library of Numerical Abstract Domains for Static Analysis -- Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic -- CalFuzzer: An Extensible Active Testing Framework for Concurrent Programs -- MCMAS: A Model Checker for the Verification of Multi-Agent Systems -- TASS: Timing Analyzer of Scenario-Based Specifications -- Translation Validation: From Simulink to C -- VS3: SMT Solvers for Program Verification -- PAT: Towards Flexible Verification under Fairness -- A Concurrent Portfolio Approach to SMT Solving.
Altri titoli varianti CAV 2009
Record Nr. UNINA-9910483039603321
Berlin ; ; New York, : Springer, c2009
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Formal Techniques for Distributed Objects, Components, and Systems [[electronic resource] ] : 37th IFIP WG 6.1 International Conference, FORTE 2017, Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017, Neuchâtel, Switzerland, June 19-22, 2017, Proceedings / / edited by Ahmed Bouajjani, Alexandra Silva
Formal Techniques for Distributed Objects, Components, and Systems [[electronic resource] ] : 37th IFIP WG 6.1 International Conference, FORTE 2017, Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017, Neuchâtel, Switzerland, June 19-22, 2017, Proceedings / / edited by Ahmed Bouajjani, Alexandra Silva
Edizione [1st ed. 2017.]
Pubbl/distr/stampa Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017
Descrizione fisica 1 online resource (XIV, 243 p. 50 illus.)
Disciplina 004.36
Collana Programming and Software Engineering
Soggetto topico Computer logic
Software engineering
Artificial intelligence
Mathematical logic
Computer communication systems
Logics and Meanings of Programs
Software Engineering
Artificial Intelligence
Mathematical Logic and Formal Languages
Computer Communication Networks
ISBN 3-319-60225-X
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Session types for Link failures -- Learning-based compositional parameter synthesis for event-recording automata -- Modularising opacity verification for Hybrid Transactional Memory -- Proving opacity via linearizability: a sound and complete method -- On futures for streaming data in ABS -- Session-based concurrency, reactively -- Procedural choreographic programming -- An observational approach to defining linearizability on weak memory models -- Applying a dependency mechanism in the formal development of voting protocol models using event-B -- Weak simulation quasimetric in a gossip scenario -- Reasoning about distributed secrets -- Classical higher-order processes -- Weak nominal modal logic -- Type inference of simulink hierarchical block diagrams in Isabelle -- Creating Büchi automata for multi-valued model checking -- Privacy assessment using static taint analysis -- EPTL - a temporal logic for weakly consistent systems.
Record Nr. UNISA-996466288503316
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Formal Techniques for Distributed Objects, Components, and Systems : 37th IFIP WG 6.1 International Conference, FORTE 2017, Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017, Neuchâtel, Switzerland, June 19-22, 2017, Proceedings / / edited by Ahmed Bouajjani, Alexandra Silva
Formal Techniques for Distributed Objects, Components, and Systems : 37th IFIP WG 6.1 International Conference, FORTE 2017, Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017, Neuchâtel, Switzerland, June 19-22, 2017, Proceedings / / edited by Ahmed Bouajjani, Alexandra Silva
Edizione [1st ed. 2017.]
Pubbl/distr/stampa Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017
Descrizione fisica 1 online resource (XIV, 243 p. 50 illus.)
Disciplina 004.36
Collana Programming and Software Engineering
Soggetto topico Computer logic
Software engineering
Artificial intelligence
Mathematical logic
Computer communication systems
Logics and Meanings of Programs
Software Engineering
Artificial Intelligence
Mathematical Logic and Formal Languages
Computer Communication Networks
ISBN 3-319-60225-X
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Session types for Link failures -- Learning-based compositional parameter synthesis for event-recording automata -- Modularising opacity verification for Hybrid Transactional Memory -- Proving opacity via linearizability: a sound and complete method -- On futures for streaming data in ABS -- Session-based concurrency, reactively -- Procedural choreographic programming -- An observational approach to defining linearizability on weak memory models -- Applying a dependency mechanism in the formal development of voting protocol models using event-B -- Weak simulation quasimetric in a gossip scenario -- Reasoning about distributed secrets -- Classical higher-order processes -- Weak nominal modal logic -- Type inference of simulink hierarchical block diagrams in Isabelle -- Creating Büchi automata for multi-valued model checking -- Privacy assessment using static taint analysis -- EPTL - a temporal logic for weakly consistent systems.
Record Nr. UNINA-9910484171503321
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Networked Systems [[electronic resource] ] : Third International Conference, NETYS 2015, Agadir, Morocco, May 13-15, 2015, Revised Selected Papers / / edited by Ahmed Bouajjani, Hugues Fauconnier
Networked Systems [[electronic resource] ] : Third International Conference, NETYS 2015, Agadir, Morocco, May 13-15, 2015, Revised Selected Papers / / edited by Ahmed Bouajjani, Hugues Fauconnier
Edizione [1st ed. 2015.]
Pubbl/distr/stampa Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015
Descrizione fisica 1 online resource (XXVIII, 526 p. 165 illus.)
Disciplina 004.6
Collana Computer Communication Networks and Telecommunications
Soggetto topico Computer communication systems
Algorithms
Software engineering
Application software
Computer Communication Networks
Algorithm Analysis and Problem Complexity
Software Engineering
Information Systems Applications (incl. Internet)
ISBN 3-319-26850-3
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Multi-core architectures -- Concurrent and distributed algorithms -- Middleware environments -- Storage clusters -- Social networks -- Peer-to-peer networks -- Sensor networks -- Wireless and mobile networks -- Privacy and security measures.
Record Nr. UNISA-996466218603316
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Networked Systems : Third International Conference, NETYS 2015, Agadir, Morocco, May 13-15, 2015, Revised Selected Papers / / edited by Ahmed Bouajjani, Hugues Fauconnier
Networked Systems : Third International Conference, NETYS 2015, Agadir, Morocco, May 13-15, 2015, Revised Selected Papers / / edited by Ahmed Bouajjani, Hugues Fauconnier
Edizione [1st ed. 2015.]
Pubbl/distr/stampa Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015
Descrizione fisica 1 online resource (XXVIII, 526 p. 165 illus.)
Disciplina 004.6
Collana Computer Communication Networks and Telecommunications
Soggetto topico Computer communication systems
Algorithms
Software engineering
Application software
Computer Communication Networks
Algorithm Analysis and Problem Complexity
Software Engineering
Information Systems Applications (incl. Internet)
ISBN 3-319-26850-3
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Multi-core architectures -- Concurrent and distributed algorithms -- Middleware environments -- Storage clusters -- Social networks -- Peer-to-peer networks -- Sensor networks -- Wireless and mobile networks -- Privacy and security measures.
Record Nr. UNINA-9910484658203321
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui