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.
The logic of software : a tasting menu of formal methods : essays dedicated to Reiner Hahnle on the occasion of his 60th birthday / / Wolfgang Ahrendt [and three others], editors
| The logic of software : a tasting menu of formal methods : essays dedicated to Reiner Hahnle on the occasion of his 60th birthday / / Wolfgang Ahrendt [and three others], editors |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2022] |
| Descrizione fisica | 1 online resource (531 pages) |
| Disciplina | 005.1015113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer logic
Computer logic - Study and teaching |
| ISBN | 3-031-08166-8 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910580133903321 |
| Cham, Switzerland : , : Springer, , [2022] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
The logic of software : a tasting menu of formal methods : essays dedicated to Reiner Hahnle on the occasion of his 60th birthday / / Wolfgang Ahrendt [and three others], editors
| The logic of software : a tasting menu of formal methods : essays dedicated to Reiner Hahnle on the occasion of his 60th birthday / / Wolfgang Ahrendt [and three others], editors |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2022] |
| Descrizione fisica | 1 online resource (531 pages) |
| Disciplina | 005.1015113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer logic
Computer logic - Study and teaching |
| ISBN | 3-031-08166-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISA-996483165003316 |
| Cham, Switzerland : , : Springer, , [2022] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Rewriting logic and its applications : 14th International Workshop, WRLA 2022, Munich, Germany, April 2-3, 2022, revised selected papers / / Kyungmin Bae
| Rewriting logic and its applications : 14th International Workshop, WRLA 2022, Munich, Germany, April 2-3, 2022, revised selected papers / / Kyungmin Bae |
| Autore | Bae Kyungmin |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer International Publishing, , [2022] |
| Descrizione fisica | 1 online resource (299 pages) |
| Disciplina | 005.1015113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer logic
Computer logic - Study and teaching |
| ISBN |
9783031124419
9783031124402 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Contents -- Invited Papers -- From Static to Dynamic Analysis and Allocation of Resources for BPMN Processes -- 1 Introduction -- 2 BPMN with Time and Resources -- 3 Static Quantitative Analysis -- 3.1 Process Description -- 3.2 Execution Semantics -- 3.3 Properties -- 3.4 Example -- 4 Dynamic Quantitative Analysis -- 4.1 Instrumentation -- 4.2 Computation of Properties -- 4.3 Dynamic Resource Allocation -- 4.4 Example -- 5 Related Work -- 6 Concluding Remarks -- References -- Rewriting Privacy -- 1 Introduction -- 2 Alpha-Beta Privacy for a Fixed State -- 2.1 The State Space -- 2.2 Example -- 2.3 Message Analysis Problems -- 3 Applications in Vote Privacy -- 3.1 Receipt Freeness -- 3.2 Stability Under Background Knowledge -- 4 Privacy as Reachability -- 4.1 Example: AF2 -- 4.2 Semantics -- 5 Conclusions and Outlook -- References -- Invited Tutorials and Experience Report -- Canonical Narrowing with Irreducibility and SMT Constraints as a Generic Symbolic Protocol Analysis Method -- 1 Introduction -- 2 Preliminaries -- 3 Canonical Narrowing with Irreducibility and SMT Constraints -- 4 Implementation -- 4.1 Our Previous Narrowing Command -- 4.2 Using Conditional Rules in Narrowing -- 4.3 Extension to Handle SMT Constraints -- 4.4 Variable Consistency -- 5 Experiments -- 5.1 Handling SMT Constraints -- 5.2 Brands and Chaum with Time -- 5.3 Brands and Chaum with Time and Space -- 6 Conclusions and Future Work -- References -- An Overview of the Maude Strategy Language and its Applications -- 1 Introduction -- 2 A Brief Introduction to the Maude Strategy Language -- 3 Some Examples -- 3.1 Deduction Procedures -- 3.2 Semantics of Programming Languages -- 3.3 Games -- 3.4 Other Examples -- 4 Related Tools and Extensions -- 4.1 Model Checking -- 4.2 Reflective Manipulation of Strategies.
4.3 A Probabilistic Extension -- 5 Conclusions -- References -- Teaching Formal Methods to Undergraduate Students Using Maude -- 1 Introduction -- 2 Setting and Challenges -- 3 How to Teach Formal Methods? -- 3.1 A Few Papers on Teaching Formal Methods. -- 3.2 What to Teach? -- 4 Why Teaching Formal Methods Using Maude? -- 5 Course and Textbook Content -- 5.1 Part I: Equational Specification in Maude and Term Rewrite Theory -- 5.2 Equational Logic (1 lecture) -- 5.3 Part II: Modeling and Analysis of Dynamic/Distributed Systems Using Rewriting Logic -- 6 Evaluation -- 6.1 Summary of Student Feedback -- 6.2 Selected Student Comments -- 7 Concluding Remarks -- References -- Regular Papers -- Business Processes Analysis with Resource-Aware Machine Learning Scheduling in Rewriting Logic -- 1 Introduction -- 2 The Business Process Modeling Notation (BPMN) -- 3 Using Long Short-Term Memory Neural Networks -- 4 Rewriting Logic Semantics with LSTM Integration -- 4.1 The Specification of BPMN Processes -- 4.2 Autonomous Processes -- 4.3 Event-Guided Processes -- 4.4 Resource Adaptation Based on LSTM Predictions -- 5 Case Study -- 6 Concluding Remarks -- References -- Modeling, Algorithm Synthesis, and Instrumentation for Co-simulation in Maude -- 1 Introduction -- 2 Preliminaries -- 2.1 Rewriting Logic and Maude -- 2.2 Co-simulation -- 3 Modeling Co-simulation Scenarios in Maude -- 4 Synthesizing and Executing Co-simulation Algorithms -- 4.1 Orchestration Data -- 4.2 Synthesis of Co-simulation Algorithms -- 4.3 Executing Co-Simulation Algorithms -- 4.4 Checking Confluence of Synthesized Co-simulation Algorithms -- 5 Synthesizing Instrumentations and SU Parameters -- 5.1 Instrumentation of a Scenario -- 5.2 Synthesizing SU Parameters -- 6 Related Work -- 7 Concluding Remarks -- References -- An Efficient Canonical Narrowing Implementation for Protocol Analysis. 1 Introduction -- 2 Preliminaries -- 3 Canonical Narrowing -- 4 Implementation -- 4.1 Using the Meta-level -- 4.2 Data Structures and the narrowing Command -- 4.3 Search for Solutions -- 4.4 Avoiding Variable Clashes -- 4.5 Algorithm Performance Improvement -- 5 Experiments -- 5.1 Experiments with the Vending Machine -- 5.2 Experiments with a Protocol Using the Exclusive-Or Property -- 5.3 Experiments Using the Properties of an Abelian Group -- 5.4 Experiments with the Vending Machine Using Idempotence -- 6 Conclusions -- References -- Checking Sufficient Completeness by Inductive Theorem Proving -- 1 Introduction -- 2 Preliminaries -- 3 A Hierarchical Methodology -- 4 Proving Sufficient Completeness Inductively -- 5 Some Examples -- 6 Related Work and Conclusions -- A Multiset Theory -- B Proofs -- References -- On Ground Convergence and Completeness of Conditional Equational Program Hierarchies -- 1 Introduction -- 2 Preliminaries -- 3 Proving Ground Convergence And Sufficient Completeness Hierarchically -- 4 Related Work and Conclusions -- A Proofs -- References -- Automating Safety Proofs About Cyber-Physical Systems Using Rewriting Modulo SMT -- 1 Introduction -- 2 Motivating Example -- 3 Symbolic Soft Agents Framework -- 3.1 Overview -- 3.2 The Structure of Soft Agent Rewriting -- 3.3 Symbolic Soft Agent Rewriting -- 4 Vehicle Specifications -- 4.1 Basic Symbolic Sorts -- 4.2 Knowledge Specifications -- 4.3 Soft-Constraint Controller -- 4.4 System Configurations -- 4.5 Safety Properties -- 4.6 Verifying Logical Scenarios -- 5 Trade-Offs Between Rewriting and Constraint Solving -- 6 Related Work -- 7 Conclusions -- References -- Executable Semantics and Type Checking for Session-Based Concurrency in Maude -- 1 Introduction -- 2 The Typed Process Model -- 3 Rewriting Semantics for s -- 4 Algorithmic Type Checking for s -- 4.1 Type Syntax. 4.2 Algorithmic Type Checking -- 4.3 Type Soundness -- 5 Lock and Deadlock Detection in Maude -- 5.1 Definitions -- 5.2 Examples -- 6 Closing Remarks -- References -- Tool Papers -- Parallel Maude-NPA for Cryptographic Protocol Analysis -- 1 Introduction -- 2 Preliminaries -- 3 Maude-NPA -- 4 Parallel Maude-NPA and Its Tool Support -- 5 Experiments -- 6 Related Work -- 7 Conclusion -- A The Number of States Located at Each Layer -- References -- Maude as a Library: An Efficient All-Purpose Programming Interface -- 1 Introduction -- 2 Overview of the Library -- 3 How to Use the Library, Illustrated by an Example -- 4 Advanced Features -- 4.1 Rewrite Graphs and Model Checking -- 4.2 Custom Special Operators -- 5 Implementation -- 5.1 Performance Considerations -- 6 Some Applications -- 6.1 Integration of Maude into the Robot Operating System -- 6.2 The Unified Maude Model Checker -- 7 Related Work -- 8 Conclusions -- References -- Author Index. |
| Record Nr. | UNISA-996483158703316 |
Bae Kyungmin
|
||
| Cham, Switzerland : , : Springer International Publishing, , [2022] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Rewriting logic and its applications : 14th International Workshop, WRLA 2022, Munich, Germany, April 2-3, 2022, revised selected papers / / Kyungmin Bae
| Rewriting logic and its applications : 14th International Workshop, WRLA 2022, Munich, Germany, April 2-3, 2022, revised selected papers / / Kyungmin Bae |
| Autore | Bae Kyungmin |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer International Publishing, , [2022] |
| Descrizione fisica | 1 online resource (299 pages) |
| Disciplina | 005.1015113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer logic
Computer logic - Study and teaching |
| ISBN |
9783031124419
9783031124402 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Contents -- Invited Papers -- From Static to Dynamic Analysis and Allocation of Resources for BPMN Processes -- 1 Introduction -- 2 BPMN with Time and Resources -- 3 Static Quantitative Analysis -- 3.1 Process Description -- 3.2 Execution Semantics -- 3.3 Properties -- 3.4 Example -- 4 Dynamic Quantitative Analysis -- 4.1 Instrumentation -- 4.2 Computation of Properties -- 4.3 Dynamic Resource Allocation -- 4.4 Example -- 5 Related Work -- 6 Concluding Remarks -- References -- Rewriting Privacy -- 1 Introduction -- 2 Alpha-Beta Privacy for a Fixed State -- 2.1 The State Space -- 2.2 Example -- 2.3 Message Analysis Problems -- 3 Applications in Vote Privacy -- 3.1 Receipt Freeness -- 3.2 Stability Under Background Knowledge -- 4 Privacy as Reachability -- 4.1 Example: AF2 -- 4.2 Semantics -- 5 Conclusions and Outlook -- References -- Invited Tutorials and Experience Report -- Canonical Narrowing with Irreducibility and SMT Constraints as a Generic Symbolic Protocol Analysis Method -- 1 Introduction -- 2 Preliminaries -- 3 Canonical Narrowing with Irreducibility and SMT Constraints -- 4 Implementation -- 4.1 Our Previous Narrowing Command -- 4.2 Using Conditional Rules in Narrowing -- 4.3 Extension to Handle SMT Constraints -- 4.4 Variable Consistency -- 5 Experiments -- 5.1 Handling SMT Constraints -- 5.2 Brands and Chaum with Time -- 5.3 Brands and Chaum with Time and Space -- 6 Conclusions and Future Work -- References -- An Overview of the Maude Strategy Language and its Applications -- 1 Introduction -- 2 A Brief Introduction to the Maude Strategy Language -- 3 Some Examples -- 3.1 Deduction Procedures -- 3.2 Semantics of Programming Languages -- 3.3 Games -- 3.4 Other Examples -- 4 Related Tools and Extensions -- 4.1 Model Checking -- 4.2 Reflective Manipulation of Strategies.
4.3 A Probabilistic Extension -- 5 Conclusions -- References -- Teaching Formal Methods to Undergraduate Students Using Maude -- 1 Introduction -- 2 Setting and Challenges -- 3 How to Teach Formal Methods? -- 3.1 A Few Papers on Teaching Formal Methods. -- 3.2 What to Teach? -- 4 Why Teaching Formal Methods Using Maude? -- 5 Course and Textbook Content -- 5.1 Part I: Equational Specification in Maude and Term Rewrite Theory -- 5.2 Equational Logic (1 lecture) -- 5.3 Part II: Modeling and Analysis of Dynamic/Distributed Systems Using Rewriting Logic -- 6 Evaluation -- 6.1 Summary of Student Feedback -- 6.2 Selected Student Comments -- 7 Concluding Remarks -- References -- Regular Papers -- Business Processes Analysis with Resource-Aware Machine Learning Scheduling in Rewriting Logic -- 1 Introduction -- 2 The Business Process Modeling Notation (BPMN) -- 3 Using Long Short-Term Memory Neural Networks -- 4 Rewriting Logic Semantics with LSTM Integration -- 4.1 The Specification of BPMN Processes -- 4.2 Autonomous Processes -- 4.3 Event-Guided Processes -- 4.4 Resource Adaptation Based on LSTM Predictions -- 5 Case Study -- 6 Concluding Remarks -- References -- Modeling, Algorithm Synthesis, and Instrumentation for Co-simulation in Maude -- 1 Introduction -- 2 Preliminaries -- 2.1 Rewriting Logic and Maude -- 2.2 Co-simulation -- 3 Modeling Co-simulation Scenarios in Maude -- 4 Synthesizing and Executing Co-simulation Algorithms -- 4.1 Orchestration Data -- 4.2 Synthesis of Co-simulation Algorithms -- 4.3 Executing Co-Simulation Algorithms -- 4.4 Checking Confluence of Synthesized Co-simulation Algorithms -- 5 Synthesizing Instrumentations and SU Parameters -- 5.1 Instrumentation of a Scenario -- 5.2 Synthesizing SU Parameters -- 6 Related Work -- 7 Concluding Remarks -- References -- An Efficient Canonical Narrowing Implementation for Protocol Analysis. 1 Introduction -- 2 Preliminaries -- 3 Canonical Narrowing -- 4 Implementation -- 4.1 Using the Meta-level -- 4.2 Data Structures and the narrowing Command -- 4.3 Search for Solutions -- 4.4 Avoiding Variable Clashes -- 4.5 Algorithm Performance Improvement -- 5 Experiments -- 5.1 Experiments with the Vending Machine -- 5.2 Experiments with a Protocol Using the Exclusive-Or Property -- 5.3 Experiments Using the Properties of an Abelian Group -- 5.4 Experiments with the Vending Machine Using Idempotence -- 6 Conclusions -- References -- Checking Sufficient Completeness by Inductive Theorem Proving -- 1 Introduction -- 2 Preliminaries -- 3 A Hierarchical Methodology -- 4 Proving Sufficient Completeness Inductively -- 5 Some Examples -- 6 Related Work and Conclusions -- A Multiset Theory -- B Proofs -- References -- On Ground Convergence and Completeness of Conditional Equational Program Hierarchies -- 1 Introduction -- 2 Preliminaries -- 3 Proving Ground Convergence And Sufficient Completeness Hierarchically -- 4 Related Work and Conclusions -- A Proofs -- References -- Automating Safety Proofs About Cyber-Physical Systems Using Rewriting Modulo SMT -- 1 Introduction -- 2 Motivating Example -- 3 Symbolic Soft Agents Framework -- 3.1 Overview -- 3.2 The Structure of Soft Agent Rewriting -- 3.3 Symbolic Soft Agent Rewriting -- 4 Vehicle Specifications -- 4.1 Basic Symbolic Sorts -- 4.2 Knowledge Specifications -- 4.3 Soft-Constraint Controller -- 4.4 System Configurations -- 4.5 Safety Properties -- 4.6 Verifying Logical Scenarios -- 5 Trade-Offs Between Rewriting and Constraint Solving -- 6 Related Work -- 7 Conclusions -- References -- Executable Semantics and Type Checking for Session-Based Concurrency in Maude -- 1 Introduction -- 2 The Typed Process Model -- 3 Rewriting Semantics for s -- 4 Algorithmic Type Checking for s -- 4.1 Type Syntax. 4.2 Algorithmic Type Checking -- 4.3 Type Soundness -- 5 Lock and Deadlock Detection in Maude -- 5.1 Definitions -- 5.2 Examples -- 6 Closing Remarks -- References -- Tool Papers -- Parallel Maude-NPA for Cryptographic Protocol Analysis -- 1 Introduction -- 2 Preliminaries -- 3 Maude-NPA -- 4 Parallel Maude-NPA and Its Tool Support -- 5 Experiments -- 6 Related Work -- 7 Conclusion -- A The Number of States Located at Each Layer -- References -- Maude as a Library: An Efficient All-Purpose Programming Interface -- 1 Introduction -- 2 Overview of the Library -- 3 How to Use the Library, Illustrated by an Example -- 4 Advanced Features -- 4.1 Rewrite Graphs and Model Checking -- 4.2 Custom Special Operators -- 5 Implementation -- 5.1 Performance Considerations -- 6 Some Applications -- 6.1 Integration of Maude into the Robot Operating System -- 6.2 The Unified Maude Model Checker -- 7 Related Work -- 8 Conclusions -- References -- Author Index. |
| Record Nr. | UNINA-9910585971503321 |
|
Bae Kyungmin
|
||
| Cham, Switzerland : , : Springer International Publishing, , [2022] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
