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.
Formal Modeling and Analysis of Timed Systems [[electronic resource] ] : 13th International Conference, FORMATS 2015, Madrid, Spain, September 2-4, 2015, Proceedings / / edited by Sriram Sankaranarayanan, Enrico Vicario
| Formal Modeling and Analysis of Timed Systems [[electronic resource] ] : 13th International Conference, FORMATS 2015, Madrid, Spain, September 2-4, 2015, Proceedings / / edited by Sriram Sankaranarayanan, Enrico Vicario |
| Edizione | [1st ed. 2015.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 |
| Descrizione fisica | 1 online resource (X, 321 p. 90 illus.) |
| Disciplina | 003.3 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Application software Machine theory Theory of Computation Computer Science Logic and Foundations of Programming Software Engineering Computer and Information Systems Applications Formal Languages and Automata Theory |
| ISBN | 3-319-22975-3 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Contents -- Verification and Control of Probabilistic Rectangular Hybrid Automata -- 1 Background and Motivation -- 2 Probabilistic Rectangular Hybrid Automata -- 3 Approximation with Probabilistic Hybrid Automata -- References -- Performance Evaluation of an Emergency Call Center: Tropical Polynomial Systems Applied to Timed Petri Nets -- 1 Introduction -- 2 A Simplified Petri Net Model of an Emergency Call Center -- 3 Piecewise Linear Dynamics of Timed Petri Nets with Free Choice and Priority Routing -- 3.1 Timed Petri Nets: Notation and Semantics -- 3.2 Timed Petri Nets with Free Choice and Priority Routing -- 3.3 Piecewise Linear Representation by Counter Variables -- 4 Computing Stationary Regimes -- 5 Application to the Emergency Call Center -- 6 Experiments -- 7 Concluding Remarks -- References -- Language Preservation Problems in Parametric Timed Automata -- 1 Introduction -- 2 Definitions -- 3 Undecidability of the Preservation Problems in General -- 3.1 Undecidability of the Language Preservation Problem -- 3.2 Undecidability of the Trace Preservation Problem. -- 3.3 Undecidability of the Robust Language-Preservation Problem -- 3.4 Undecidability of the Robust Trace Preservation Problem -- 4 A Semi-algorithm for the Trace Preservation Synthesis -- 5 Decidability Results for Subclasses of PTA -- 5.1 1-Clock PTA -- 5.2 Decidability and Synthesis for Deterministic 1-Clock PTA -- 5.3 Undecidability for L/U-PTA -- 5.4 A Decidability Result for 1-Parameter L-PTA and U-PTA -- 6 Conclusion and Perspectives -- References -- Timed Symbolic Dynamics -- 1 Introduction -- 2 Preliminaries -- 2.1 Dynamical Systems -- 2.2 -Entropies and Topological Entropy -- 2.3 Shift Spaces on General Alphabet -- 2.4 Edge and Sofic Shifts from Classical Symbolic Dynamics -- 2.5 Comparison with Finite State Automata.
3 Factor Based Characterisations -- 3.1 Factor Based Characterisation of General Alphabet Shift Spaces -- 3.2 Entropies for General Alphabet Shift Spaces -- 3.3 Sliding Block Codes for General Alphabet Shift Spaces -- 4 Timed Shift Spaces and Their Measures -- 4.1 Timed Shift Spaces -- 4.2 Discretisation of Shift Spaces and Their Entropy -- 4.3 Metric Mean Dimension of Timed Sofic Shifts -- 5 Conclusion and Perspectives -- References -- Timed-Automata Abstraction of Switched Dynamical Systems Using Control Funnels -- 1 Introduction -- 2 Graphs of Control Funnels -- 2.1 Control Funnels -- 2.2 Motion Planning -- 2.3 Motion Planning with Graphs of Control Funnels -- 3 Reduction to Timed Automata -- 4 LQR Funnels -- 5 Examples of Application -- 5.1 Synchronization of Sine Waves -- 5.2 A 1D Pick-and-Place Problem -- 6 Conclusion and Future Work -- References -- Quantitative Analysis of Communication Scenarios -- 1 Introduction -- 2 Preliminaries -- 2.1 Branching-Time Models and Quantitative Annotations -- 2.2 Scenarios Specifying Communication Systems -- 3 Branching-Time Semantics -- 3.1 Model Checking Branching-Time Requirements -- 4 Quantitative Message Sequence Graphs -- 4.1 Model Checking Quantitative Requirements -- 5 Implementation and Case Study -- 5.1 Models and Requirements in our Case Study -- 5.2 Evaluation -- 6 Conclusion -- References -- Multi-objective Parameter Synthesis in Probabilistic Hybrid Systems -- 1 Introduction -- 2 Parametric Probabilistic Hybrid Automata -- 2.1 Interpretation as Parametric Infinite-State Markov Chain -- 2.2 Parameter Synthesis -- 3 Estimating Expectations by Sampling -- 4 Symbolic Representation of Importance Sampling -- 5 Existence or Absence of Parameter Instances -- 6 Experiments -- 7 Related Work -- 8 Conclusion -- References -- On the Scalability of Constraint Solving for Static/Off-Line Real-Time Scheduling. 1 Introduction -- 2 Related Work -- 3 ILP/SMT/CP Modeling of Scheduling Problems -- 3.1 Single-Period Dependent Tasks, Heterogenous Architecture -- 3.2 Simplified Encoding for the Homogenous Case -- 3.3 Multi-period, Non-preemptive, Non-dependent Tasks -- 3.4 Multi-period, Preemptive, Non-dependent Tasks -- 4 Test Cases -- 4.1 Test Case Generation -- 4.2 Signal Processing Case Studies -- 5 Experimental Results -- 5.1 Synthetic Test Cases -- 5.2 Signal Processing Case Studies -- 6 Conclusion -- References -- Improving Search Order for Reachability Testing in Timed Automata -- 1 Introduction -- 2 Preliminaries -- 2.1 Timed Automata and the Reachability Problem -- 2.2 Symbolic Semantics -- 2.3 Reachability Algorithm -- 3 Ranking System -- 4 Waiting Strategy -- 4.1 Topological-Like Ordering for a Timed Automaton -- 4.2 Topological-Like Ordering for Networks of Timed Automata -- 5 Experimental Evaluation -- 6 Conclusion -- References -- Symbolic Minimum Expected Time Controller Synthesis for Probabilistic Timed Automata -- 1 Introduction -- 2 Background -- 3 Probabilistic Timed Automata -- 4 Minimum Expected Time Algorithm for PTAs -- 5 Conclusion -- References -- Quantitative Attack Tree Analysis via Priced Timed Automata -- 1 Introduction -- 2 Graphical Security Modeling -- 2.1 Attack Trees -- 2.2 Metrics on ATs -- 3 Priced Timed Automata -- 4 Analyzing Attack Trees via Price Timed Automata -- 4.1 From Attack Trees to Price Timed Automata -- 4.2 Quantitative Analysis of Attack Trees -- 5 Case Studies -- 6 Conclusion -- References -- Fluid Model Checking of Timed Properties -- 1 Introduction -- 2 Background and Modelling Language -- 2.1 Timed Properties -- 3 Fluid Model Checking of Timed Properties -- 3.1 The Mean Behaviour of the Population Model -- 4 Experimental Results -- 5 Conclusions -- References -- Nested Timed Automata with Frozen Clocks. 1 Introduction -- 2 Dense Timed Pushdown Automata with Frozen Ages -- 2.1 Dense Timed Pushdown Automata -- 2.2 DTPDAs with Frozen Ages -- 3 Reachability of DTPDAs with Frozen Ages -- 3.1 Digiword and Its Operations -- 3.2 Snapshot Pushdown System -- 3.3 Well-Formed Constraint -- 4 Nested Timed Automata with Frozen Clocks -- 4.1 Nested Timed Automata with Frozen Clocks -- 4.2 Reachability of NeTA-Fs with Multiple Global Clocks -- 4.3 Reachability of NeTA-F with a Single Global Clock -- 5 Conclusion -- References -- Quantitative Analysis of Concurrent Reversible Computations -- 1 Introduction -- 2 Continuous-Time Markov Chains -- 3 Stochastic Automata -- 4 Reversible Stochastic Automata -- 4.1 Synchronisation of an Arbitrary Number of Automata -- 5 Conclusion -- References -- Hybrid Tools for Hybrid Systems -- Proving Stability and Safety at Once -- 1 Introduction -- 2 Related Work -- 3 Preliminaries -- 3.1 Checking Stability via Stabhyli -- 3.2 Checking Reachability via SoapBox -- 4 Hybrid Stability and Reachability Tool -- 4.1 Single-Mode Lyapunov Function Computation -- 4.2 SafeSet Computation -- 4.3 SafeBox Conversion -- 4.4 Unrolling Algorithm -- 4.5 Global Lyapunov Function Computation -- 5 Benchmarking -- 6 Summary -- References -- Verification and Control of Partially Observable Probabilistic Real-Time Systems -- 1 Introduction -- 2 Partially Observable Markov Decision Processes -- 3 Partially Observable Probabilistic Timed Automata -- 4 Verification and Strategy Synthesis for POPTAs -- 5 Implementation and Case Studies -- 6 Conclusions -- References -- Deciding Concurrent Planar Monotonic Linear Hybrid Systems -- 1 Introduction -- 2 Preliminaries -- 3 Linear Hybrid Systems -- 3.1 Semantics -- 3.2 Special Subclasses of Linear Hybrid Automata -- 3.3 Parallel Composition of Linear Hybrid Automata. 4 Timed Language Equivalence of PMHS and Timed Automata -- 5 Main Result -- 6 A Decidable Class of Multi-rate Automata -- 7 Conclusion -- References -- Contracts for Schedulability Analysis -- 1 Introduction and Related Work -- 2 Scheduling Components -- 2.1 Our Approach: Building on Top of Assume/Guarantee Contracts -- 2.2 Concrete Scheduling Components -- 2.3 Abstract Scheduling Components -- 2.4 Faithfulness of the Mapping -- 3 Scheduling Contracts -- 3.1 Getting Sub-contracts in the AUTOSAR Development Process -- 4 An Example in the Context of AUTOSAR -- 5 Conclusion -- References -- Bounded Determinization of Timed Automata with Silent Transitions -- 1 Introduction -- 2 Timed Automata with Silent Transitions -- 3 k-Bounded Unfolding of Timed Automata -- 3.1 Renaming the Clocks -- 4 Removing the Silent Transitions -- 5 Determinization -- 6 Complexity -- 7 Implementation and Experimental Results -- 8 Related Work -- 9 Conclusion -- References -- A Score Function for Optimizing the Cycle-Life of Battery-Powered Embedded Systems -- 1 Introduction -- 2 Uppaal Stratego -- 3 Battery Concepts -- 4 The Wear Score Function for SOC-Profiles -- 5 Nano-satellite Case Study -- 5.1 System Description -- 5.2 Satellite Model -- 5.3 Learning and Optimization -- 6 Discussion of the Wear Score Function -- 6.1 Limitations -- 7 Related Work -- 8 Conclusion -- References -- A Appendix -- Author Index. |
| Record Nr. | UNISA-996200367003316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Formal Modeling and Analysis of Timed Systems [[electronic resource] ] : 13th International Conference, FORMATS 2015, Madrid, Spain, September 2-4, 2015, Proceedings / / edited by Sriram Sankaranarayanan, Enrico Vicario
| Formal Modeling and Analysis of Timed Systems [[electronic resource] ] : 13th International Conference, FORMATS 2015, Madrid, Spain, September 2-4, 2015, Proceedings / / edited by Sriram Sankaranarayanan, Enrico Vicario |
| Edizione | [1st ed. 2015.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 |
| Descrizione fisica | 1 online resource (X, 321 p. 90 illus.) |
| Disciplina | 003.3 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Application software Machine theory Theory of Computation Computer Science Logic and Foundations of Programming Software Engineering Computer and Information Systems Applications Formal Languages and Automata Theory |
| ISBN | 3-319-22975-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Contents -- Verification and Control of Probabilistic Rectangular Hybrid Automata -- 1 Background and Motivation -- 2 Probabilistic Rectangular Hybrid Automata -- 3 Approximation with Probabilistic Hybrid Automata -- References -- Performance Evaluation of an Emergency Call Center: Tropical Polynomial Systems Applied to Timed Petri Nets -- 1 Introduction -- 2 A Simplified Petri Net Model of an Emergency Call Center -- 3 Piecewise Linear Dynamics of Timed Petri Nets with Free Choice and Priority Routing -- 3.1 Timed Petri Nets: Notation and Semantics -- 3.2 Timed Petri Nets with Free Choice and Priority Routing -- 3.3 Piecewise Linear Representation by Counter Variables -- 4 Computing Stationary Regimes -- 5 Application to the Emergency Call Center -- 6 Experiments -- 7 Concluding Remarks -- References -- Language Preservation Problems in Parametric Timed Automata -- 1 Introduction -- 2 Definitions -- 3 Undecidability of the Preservation Problems in General -- 3.1 Undecidability of the Language Preservation Problem -- 3.2 Undecidability of the Trace Preservation Problem. -- 3.3 Undecidability of the Robust Language-Preservation Problem -- 3.4 Undecidability of the Robust Trace Preservation Problem -- 4 A Semi-algorithm for the Trace Preservation Synthesis -- 5 Decidability Results for Subclasses of PTA -- 5.1 1-Clock PTA -- 5.2 Decidability and Synthesis for Deterministic 1-Clock PTA -- 5.3 Undecidability for L/U-PTA -- 5.4 A Decidability Result for 1-Parameter L-PTA and U-PTA -- 6 Conclusion and Perspectives -- References -- Timed Symbolic Dynamics -- 1 Introduction -- 2 Preliminaries -- 2.1 Dynamical Systems -- 2.2 -Entropies and Topological Entropy -- 2.3 Shift Spaces on General Alphabet -- 2.4 Edge and Sofic Shifts from Classical Symbolic Dynamics -- 2.5 Comparison with Finite State Automata.
3 Factor Based Characterisations -- 3.1 Factor Based Characterisation of General Alphabet Shift Spaces -- 3.2 Entropies for General Alphabet Shift Spaces -- 3.3 Sliding Block Codes for General Alphabet Shift Spaces -- 4 Timed Shift Spaces and Their Measures -- 4.1 Timed Shift Spaces -- 4.2 Discretisation of Shift Spaces and Their Entropy -- 4.3 Metric Mean Dimension of Timed Sofic Shifts -- 5 Conclusion and Perspectives -- References -- Timed-Automata Abstraction of Switched Dynamical Systems Using Control Funnels -- 1 Introduction -- 2 Graphs of Control Funnels -- 2.1 Control Funnels -- 2.2 Motion Planning -- 2.3 Motion Planning with Graphs of Control Funnels -- 3 Reduction to Timed Automata -- 4 LQR Funnels -- 5 Examples of Application -- 5.1 Synchronization of Sine Waves -- 5.2 A 1D Pick-and-Place Problem -- 6 Conclusion and Future Work -- References -- Quantitative Analysis of Communication Scenarios -- 1 Introduction -- 2 Preliminaries -- 2.1 Branching-Time Models and Quantitative Annotations -- 2.2 Scenarios Specifying Communication Systems -- 3 Branching-Time Semantics -- 3.1 Model Checking Branching-Time Requirements -- 4 Quantitative Message Sequence Graphs -- 4.1 Model Checking Quantitative Requirements -- 5 Implementation and Case Study -- 5.1 Models and Requirements in our Case Study -- 5.2 Evaluation -- 6 Conclusion -- References -- Multi-objective Parameter Synthesis in Probabilistic Hybrid Systems -- 1 Introduction -- 2 Parametric Probabilistic Hybrid Automata -- 2.1 Interpretation as Parametric Infinite-State Markov Chain -- 2.2 Parameter Synthesis -- 3 Estimating Expectations by Sampling -- 4 Symbolic Representation of Importance Sampling -- 5 Existence or Absence of Parameter Instances -- 6 Experiments -- 7 Related Work -- 8 Conclusion -- References -- On the Scalability of Constraint Solving for Static/Off-Line Real-Time Scheduling. 1 Introduction -- 2 Related Work -- 3 ILP/SMT/CP Modeling of Scheduling Problems -- 3.1 Single-Period Dependent Tasks, Heterogenous Architecture -- 3.2 Simplified Encoding for the Homogenous Case -- 3.3 Multi-period, Non-preemptive, Non-dependent Tasks -- 3.4 Multi-period, Preemptive, Non-dependent Tasks -- 4 Test Cases -- 4.1 Test Case Generation -- 4.2 Signal Processing Case Studies -- 5 Experimental Results -- 5.1 Synthetic Test Cases -- 5.2 Signal Processing Case Studies -- 6 Conclusion -- References -- Improving Search Order for Reachability Testing in Timed Automata -- 1 Introduction -- 2 Preliminaries -- 2.1 Timed Automata and the Reachability Problem -- 2.2 Symbolic Semantics -- 2.3 Reachability Algorithm -- 3 Ranking System -- 4 Waiting Strategy -- 4.1 Topological-Like Ordering for a Timed Automaton -- 4.2 Topological-Like Ordering for Networks of Timed Automata -- 5 Experimental Evaluation -- 6 Conclusion -- References -- Symbolic Minimum Expected Time Controller Synthesis for Probabilistic Timed Automata -- 1 Introduction -- 2 Background -- 3 Probabilistic Timed Automata -- 4 Minimum Expected Time Algorithm for PTAs -- 5 Conclusion -- References -- Quantitative Attack Tree Analysis via Priced Timed Automata -- 1 Introduction -- 2 Graphical Security Modeling -- 2.1 Attack Trees -- 2.2 Metrics on ATs -- 3 Priced Timed Automata -- 4 Analyzing Attack Trees via Price Timed Automata -- 4.1 From Attack Trees to Price Timed Automata -- 4.2 Quantitative Analysis of Attack Trees -- 5 Case Studies -- 6 Conclusion -- References -- Fluid Model Checking of Timed Properties -- 1 Introduction -- 2 Background and Modelling Language -- 2.1 Timed Properties -- 3 Fluid Model Checking of Timed Properties -- 3.1 The Mean Behaviour of the Population Model -- 4 Experimental Results -- 5 Conclusions -- References -- Nested Timed Automata with Frozen Clocks. 1 Introduction -- 2 Dense Timed Pushdown Automata with Frozen Ages -- 2.1 Dense Timed Pushdown Automata -- 2.2 DTPDAs with Frozen Ages -- 3 Reachability of DTPDAs with Frozen Ages -- 3.1 Digiword and Its Operations -- 3.2 Snapshot Pushdown System -- 3.3 Well-Formed Constraint -- 4 Nested Timed Automata with Frozen Clocks -- 4.1 Nested Timed Automata with Frozen Clocks -- 4.2 Reachability of NeTA-Fs with Multiple Global Clocks -- 4.3 Reachability of NeTA-F with a Single Global Clock -- 5 Conclusion -- References -- Quantitative Analysis of Concurrent Reversible Computations -- 1 Introduction -- 2 Continuous-Time Markov Chains -- 3 Stochastic Automata -- 4 Reversible Stochastic Automata -- 4.1 Synchronisation of an Arbitrary Number of Automata -- 5 Conclusion -- References -- Hybrid Tools for Hybrid Systems -- Proving Stability and Safety at Once -- 1 Introduction -- 2 Related Work -- 3 Preliminaries -- 3.1 Checking Stability via Stabhyli -- 3.2 Checking Reachability via SoapBox -- 4 Hybrid Stability and Reachability Tool -- 4.1 Single-Mode Lyapunov Function Computation -- 4.2 SafeSet Computation -- 4.3 SafeBox Conversion -- 4.4 Unrolling Algorithm -- 4.5 Global Lyapunov Function Computation -- 5 Benchmarking -- 6 Summary -- References -- Verification and Control of Partially Observable Probabilistic Real-Time Systems -- 1 Introduction -- 2 Partially Observable Markov Decision Processes -- 3 Partially Observable Probabilistic Timed Automata -- 4 Verification and Strategy Synthesis for POPTAs -- 5 Implementation and Case Studies -- 6 Conclusions -- References -- Deciding Concurrent Planar Monotonic Linear Hybrid Systems -- 1 Introduction -- 2 Preliminaries -- 3 Linear Hybrid Systems -- 3.1 Semantics -- 3.2 Special Subclasses of Linear Hybrid Automata -- 3.3 Parallel Composition of Linear Hybrid Automata. 4 Timed Language Equivalence of PMHS and Timed Automata -- 5 Main Result -- 6 A Decidable Class of Multi-rate Automata -- 7 Conclusion -- References -- Contracts for Schedulability Analysis -- 1 Introduction and Related Work -- 2 Scheduling Components -- 2.1 Our Approach: Building on Top of Assume/Guarantee Contracts -- 2.2 Concrete Scheduling Components -- 2.3 Abstract Scheduling Components -- 2.4 Faithfulness of the Mapping -- 3 Scheduling Contracts -- 3.1 Getting Sub-contracts in the AUTOSAR Development Process -- 4 An Example in the Context of AUTOSAR -- 5 Conclusion -- References -- Bounded Determinization of Timed Automata with Silent Transitions -- 1 Introduction -- 2 Timed Automata with Silent Transitions -- 3 k-Bounded Unfolding of Timed Automata -- 3.1 Renaming the Clocks -- 4 Removing the Silent Transitions -- 5 Determinization -- 6 Complexity -- 7 Implementation and Experimental Results -- 8 Related Work -- 9 Conclusion -- References -- A Score Function for Optimizing the Cycle-Life of Battery-Powered Embedded Systems -- 1 Introduction -- 2 Uppaal Stratego -- 3 Battery Concepts -- 4 The Wear Score Function for SOC-Profiles -- 5 Nano-satellite Case Study -- 5.1 System Description -- 5.2 Satellite Model -- 5.3 Learning and Optimization -- 6 Discussion of the Wear Score Function -- 6.1 Limitations -- 7 Related Work -- 8 Conclusion -- References -- A Appendix -- Author Index. |
| Record Nr. | UNINA-9910483460503321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
HSCC '15 : 18th ACM International Conference on Hybrid Systems : Computation and Control
| HSCC '15 : 18th ACM International Conference on Hybrid Systems : Computation and Control |
| Autore | Girard Antoine |
| Pubbl/distr/stampa | [Place of publication not identified], : ACM, 2015 |
| Descrizione fisica | 1 online resource (321 pages) |
| Collana | ACM Conferences |
| Soggetto topico |
Computer Science
Engineering & Applied Sciences |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Altri titoli varianti |
Hybrid Systems Computation and Control '15 : eighteenth Association for Computing Machinery International Conference on Hybrid Systems : Computation and Control
Proceedings of the 18th International Conference on Hybrid Systems : Computation and Control HSCC '15 18th International Conference on Hybrid Systems : Computation and Control (part of CPS Week), Seattle, WA, USA - April 14-16, 2015 |
| Record Nr. | UNINA-9910376615003321 |
Girard Antoine
|
||
| [Place of publication not identified], : ACM, 2015 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings, Part II / / edited by Sriram Sankaranarayanan, Natasha Sharygina
| Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings, Part II / / edited by Sriram Sankaranarayanan, Natasha Sharygina |
| Edizione | [1st ed. 2023.] |
| Pubbl/distr/stampa | Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2023 |
| Descrizione fisica | 1 online resource (xxiv, 604 pages) : illustrations (some color) |
| Disciplina | 005.1 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer science
Theory of Computation |
| ISBN | 3-031-30820-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Tool Demos -- EVA: a Tool for the Compositional Verification of AUTOSAR Models -- WASIM: A Word-level Abstract Symbolic Simulation Framework for Hardware Formal Verification -- Multiparty Session Typing in Java, Deductively -- PyLTA: A Verification Tool for Parameterized Distributed Algorithms -- FuzzBtor2: A Random Generator of Word-Level Model Checking Problems in Btor2 Format -- Eclipse ESCET™: The Eclipse Supervisory Control Engineering Toolkit -- Combinatorial Optimization/Theorem Proving -- New Core-Guided and Hitting Set Algorithms for Multi-Objective Combinatorial Optimization -- Verified reductions for optimization -- Specifying and Verifying Higher-order Rust Iterators -- Extending a High-Performance Prover to Higher-Order Logic -- Tools (Regular Papers) -- The WhyRel Prototype for Relational Verification of Pointer Programs -- Bridging Hardware and Software Analysis with Btor2C: A Word-Level-Circuit-to-C Converter -- CoPTIC: Constraint Programming Translated Into C -- Acacia-Bonsai: A Modern Implementation of Downset-Based LTL Realizability -- Synthesis -- Computing Adequately Permissive Assumptions for Synthesis -- Verification-guided Programmatic Controller Synthesis -- Taming Large Bounds in Synthesis from Bounded-Liveness Specifications -- Lockstep Composition for Unbalanced Loops -- Synthesis of Distributed Agreement-Based Systems with Effciently Decidable Verification -- LTL Reactive Synthesis with a Few Hints -- Timed Automata Verification and Synthesis via Finite Automata Learning -- Graphs/Probabilistic Systems -- A Truly Symbolic Linear-Time Algorithm for SCC Decomposition -- Transforming quantified Boolean formulas using biclique covers -- Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration -- Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants -- Runtime Monitoring/Program Analysis -- Industrial-Strength Controlled Concurrency Testing for C# Programs with Coyote -- Context-Sensitive Meta-Constraint Systems for Explainable Program Analysis -- Explainable Online Monitoring of Metric Temporal Logic -- 12th Competition on Software Verification — SV-COMP 2023 -- Competition on Software Verification and Witness Validation: SV-COMP 2023 -- Symbiotic-Witch 2: More Efficient Algorithm and Witness Refutation (Competition Contribution) -- 2LS: Arrays and Loop Unwinding (Competition Contribution) -- Bubaak: Runtime Monitoring of Program Verifiers (Competition Contribution) -- EBF 4.2: Black-Box Cooperative Verification for Concurrent Programs (Competition Contribution) -- Goblint: Autotuning Thread-Modular Abstract Interpretation (Competition Contribution) -- Java Ranger: Supporting String and Array Operations (Competition Contribution) -- Korn–Software Verification with Horn Clauses (Competition Contribution) -- Mopsa-C: Modular Domains and Relational Abstract Interpretation for C Programs (Competition Contribution) -- PIChecker: A POR and Interpolation based Verifier for Concurrent Programs (Competition Contribution) -- Ultimate Automizer and the CommuHash Normal Form (Competition Contribution) -- Ultimate Taipan and Race Detection in Ultimate (Competition Contribution) -- VeriAbsL: Scalable Verification by Abstraction and Strategy Prediction (Competition Contribution) -- VeriFuzz 1.4: Checking for (Non-)termination (Competition Contribution). . |
| Record Nr. | UNINA-9910717415003321 |
| Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2023 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings, Part I / / edited by Sriram Sankaranarayanan, Natasha Sharygina
| Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings, Part I / / edited by Sriram Sankaranarayanan, Natasha Sharygina |
| Edizione | [1st ed. 2023.] |
| Pubbl/distr/stampa | Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2023 |
| Descrizione fisica | 1 online resource (xxiii, 708 pages) : illustrations (some color) |
| Disciplina | 005.1 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer science
Theory of Computation |
| ISBN | 3-031-30823-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talk.-A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems -- Model Checking -- Bounded Model Checking for Asynchronous Hyperproperties -- Model Checking Linear Dynamical Systems under Floating-point Rounding -- Efficient Loop Conditions for Bounded Model Checking Hyperproperties -- Reconciling Preemption Bounding with DPOR -- Optimal Stateless Model Checking for Causal Consistency -- Symbolic Model Checking for TLA+ Made Faster -- AutoHyper: Explicit-State Model Checking for HyperLTL -- Machine Learning/Neural Networks -- Feature Necessity & Relevancy in ML Classifier Explanations -- Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks -- OccRob: Effcient SMT-Based Occlusion Robustness Verification of Deep Neural Networks -- Neural Network-Guided Synthesis of Recursive List Functions -- Automata -- Modular Mix-and-Match Complementation of Buechi automata -- Validating Streaming JSON Documents With Learned VPAs -- Antichains Algorithms for the Inclusion Problem Between ω -VPL -- Stack-Aware Hyperproperties -- Proofs -- Propositional Proof Skeletons -- Unsatisfiability Proofs for Distributed Clause-Sharing SAT Solvers -- Carcara: An effcient proof checker and elaborator for SMT proofs in the Alethe format -- Constraint Solving/Blockchain -- The Packing Chromatic Number of the Infinite Square Grid is 15 -- Active Learning for SAT Solver Benchmarking -- ParaQooba: A Fast and Flexible Framework for Parallel and Distributed QBF Solving -- Inferring Needless Write Memory Accesses on Ethereum Bytecode -- Markov Chains/Stochastic Control -- A Practitioner’s Guide to MDP Model Checking Algorithms -- Correct Approximation of Stationary Distributions -- Robust Almost-Sure Reachability in Multi-Environment MDPs -- Mungojerrie: Linear-Time Objectives in Model-Free Reinforcement Learning -- Verification -- A Formal CHERI-C Semantics for Verification -- Automated Verification for Real-Time Systems via Implicit Clocks and an Extended Antimirov Algorithm -- Parameterized Verification under TSO with Data Types -- Verifying Learning-Based Robotic Navigation Systems: A Case Study -- Make flows small again: revisiting the flow framework -- ALASCA: Reasoning in Quantified Linear Arithmetic -- A Matrix-Based Approach to Parity Games -- A GPU Tree Database for Many-Core Explicit State Space Exploration. |
| Record Nr. | UNINA-9910717415303321 |
| Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2023 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings, Part II / / edited by Sriram Sankaranarayanan, Natasha Sharygina
| Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings, Part II / / edited by Sriram Sankaranarayanan, Natasha Sharygina |
| Edizione | [1st ed. 2023.] |
| Pubbl/distr/stampa | Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2023 |
| Descrizione fisica | 1 online resource (xxiv, 604 pages) : illustrations (some color) |
| Disciplina | 005.1 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer science
Theory of Computation |
| ISBN | 3-031-30820-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Tool Demos -- EVA: a Tool for the Compositional Verification of AUTOSAR Models -- WASIM: A Word-level Abstract Symbolic Simulation Framework for Hardware Formal Verification -- Multiparty Session Typing in Java, Deductively -- PyLTA: A Verification Tool for Parameterized Distributed Algorithms -- FuzzBtor2: A Random Generator of Word-Level Model Checking Problems in Btor2 Format -- Eclipse ESCET™: The Eclipse Supervisory Control Engineering Toolkit -- Combinatorial Optimization/Theorem Proving -- New Core-Guided and Hitting Set Algorithms for Multi-Objective Combinatorial Optimization -- Verified reductions for optimization -- Specifying and Verifying Higher-order Rust Iterators -- Extending a High-Performance Prover to Higher-Order Logic -- Tools (Regular Papers) -- The WhyRel Prototype for Relational Verification of Pointer Programs -- Bridging Hardware and Software Analysis with Btor2C: A Word-Level-Circuit-to-C Converter -- CoPTIC: Constraint Programming Translated Into C -- Acacia-Bonsai: A Modern Implementation of Downset-Based LTL Realizability -- Synthesis -- Computing Adequately Permissive Assumptions for Synthesis -- Verification-guided Programmatic Controller Synthesis -- Taming Large Bounds in Synthesis from Bounded-Liveness Specifications -- Lockstep Composition for Unbalanced Loops -- Synthesis of Distributed Agreement-Based Systems with Effciently Decidable Verification -- LTL Reactive Synthesis with a Few Hints -- Timed Automata Verification and Synthesis via Finite Automata Learning -- Graphs/Probabilistic Systems -- A Truly Symbolic Linear-Time Algorithm for SCC Decomposition -- Transforming quantified Boolean formulas using biclique covers -- Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration -- Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants -- Runtime Monitoring/Program Analysis -- Industrial-Strength Controlled Concurrency Testing for C# Programs with Coyote -- Context-Sensitive Meta-Constraint Systems for Explainable Program Analysis -- Explainable Online Monitoring of Metric Temporal Logic -- 12th Competition on Software Verification — SV-COMP 2023 -- Competition on Software Verification and Witness Validation: SV-COMP 2023 -- Symbiotic-Witch 2: More Efficient Algorithm and Witness Refutation (Competition Contribution) -- 2LS: Arrays and Loop Unwinding (Competition Contribution) -- Bubaak: Runtime Monitoring of Program Verifiers (Competition Contribution) -- EBF 4.2: Black-Box Cooperative Verification for Concurrent Programs (Competition Contribution) -- Goblint: Autotuning Thread-Modular Abstract Interpretation (Competition Contribution) -- Java Ranger: Supporting String and Array Operations (Competition Contribution) -- Korn–Software Verification with Horn Clauses (Competition Contribution) -- Mopsa-C: Modular Domains and Relational Abstract Interpretation for C Programs (Competition Contribution) -- PIChecker: A POR and Interpolation based Verifier for Concurrent Programs (Competition Contribution) -- Ultimate Automizer and the CommuHash Normal Form (Competition Contribution) -- Ultimate Taipan and Race Detection in Ultimate (Competition Contribution) -- VeriAbsL: Scalable Verification by Abstraction and Strategy Prediction (Competition Contribution) -- VeriFuzz 1.4: Checking for (Non-)termination (Competition Contribution). . |
| Record Nr. | UNISA-996525668903316 |
| Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2023 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings, Part I / / edited by Sriram Sankaranarayanan, Natasha Sharygina
| Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings, Part I / / edited by Sriram Sankaranarayanan, Natasha Sharygina |
| Edizione | [1st ed. 2023.] |
| Pubbl/distr/stampa | Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2023 |
| Descrizione fisica | 1 online resource (xxiii, 708 pages) : illustrations (some color) |
| Disciplina | 005.1 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer science
Theory of Computation |
| ISBN | 3-031-30823-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talk.-A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems -- Model Checking -- Bounded Model Checking for Asynchronous Hyperproperties -- Model Checking Linear Dynamical Systems under Floating-point Rounding -- Efficient Loop Conditions for Bounded Model Checking Hyperproperties -- Reconciling Preemption Bounding with DPOR -- Optimal Stateless Model Checking for Causal Consistency -- Symbolic Model Checking for TLA+ Made Faster -- AutoHyper: Explicit-State Model Checking for HyperLTL -- Machine Learning/Neural Networks -- Feature Necessity & Relevancy in ML Classifier Explanations -- Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks -- OccRob: Effcient SMT-Based Occlusion Robustness Verification of Deep Neural Networks -- Neural Network-Guided Synthesis of Recursive List Functions -- Automata -- Modular Mix-and-Match Complementation of Buechi automata -- Validating Streaming JSON Documents With Learned VPAs -- Antichains Algorithms for the Inclusion Problem Between ω -VPL -- Stack-Aware Hyperproperties -- Proofs -- Propositional Proof Skeletons -- Unsatisfiability Proofs for Distributed Clause-Sharing SAT Solvers -- Carcara: An effcient proof checker and elaborator for SMT proofs in the Alethe format -- Constraint Solving/Blockchain -- The Packing Chromatic Number of the Infinite Square Grid is 15 -- Active Learning for SAT Solver Benchmarking -- ParaQooba: A Fast and Flexible Framework for Parallel and Distributed QBF Solving -- Inferring Needless Write Memory Accesses on Ethereum Bytecode -- Markov Chains/Stochastic Control -- A Practitioner’s Guide to MDP Model Checking Algorithms -- Correct Approximation of Stationary Distributions -- Robust Almost-Sure Reachability in Multi-Environment MDPs -- Mungojerrie: Linear-Time Objectives in Model-Free Reinforcement Learning -- Verification -- A Formal CHERI-C Semantics for Verification -- Automated Verification for Real-Time Systems via Implicit Clocks and an Extended Antimirov Algorithm -- Parameterized Verification under TSO with Data Types -- Verifying Learning-Based Robotic Navigation Systems: A Case Study -- Make flows small again: revisiting the flow framework -- ALASCA: Reasoning in Quantified Linear Arithmetic -- A Matrix-Based Approach to Parity Games -- A GPU Tree Database for Many-Core Explicit State Space Exploration. |
| Record Nr. | UNISA-996525668703316 |
| Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2023 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Video Atlas of Arthroscopic Rotator Cuff Repair / / by: Srikumaran, Uma
| Video Atlas of Arthroscopic Rotator Cuff Repair / / by: Srikumaran, Uma |
| Autore | Abboud Joseph A |
| Pubbl/distr/stampa | New York : , : Thieme, , [2021] |
| Descrizione fisica | 1 online resource (326 pages) : illustrations |
| Disciplina | 617.4720597 |
| Soggetto topico |
Arthroscopy
Shoulder joint - Rotator cuff - Surgery |
| Soggetto genere / forma | Atlas |
| ISBN |
1-63853-488-8
1-62623-713-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910794234303321 |
|
Abboud Joseph A
|
||
| New York : , : Thieme, , [2021] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Video Atlas of Arthroscopic Rotator Cuff Repair / / by: Srikumaran, Uma
| Video Atlas of Arthroscopic Rotator Cuff Repair / / by: Srikumaran, Uma |
| Autore | Abboud Joseph A |
| Pubbl/distr/stampa | New York : , : Thieme, , [2021] |
| Descrizione fisica | 1 online resource (326 pages) : illustrations |
| Disciplina | 617.4720597 |
| Soggetto topico |
Arthroscopy
Shoulder joint - Rotator cuff - Surgery |
| Soggetto genere / forma | Atlas |
| ISBN |
1-63853-488-8
1-62623-713-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910812294503321 |
|
Abboud Joseph A
|
||
| New York : , : Thieme, , [2021] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||