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.
Fundamental Approaches to Software Engineering [[electronic resource] ] : 24th International Conference, FASE 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021, Proceedings / / edited by Esther Guerra, Mariëlle Stoelinga
| Fundamental Approaches to Software Engineering [[electronic resource] ] : 24th International Conference, FASE 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021, Proceedings / / edited by Esther Guerra, Mariëlle Stoelinga |
| Autore | Guerra Esther |
| Edizione | [1st ed. 2021.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2021 |
| Descrizione fisica | 1 online resource (383 pages) |
| Disciplina | 005.1 |
| Altri autori (Persone) | StoelingaMariëlle |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Data structures (Computer science) Information theory Natural language processing (Computer science) Computer programming Computer science Software Engineering Data Structures and Information Theory Natural Language Processing (NLP) Programming Techniques Theory of Computation |
| ISBN | 3-030-71500-0 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | FASE Contributions -- On Benchmarking for Concurrent Runtime Verification -- Certified Abstract Cost Analysis -- Bootstrapping Automated Testing for RESTful Web Services -- A Decision Tree Lifted Domain for Analyzing Program Families with Numerical Features -- Finding a Universal Execution Strategy for Model Transformation Networks -- CoVEGI: Cooperative Veri cation via Externally Generated Invariants -- Engineering Secure Self-Adaptive Systems with Bayesian Games -- An Abstract Contract Theory for Programs with Procedures -- Paracosm: A Test Framework for Autonomous Driving Simulations -- Compositional Analysis of Probabilistic Timed Graph Transformation Systems -- Efficient Bounded Model Checking of Heap-Manipulating Programs using Tight Field Bounds -- Effects of Program Representation on Pointer Analyses - An Empirical Study -- Keeping Pace with the History of Evolving Runtime Models -- SpecTest: Specification-Based Compiler Testing -- PASTA: An Efficient Proactive Adaptation Approach Based on Statistical Model Checking for Self-Adaptive Systems -- Understanding Local Robustness of Deep Neural Networks under Natural Variations -- Test-Comp Contributions -- Status Report on Software Testing: Test-Comp 2021 -- CoVeriTest with Adaptive Time Scheduling (Competition Contribution) -- FuSeBMC: A White-Box Fuzzer for Finding Security Vulnerabilities in C Programs (Competition Contribution) -- Symbiotic 8: Parallel and Targeted Test Generation (Competition Contribution). |
| Record Nr. | UNISA-996464405903316 |
Guerra Esther
|
||
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2021 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Fundamental Approaches to Software Engineering : 24th International Conference, FASE 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021, Proceedings / / edited by Esther Guerra, Mariëlle Stoelinga
| Fundamental Approaches to Software Engineering : 24th International Conference, FASE 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021, Proceedings / / edited by Esther Guerra, Mariëlle Stoelinga |
| Autore | Guerra Esther |
| Edizione | [1st ed. 2021.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2021 |
| Descrizione fisica | 1 online resource (383 pages) |
| Disciplina | 005.1 |
| Altri autori (Persone) | StoelingaMariëlle |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Data structures (Computer science) Information theory Natural language processing (Computer science) Computer programming Computer science Software Engineering Data Structures and Information Theory Natural Language Processing (NLP) Programming Techniques Theory of Computation |
| ISBN | 3-030-71500-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | FASE Contributions -- On Benchmarking for Concurrent Runtime Verification -- Certified Abstract Cost Analysis -- Bootstrapping Automated Testing for RESTful Web Services -- A Decision Tree Lifted Domain for Analyzing Program Families with Numerical Features -- Finding a Universal Execution Strategy for Model Transformation Networks -- CoVEGI: Cooperative Veri cation via Externally Generated Invariants -- Engineering Secure Self-Adaptive Systems with Bayesian Games -- An Abstract Contract Theory for Programs with Procedures -- Paracosm: A Test Framework for Autonomous Driving Simulations -- Compositional Analysis of Probabilistic Timed Graph Transformation Systems -- Efficient Bounded Model Checking of Heap-Manipulating Programs using Tight Field Bounds -- Effects of Program Representation on Pointer Analyses - An Empirical Study -- Keeping Pace with the History of Evolving Runtime Models -- SpecTest: Specification-Based Compiler Testing -- PASTA: An Efficient Proactive Adaptation Approach Based on Statistical Model Checking for Self-Adaptive Systems -- Understanding Local Robustness of Deep Neural Networks under Natural Variations -- Test-Comp Contributions -- Status Report on Software Testing: Test-Comp 2021 -- CoVeriTest with Adaptive Time Scheduling (Competition Contribution) -- FuSeBMC: A White-Box Fuzzer for Finding Security Vulnerabilities in C Programs (Competition Contribution) -- Symbiotic 8: Parallel and Targeted Test Generation (Competition Contribution). |
| Record Nr. | UNINA-9910473457103321 |
|
Guerra Esther
|
||
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2021 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
A journey from process algebra via timed automata to model learning : essays dedicated to Frits Vaandrager on the occasion of his 60th birthday / / edited by Nils Jansen, Mariëlle Stoelinga and Petra van den Bos
| A journey from process algebra via timed automata to model learning : essays dedicated to Frits Vaandrager on the occasion of his 60th birthday / / edited by Nils Jansen, Mariëlle Stoelinga and Petra van den Bos |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2022] |
| Descrizione fisica | 1 online resource (593 pages) |
| Disciplina | 004.0151 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Formal methods (Computer science)
Computer science - Mathematics |
| ISBN | 3-031-15629-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Contents -- Non-finite Axiomatisability Results via Reductions: CSP Parallel Composition and CCS Restriction -- 1 Introduction -- 2 Preliminaries -- 3 The Proof Strategy: Reduction Mappings -- 4 Axiomatisability Results for CSP Parallel Composition -- 4.1 The Languages BCCSPAp, BCCSPActp, BCCSPp and BCCSPp -- 4.2 The Negative Result for BCCSPAp -- 4.3 The Case of BCCSPp and the Negative Result for BCCSPp -- 4.4 The Case of BCCSPActp -- 5 The Case of Restriction -- 5.1 The Negative Result -- 5.2 The Reduction -- 6 Concluding Remarks -- References -- Operational Causality - Necessarily Sufficient and Sufficiently Necessary -- 1 Introduction -- 2 Preliminaries -- 3 Necessary and Sufficient Causes -- 3.1 Necessary Causes -- 3.2 Sufficient Causes -- 4 Finding Good Causes -- 4.1 Degrees of Sufficiency and Necessity -- 4.2 Weight-Minimal Necessary Causes -- 5 Conclusion -- References -- Axiomatizing Consciousness with Applications -- 1 Towards Consciousness -- 2 Consciousness as Discrete, Probabilistic-Computable Actor -- 3 Compound Consciousness -- 4 Self -- 5 Mindfulness: Mechanism and Application to ER -- 6 Suffering -- 6.1 Suffering as Pain -- 6.2 Suffering as Change -- 6.3 Suffering from Lack -- 7 Release: "3223379 Suffering and "3222378 Freedom -- 8 Freedom Paradox -- 9 Layers of Consciousness -- 10 Conclusion -- References -- Symmetric Transrationals: The Data Type and the Algorithmic Degree of its Equational Theory -- 1 Introduction -- 2 Basic Theory of Abstract Data Types -- 2.1 Expansions, Extensions, and Enlargements -- 3 The Symmetric Transfields -- 3.1 Algebra of Peripheral Numbers and their Equational Specification -- 3.2 Making a Symmetric Transfield -- 3.3 Making a Bounded Symmetric Transfield -- 4 Rationals and Transrationals -- 4.1 Transrationals and Bounded Transrationals.
4.2 Minimality of the Bounded Transrationals -- 5 One-One Degree of Equations in Symmetric Transrationals -- 5.1 The Diophantine Problem for the Rationals -- 5.2 Equational Theories -- 6 Concluding Remarks -- 6.1 Background on the Rationals and Their Enlargements -- 6.2 Practical Computer Arithmetics -- 6.3 Hybrid Systems -- References -- A Survey of Model Learning Techniques for Recurrent Neural Networks -- 1 Introduction -- 2 Recurrent Neural Networks as Language Acceptors -- 3 Model Learning for Recurrent Neural Networks -- 3.1 Answering Equivalence Queries Probably Approximately Correct -- 3.2 Equivalence Queries Inspired by Statistical Model Checking -- 3.3 An Abstraction Refinement Approach to Equivalence Queries -- 4 Explainability Beyond Regular Languages -- 5 Conclusion -- References -- Back-and-Forth in Space: On Logics and Bisimilarity in Closure Spaces -- 1 Introduction -- 2 Preliminaries -- 3 Bisimilarity for Closure Models -- 3.1 CM-bisimilarity -- 3.2 Logical Characterisation of CM-bisimilarity -- 4 CMC-bisimilarity for QdCMs -- 4.1 CMC-bisimilarity for QdCMs -- 4.2 Logical Characterisation of CMC-bisimilarity -- 5 CoPa-Bisimilarity for QdCM -- 5.1 CoPa-bisimilarity -- 5.2 Logical Characterisation of CoPa-bisimilarity -- 6 Conclusions -- References -- Better Automata Through Process Algebra -- 1 Introduction -- 2 Languages, Regular Expressions and Automata -- 2.1 Alphabets and Languages -- 2.2 Regular Expressions -- 2.3 Finite Automata -- 3 Kleene's Theorem -- 4 NFAs via Structural Operational Semantics -- 4.1 An Operational Semantics for Regular Expressions -- 4.2 Building Automata Using Acceptance and Transitions -- 4.3 Computing NFAs from Regular Expressions -- 5 Discussion -- 6 Conclusions and Directions for Future Work -- A SOS Rules for Acceptance and Transitions -- References. Family-Based Fingerprint Analysis: A Position Paper -- 1 Introduction -- 2 Software Fingerprinting -- 2.1 Model Learning -- 2.2 A Methodology and Taxonomy for Formal Fingerprint Analysis -- 3 Family-Based Fingerprint Analysis -- 3.1 Family-Based Modeling and Analysis -- 3.2 A Framework for Family-Based Fingerprint Analysis -- 3.3 Practical and Theoretical Implications -- 4 Final Remarks -- References -- What's in School? - Topic Maps for Secondary School Computer Science -- 1 Introduction -- 2 Computer Science Learning and Teaching Standards -- 3 Topic Maps -- 4 Model Checking Unit -- 5 Discussion and Conclusion -- References -- Tree-Based Adaptive Model Learning -- 1 Introduction -- 2 Preliminaries -- 2.1 Learning with a Classification Tree -- 3 Learning Evolving Systems Incrementally -- 3.1 Correctness and Termination -- 4 Experiments -- 5 Conclusion -- A Omitted Incremental Subroutines -- B Additional Experiment Graphs -- B.1 Mutation Benchmark -- B.2 Feature-Add Benchmark -- References -- From Languages to Behaviors and Back -- 1 Introduction -- 2 Preliminaries for Behavioral Systems -- 2.1 A Semantic Point of View -- 2.2 A Technical Point of View -- 3 Systems of Procedural Transition Systems -- 3.1 A Semantic Point of View -- 3.2 A Technical Point of View -- 4 Learning Systems of Procedural Transition Systems -- 4.1 A Semantic Point of View -- 4.2 A Technical Point of View -- 5 On Behaviors and Reductions to Well-Matched Languages -- 6 Evaluation -- 6.1 Benchmark Setup -- 6.2 Results -- 7 Related Work -- 8 Outlook and Future Work -- References -- The Quest for an Adequate Semantic Basis of Dense-Time Metric Temporal Logic -- 1 Introduction -- 2 Signal Duration Calculus -- 3 Formulae Differentiating Signal Classes -- 4 Conclusion -- References -- Equivalence Checking 40 Years After: A Review of Bisimulation Tools -- 1 Introduction. 2 Retrospective of the 1980s -- 2.1 Bisimulation Tools Based on Term Rewriting -- 2.2 Algorithms for Bisimulations on Finite-State Systems -- 2.3 Early Bisimulation Tools -- 3 Retrospective of the 1990s -- 3.1 New Algorithms for Bisimulations -- 3.2 Algorithms for On-the-Fly Verification -- 3.3 Algorithms for Symbolic Verification -- 3.4 Algorithms for Compositional Verification -- 3.5 Enhanced Bisimulation Tools -- 3.6 New Bisimulation Tools -- 3.7 Bisimulation Tools for Timed and Hybrid Systems -- 3.8 Bisimulation Tools for Probabilistic and Stochastic Systems -- 3.9 Bisimulation Tools for Mobile Systems -- 4 Retrospective of the 2000s -- 4.1 New Algorithm for Strong Bisimulation -- 4.2 New Bisimulation Tools -- 4.3 Bisimulation Tools Using On-the-Fly Verification -- 4.4 Bisimulation Tools Based on Compositional Verification -- 4.5 Bisimulation Tools Based on Parallel/Distributed Computing -- 4.6 Bisimulation Tools Based on Symbolic Verification -- 4.7 Bisimulation Tools for Timed Systems -- 4.8 Bisimulation Tools for Probabilistic and Stochastic Systems -- 5 Retrospective of the 2010s -- 5.1 New Bisimulation Tools -- 5.2 Bisimulation Tools for Probabilistic and Stochastic Systems -- 5.3 Bisimulation Tools for Mobile Systems -- 5.4 Bisimulation Tools Based on Parallel/Distributed Computing -- 5.5 Bisimulation Tools Based on Compositional Verification -- 5.6 Recent Results for Strong and Branching Bisimulations -- 6 Conclusion -- References -- Apartness and Distinguishing Formulas in Hennessy-Milner Logic -- 1 Introduction -- 2 Bisimulation and Apartness for LTSs -- 2.1 Hennessy-Milner Logic for Bisimulation -- 3 Weak Bisimulation and Apartness for LTSs -- 3.1 Hennessy-Milner Logic for Weak Bisimulation -- 4 Branching Bisimulation and Apartness for LTSs -- 4.1 Hennessy-Milner Logic for Branching Bisimulation -- 4.2 Examples. 4.3 Related and Further Work -- References -- Playing Wordle with Uppaal Stratego -- 1 Introduction -- 2 Wordle -- 3 Uppaal Stratego -- 4 Wordle in Uppaal Stratego -- 5 Evaluation -- 6 Conclusion -- References -- Using the Parallel ATerm Library for Parallel Model Checking and State Space Generation -- 1 Introduction -- 2 ATerm Library -- 3 State Space Generation -- 4 Model Checking via Boolean Equation Systems -- 5 Conclusion -- References -- Active Automata Learning as Black-Box Search and Lazy Partition Refinement -- 1 Introduction -- 2 Regular Languages and Automata -- 3 MAT Learning -- 4 The L Algorithm -- 5 Demonstration -- 6 Evaluation -- 7 Conclusion -- References -- A Reconstruction of Ewens' Sampling Formula via Lists of Coins -- 1 Introduction -- 2 The Challenge -- 3 Going Probabilistic -- 4 Adding a Mutation Rate Parameter -- 5 The Lengths of Coin Sequences -- 6 Multisets Instead of Lists -- References -- .26em plus .1em minus .1emRooted Divergence-Preserving Branching Bisimilarity is a Congruence: A Simpler Proof -- 1 Introduction -- 2 Finite-State CCS and Branching Bisimulation -- 3 Congruence for Finite-State Processes -- 4 Comparison with the Congruence Proof for a Traditional Definition -- 5 Extending the Proof to Full CCS? -- References -- Learning Language Intersections -- 1 Introduction -- 2 Strategies -- 2.1 The Word-by-Word Strategy -- 2.2 The Independent Strategy -- 2.3 The Machine-by-Machine Strategy -- 3 Prototype Implementation -- 3.1 The Membership Oracle Signature -- 3.2 An Adequate Equivalence Oracle -- 4 Empirical Evaluation -- 4.1 Setup -- 4.2 Summary -- 4.3 Detailed Results -- 5 Conclusion and Outlook -- References -- Runtime Verification of Compound Components with ComMA -- 1 Introduction -- 2 Interface Modeling and Monitoring -- 2.1 ComMA Interface Modeling -- 2.2 Interface Monitoring -- 3 Component Models. 3.1 Components with Functional Constraints. |
| Record Nr. | UNISA-996490365303316 |
| Cham, Switzerland : , : Springer, , [2022] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
A journey from process algebra via timed automata to model learning : essays dedicated to Frits Vaandrager on the occasion of his 60th birthday / / edited by Nils Jansen, Mariëlle Stoelinga and Petra van den Bos
| A journey from process algebra via timed automata to model learning : essays dedicated to Frits Vaandrager on the occasion of his 60th birthday / / edited by Nils Jansen, Mariëlle Stoelinga and Petra van den Bos |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2022] |
| Descrizione fisica | 1 online resource (593 pages) |
| Disciplina | 004.0151 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Formal methods (Computer science)
Computer science - Mathematics |
| ISBN | 3-031-15629-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Contents -- Non-finite Axiomatisability Results via Reductions: CSP Parallel Composition and CCS Restriction -- 1 Introduction -- 2 Preliminaries -- 3 The Proof Strategy: Reduction Mappings -- 4 Axiomatisability Results for CSP Parallel Composition -- 4.1 The Languages BCCSPAp, BCCSPActp, BCCSPp and BCCSPp -- 4.2 The Negative Result for BCCSPAp -- 4.3 The Case of BCCSPp and the Negative Result for BCCSPp -- 4.4 The Case of BCCSPActp -- 5 The Case of Restriction -- 5.1 The Negative Result -- 5.2 The Reduction -- 6 Concluding Remarks -- References -- Operational Causality - Necessarily Sufficient and Sufficiently Necessary -- 1 Introduction -- 2 Preliminaries -- 3 Necessary and Sufficient Causes -- 3.1 Necessary Causes -- 3.2 Sufficient Causes -- 4 Finding Good Causes -- 4.1 Degrees of Sufficiency and Necessity -- 4.2 Weight-Minimal Necessary Causes -- 5 Conclusion -- References -- Axiomatizing Consciousness with Applications -- 1 Towards Consciousness -- 2 Consciousness as Discrete, Probabilistic-Computable Actor -- 3 Compound Consciousness -- 4 Self -- 5 Mindfulness: Mechanism and Application to ER -- 6 Suffering -- 6.1 Suffering as Pain -- 6.2 Suffering as Change -- 6.3 Suffering from Lack -- 7 Release: "3223379 Suffering and "3222378 Freedom -- 8 Freedom Paradox -- 9 Layers of Consciousness -- 10 Conclusion -- References -- Symmetric Transrationals: The Data Type and the Algorithmic Degree of its Equational Theory -- 1 Introduction -- 2 Basic Theory of Abstract Data Types -- 2.1 Expansions, Extensions, and Enlargements -- 3 The Symmetric Transfields -- 3.1 Algebra of Peripheral Numbers and their Equational Specification -- 3.2 Making a Symmetric Transfield -- 3.3 Making a Bounded Symmetric Transfield -- 4 Rationals and Transrationals -- 4.1 Transrationals and Bounded Transrationals.
4.2 Minimality of the Bounded Transrationals -- 5 One-One Degree of Equations in Symmetric Transrationals -- 5.1 The Diophantine Problem for the Rationals -- 5.2 Equational Theories -- 6 Concluding Remarks -- 6.1 Background on the Rationals and Their Enlargements -- 6.2 Practical Computer Arithmetics -- 6.3 Hybrid Systems -- References -- A Survey of Model Learning Techniques for Recurrent Neural Networks -- 1 Introduction -- 2 Recurrent Neural Networks as Language Acceptors -- 3 Model Learning for Recurrent Neural Networks -- 3.1 Answering Equivalence Queries Probably Approximately Correct -- 3.2 Equivalence Queries Inspired by Statistical Model Checking -- 3.3 An Abstraction Refinement Approach to Equivalence Queries -- 4 Explainability Beyond Regular Languages -- 5 Conclusion -- References -- Back-and-Forth in Space: On Logics and Bisimilarity in Closure Spaces -- 1 Introduction -- 2 Preliminaries -- 3 Bisimilarity for Closure Models -- 3.1 CM-bisimilarity -- 3.2 Logical Characterisation of CM-bisimilarity -- 4 CMC-bisimilarity for QdCMs -- 4.1 CMC-bisimilarity for QdCMs -- 4.2 Logical Characterisation of CMC-bisimilarity -- 5 CoPa-Bisimilarity for QdCM -- 5.1 CoPa-bisimilarity -- 5.2 Logical Characterisation of CoPa-bisimilarity -- 6 Conclusions -- References -- Better Automata Through Process Algebra -- 1 Introduction -- 2 Languages, Regular Expressions and Automata -- 2.1 Alphabets and Languages -- 2.2 Regular Expressions -- 2.3 Finite Automata -- 3 Kleene's Theorem -- 4 NFAs via Structural Operational Semantics -- 4.1 An Operational Semantics for Regular Expressions -- 4.2 Building Automata Using Acceptance and Transitions -- 4.3 Computing NFAs from Regular Expressions -- 5 Discussion -- 6 Conclusions and Directions for Future Work -- A SOS Rules for Acceptance and Transitions -- References. Family-Based Fingerprint Analysis: A Position Paper -- 1 Introduction -- 2 Software Fingerprinting -- 2.1 Model Learning -- 2.2 A Methodology and Taxonomy for Formal Fingerprint Analysis -- 3 Family-Based Fingerprint Analysis -- 3.1 Family-Based Modeling and Analysis -- 3.2 A Framework for Family-Based Fingerprint Analysis -- 3.3 Practical and Theoretical Implications -- 4 Final Remarks -- References -- What's in School? - Topic Maps for Secondary School Computer Science -- 1 Introduction -- 2 Computer Science Learning and Teaching Standards -- 3 Topic Maps -- 4 Model Checking Unit -- 5 Discussion and Conclusion -- References -- Tree-Based Adaptive Model Learning -- 1 Introduction -- 2 Preliminaries -- 2.1 Learning with a Classification Tree -- 3 Learning Evolving Systems Incrementally -- 3.1 Correctness and Termination -- 4 Experiments -- 5 Conclusion -- A Omitted Incremental Subroutines -- B Additional Experiment Graphs -- B.1 Mutation Benchmark -- B.2 Feature-Add Benchmark -- References -- From Languages to Behaviors and Back -- 1 Introduction -- 2 Preliminaries for Behavioral Systems -- 2.1 A Semantic Point of View -- 2.2 A Technical Point of View -- 3 Systems of Procedural Transition Systems -- 3.1 A Semantic Point of View -- 3.2 A Technical Point of View -- 4 Learning Systems of Procedural Transition Systems -- 4.1 A Semantic Point of View -- 4.2 A Technical Point of View -- 5 On Behaviors and Reductions to Well-Matched Languages -- 6 Evaluation -- 6.1 Benchmark Setup -- 6.2 Results -- 7 Related Work -- 8 Outlook and Future Work -- References -- The Quest for an Adequate Semantic Basis of Dense-Time Metric Temporal Logic -- 1 Introduction -- 2 Signal Duration Calculus -- 3 Formulae Differentiating Signal Classes -- 4 Conclusion -- References -- Equivalence Checking 40 Years After: A Review of Bisimulation Tools -- 1 Introduction. 2 Retrospective of the 1980s -- 2.1 Bisimulation Tools Based on Term Rewriting -- 2.2 Algorithms for Bisimulations on Finite-State Systems -- 2.3 Early Bisimulation Tools -- 3 Retrospective of the 1990s -- 3.1 New Algorithms for Bisimulations -- 3.2 Algorithms for On-the-Fly Verification -- 3.3 Algorithms for Symbolic Verification -- 3.4 Algorithms for Compositional Verification -- 3.5 Enhanced Bisimulation Tools -- 3.6 New Bisimulation Tools -- 3.7 Bisimulation Tools for Timed and Hybrid Systems -- 3.8 Bisimulation Tools for Probabilistic and Stochastic Systems -- 3.9 Bisimulation Tools for Mobile Systems -- 4 Retrospective of the 2000s -- 4.1 New Algorithm for Strong Bisimulation -- 4.2 New Bisimulation Tools -- 4.3 Bisimulation Tools Using On-the-Fly Verification -- 4.4 Bisimulation Tools Based on Compositional Verification -- 4.5 Bisimulation Tools Based on Parallel/Distributed Computing -- 4.6 Bisimulation Tools Based on Symbolic Verification -- 4.7 Bisimulation Tools for Timed Systems -- 4.8 Bisimulation Tools for Probabilistic and Stochastic Systems -- 5 Retrospective of the 2010s -- 5.1 New Bisimulation Tools -- 5.2 Bisimulation Tools for Probabilistic and Stochastic Systems -- 5.3 Bisimulation Tools for Mobile Systems -- 5.4 Bisimulation Tools Based on Parallel/Distributed Computing -- 5.5 Bisimulation Tools Based on Compositional Verification -- 5.6 Recent Results for Strong and Branching Bisimulations -- 6 Conclusion -- References -- Apartness and Distinguishing Formulas in Hennessy-Milner Logic -- 1 Introduction -- 2 Bisimulation and Apartness for LTSs -- 2.1 Hennessy-Milner Logic for Bisimulation -- 3 Weak Bisimulation and Apartness for LTSs -- 3.1 Hennessy-Milner Logic for Weak Bisimulation -- 4 Branching Bisimulation and Apartness for LTSs -- 4.1 Hennessy-Milner Logic for Branching Bisimulation -- 4.2 Examples. 4.3 Related and Further Work -- References -- Playing Wordle with Uppaal Stratego -- 1 Introduction -- 2 Wordle -- 3 Uppaal Stratego -- 4 Wordle in Uppaal Stratego -- 5 Evaluation -- 6 Conclusion -- References -- Using the Parallel ATerm Library for Parallel Model Checking and State Space Generation -- 1 Introduction -- 2 ATerm Library -- 3 State Space Generation -- 4 Model Checking via Boolean Equation Systems -- 5 Conclusion -- References -- Active Automata Learning as Black-Box Search and Lazy Partition Refinement -- 1 Introduction -- 2 Regular Languages and Automata -- 3 MAT Learning -- 4 The L Algorithm -- 5 Demonstration -- 6 Evaluation -- 7 Conclusion -- References -- A Reconstruction of Ewens' Sampling Formula via Lists of Coins -- 1 Introduction -- 2 The Challenge -- 3 Going Probabilistic -- 4 Adding a Mutation Rate Parameter -- 5 The Lengths of Coin Sequences -- 6 Multisets Instead of Lists -- References -- .26em plus .1em minus .1emRooted Divergence-Preserving Branching Bisimilarity is a Congruence: A Simpler Proof -- 1 Introduction -- 2 Finite-State CCS and Branching Bisimulation -- 3 Congruence for Finite-State Processes -- 4 Comparison with the Congruence Proof for a Traditional Definition -- 5 Extending the Proof to Full CCS? -- References -- Learning Language Intersections -- 1 Introduction -- 2 Strategies -- 2.1 The Word-by-Word Strategy -- 2.2 The Independent Strategy -- 2.3 The Machine-by-Machine Strategy -- 3 Prototype Implementation -- 3.1 The Membership Oracle Signature -- 3.2 An Adequate Equivalence Oracle -- 4 Empirical Evaluation -- 4.1 Setup -- 4.2 Summary -- 4.3 Detailed Results -- 5 Conclusion and Outlook -- References -- Runtime Verification of Compound Components with ComMA -- 1 Introduction -- 2 Interface Modeling and Monitoring -- 2.1 ComMA Interface Modeling -- 2.2 Interface Monitoring -- 3 Component Models. 3.1 Components with Functional Constraints. |
| Record Nr. | UNINA-9910592992603321 |
| Cham, Switzerland : , : Springer, , [2022] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||