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.
All About Maude - A High-Performance Logical Framework [[electronic resource] ] : How to Specify, Program, and Verify Systems in Rewriting Logic / / by Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott
| All About Maude - A High-Performance Logical Framework [[electronic resource] ] : How to Specify, Program, and Verify Systems in Rewriting Logic / / by Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott |
| Autore | Clavel Manuel |
| Edizione | [1st ed. 2007.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
| Descrizione fisica | 1 online resource (XXII, 802 p.) |
| Disciplina | 004.015113 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Programming languages (Electronic computers)
Computer programming Software engineering Artificial intelligence Mathematical logic Programming Languages, Compilers, Interpreters Programming Techniques Software Engineering Artificial Intelligence Mathematical Logic and Formal Languages |
| ISBN | 3-540-71999-7 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | I: Core Maude -- Using Maude -- Syntax and Basic Parsing -- Functional Modules -- A Hierarchy of Data Types: From Trees to Sets -- System Modules -- Playing with Maude -- Module Operations -- Predefined Data Modules -- Specifying Parameterized Data Structures in Maude -- Object-Based Programming -- Model Checking Invariants Through Search -- LTL Model Checking -- Reflection, Metalevel Computation, and Strategies -- Metaprogramming Applications -- Mobile Maude -- User Interfaces and Metalanguage Applications -- II: Full Maude -- Full Maude: Extending Core Maude -- Object-Oriented Modules -- III: Applications and Tools -- A Sampler of Application Areas -- Some Tools -- IV: Reference -- Debugging and Troubleshooting -- Complete List of Maude Commands -- Core Maude Grammar. |
| Record Nr. | UNINA-9910484639403321 |
Clavel Manuel
|
||
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
All About Maude - A High-Performance Logical Framework [[electronic resource] ] : How to Specify, Program, and Verify Systems in Rewriting Logic / / by Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott
| All About Maude - A High-Performance Logical Framework [[electronic resource] ] : How to Specify, Program, and Verify Systems in Rewriting Logic / / by Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott |
| Autore | Clavel Manuel |
| Edizione | [1st ed. 2007.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
| Descrizione fisica | 1 online resource (XXII, 802 p.) |
| Disciplina | 004.015113 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Programming languages (Electronic computers)
Computer programming Software engineering Artificial intelligence Mathematical logic Programming Languages, Compilers, Interpreters Programming Techniques Software Engineering Artificial Intelligence Mathematical Logic and Formal Languages |
| ISBN | 3-540-71999-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | I: Core Maude -- Using Maude -- Syntax and Basic Parsing -- Functional Modules -- A Hierarchy of Data Types: From Trees to Sets -- System Modules -- Playing with Maude -- Module Operations -- Predefined Data Modules -- Specifying Parameterized Data Structures in Maude -- Object-Based Programming -- Model Checking Invariants Through Search -- LTL Model Checking -- Reflection, Metalevel Computation, and Strategies -- Metaprogramming Applications -- Mobile Maude -- User Interfaces and Metalanguage Applications -- II: Full Maude -- Full Maude: Extending Core Maude -- Object-Oriented Modules -- III: Applications and Tools -- A Sampler of Application Areas -- Some Tools -- IV: Reference -- Debugging and Troubleshooting -- Complete List of Maude Commands -- Core Maude Grammar. |
| Record Nr. | UNISA-996466336703316 |
|
Clavel Manuel
|
||
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Coordination Models and Languages [[electronic resource] ] : 5th International Conference, COORDINATION 2002, YORK, UK, April 8-11, 2002 Proceedings / / edited by Farhad Arbab, Carolyn Talcott
| Coordination Models and Languages [[electronic resource] ] : 5th International Conference, COORDINATION 2002, YORK, UK, April 8-11, 2002 Proceedings / / edited by Farhad Arbab, Carolyn Talcott |
| Edizione | [1st ed. 2002.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 |
| Descrizione fisica | 1 online resource (XII, 412 p.) |
| Disciplina | 004/.35 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Architecture, Computer
Programming languages (Electronic computers) Computer programming Computer communication systems Computers Software engineering Computer System Implementation Programming Languages, Compilers, Interpreters Programming Techniques Computer Communication Networks Computation by Abstract Devices Software Engineering |
| ISBN | 3-540-46000-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Presentations -- Playing Games with Software Design -- Coordination and System Design in a Network-Centric Age -- Time, Knowledge, and Cooperation: Alternating-Time Temporal Epistemic Logic and Its Applications -- Accepted Papers -- Coordination for Orchestration -- Concurrent Semantics for the Web Services Specification Language DAML-S -- Coordination through Channel Composition -- Exogenous and Endogenous Extensions of Architectural Types -- Coordinating Mobile Object-Oriented Code -- Formalizing Properties of Mobile Agent Systems -- Dynamically Adapting the Behaviour of Software Components -- An Associative Broadcast Based Coordination Model for Distributed Processes -- State—and Event-Based Reactive Programming in Shared Dataspaces -- Integrating Two Organizational Systems through Communication Genres -- OpenCoLaS a Coordination Framework for CoLaS Dialects -- Coordination in a Reflective Architecture Description Language -- Coordinating Software Evolution via Two-Tier Programming -- Criteria for the Analysis of Coordination in Multi-agent Applications -- Towards a Colimit-Based Semantics for Visual Programming -- The Cost of Communication Protocols and Coordination Languages in Embedded Systems -- Operational Semantics for Coordination in Paradigm -- Service Provision in Ad Hoc Networks -- PN2: An Elementary Model for Design and Analysis of Multi-agent Systems -- A Recovery Technique Using Multi-agent in Distributed Computing Systems -- An Order-Based, Distributed Algorithm for Implementing Multiparty Interactions -- Exploiting Transiently Shared Tuple Spaces for Location Transparent Code Mobility -- Formal Specification of JavaSpaces™ Architecture Using ?CRL -- Objective vs. Subjective Coordination in Agent-Based Systems: A Case Study -- Scheduling under Uncertainty: Planning for the Ubiquitous Grid -- Using Logical Operators as an Extended Coordination Mechanism in Linda -- A Framework for Coordinating Parallel Branch and Bound Algorithms -- Policies for Cooperative Virtual Teams -- The Spacetub Models and Framework -- Tuple-Based Models in the Observation Framework -- Extending the Matching Facilities of Linda -- Semantics of Protocol Modules Composition and Interaction. |
| Record Nr. | UNINA-9910143910003321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Coordination Models and Languages [[electronic resource] ] : 5th International Conference, COORDINATION 2002, YORK, UK, April 8-11, 2002 Proceedings / / edited by Farhad Arbab, Carolyn Talcott
| Coordination Models and Languages [[electronic resource] ] : 5th International Conference, COORDINATION 2002, YORK, UK, April 8-11, 2002 Proceedings / / edited by Farhad Arbab, Carolyn Talcott |
| Edizione | [1st ed. 2002.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 |
| Descrizione fisica | 1 online resource (XII, 412 p.) |
| Disciplina | 004/.35 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Architecture, Computer
Programming languages (Electronic computers) Computer programming Computer communication systems Computers Software engineering Computer System Implementation Programming Languages, Compilers, Interpreters Programming Techniques Computer Communication Networks Computation by Abstract Devices Software Engineering |
| ISBN | 3-540-46000-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Presentations -- Playing Games with Software Design -- Coordination and System Design in a Network-Centric Age -- Time, Knowledge, and Cooperation: Alternating-Time Temporal Epistemic Logic and Its Applications -- Accepted Papers -- Coordination for Orchestration -- Concurrent Semantics for the Web Services Specification Language DAML-S -- Coordination through Channel Composition -- Exogenous and Endogenous Extensions of Architectural Types -- Coordinating Mobile Object-Oriented Code -- Formalizing Properties of Mobile Agent Systems -- Dynamically Adapting the Behaviour of Software Components -- An Associative Broadcast Based Coordination Model for Distributed Processes -- State—and Event-Based Reactive Programming in Shared Dataspaces -- Integrating Two Organizational Systems through Communication Genres -- OpenCoLaS a Coordination Framework for CoLaS Dialects -- Coordination in a Reflective Architecture Description Language -- Coordinating Software Evolution via Two-Tier Programming -- Criteria for the Analysis of Coordination in Multi-agent Applications -- Towards a Colimit-Based Semantics for Visual Programming -- The Cost of Communication Protocols and Coordination Languages in Embedded Systems -- Operational Semantics for Coordination in Paradigm -- Service Provision in Ad Hoc Networks -- PN2: An Elementary Model for Design and Analysis of Multi-agent Systems -- A Recovery Technique Using Multi-agent in Distributed Computing Systems -- An Order-Based, Distributed Algorithm for Implementing Multiparty Interactions -- Exploiting Transiently Shared Tuple Spaces for Location Transparent Code Mobility -- Formal Specification of JavaSpaces™ Architecture Using ?CRL -- Objective vs. Subjective Coordination in Agent-Based Systems: A Case Study -- Scheduling under Uncertainty: Planning for the Ubiquitous Grid -- Using Logical Operators as an Extended Coordination Mechanism in Linda -- A Framework for Coordinating Parallel Branch and Bound Algorithms -- Policies for Cooperative Virtual Teams -- The Spacetub Models and Framework -- Tuple-Based Models in the Observation Framework -- Extending the Matching Facilities of Linda -- Semantics of Protocol Modules Composition and Interaction. |
| Record Nr. | UNISA-996465410403316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Logic, Rewriting, and Concurrency [[electronic resource] ] : Essays Dedicated to José Meseguer on the Occasion of His 65th Birthday / / edited by Narciso Martí-Oliet, Peter Csaba Ölveczky, Carolyn Talcott
| Logic, Rewriting, and Concurrency [[electronic resource] ] : Essays Dedicated to José Meseguer on the Occasion of His 65th Birthday / / edited by Narciso Martí-Oliet, Peter Csaba Ölveczky, Carolyn Talcott |
| Edizione | [1st ed. 2015.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 |
| Descrizione fisica | 1 online resource (XI, 634 p. 103 illus.) |
| Disciplina | 621.395 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Machine theory
Computer science Compilers (Computer programs) Computer programming Software engineering Formal Languages and Automata Theory Computer Science Logic and Foundations of Programming Compilers and Interpreters Programming Techniques Software Engineering |
| ISBN | 3-319-23165-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Contents -- José Meseguer: Scientist and Friend Extraordinaire -- 1 José's Origins and Positions -- 2 José's Research -- 3 José the Person and Scientist -- 4 José's PhD Students -- References -- Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude -- 1 Introduction -- 2 Preliminaries -- 2.1 Search Tree Example -- 2.2 Membership Equational Logic -- 2.3 Unification -- 2.4 Rewriting Logic -- 2.5 Executable Rewrite Theories -- 2.6 Reachability Goals -- 2.7 Narrowing -- 3 Sentence-Normalized Rewriting -- 4 Conditional Narrowing Modulo Unification -- 4.1 Transformations and Calculus Rules for Unification -- 5 Reachability by Conditional Narrowing -- 5.1 Calculus Rules for Reachability -- 6 Example -- 7 Related Work, Conclusions and Future Work -- References -- Combining Runtime Checking and Slicing to Improve Maude Error Diagnosis -- 1 Introduction -- 2 Rewriting Logic and Maude -- 2.1 Preliminaries -- 2.2 Rewrite Theories and Maude Modules -- 2.3 Rewriting and Generalization Modulo Equational Theories -- 3 The Assertion Language -- 3.1 The Assertion Logic -- 3.2 System and Functional Assertions -- 4 Enhancing Trace Slicing -- 5 Integrating Assertion-Checking and Trace Slicing -- 5.1 Dynamic Assertion-Checking -- 5.2 Runtime Assertion-Based Backward Trace Slicing -- 5.3 The ABETS system -- 6 Conclusions and Further Work -- References -- Computer Modeling in Neuroscience: From Imperative to Declarative Programming -- Abstract -- 1 Introduction -- 2 Brief Survey of Imperative Models in Neuroscience -- 3 Declarative Model of Extinction of Fear Conditioning -- 3.1 Neurobiology of the Amygdala -- 3.2 Computational Approach Specifics -- 3.3 Analysis of the Model -- 3.4 Implications of Main Model Findings -- 4 New Approach in Computational Neuroscience -- References -- Hybrid Multirate PALS.
1 Introduction -- 2 Preliminaries on Multirate PALS -- 3 Specifying Physical Environments -- 3.1 Controlled Physical Environments -- 3.2 Correlating Physical Environments -- 4 Hybrid Multirate PALS -- 4.1 Environment-Restricted Synchronous Ensembles -- 4.2 Realizable Transition Sequences -- 4.3 Hybrid Multirate PALS Distributed Models -- 4.4 Relating the Synchronous and Asynchronous Models -- 5 Verifying Invariants Using SMT Solving -- 5.1 Logical Representations -- 5.2 Local Clocks and SMT Solving -- 6 Concluding Remarks -- References -- Debits and Credits in Petri Nets and Linear Logic -- 1 Introduction -- 2 Intuitionistic Linear Logic with Mix -- 2.1 Simple Products and Multisets -- 2.2 Horn ILLmix Sequents -- 3 Debit Nets -- 4 Debit Nets as a Model of Horn ILLmix -- 4.1 Big-Step Semantics -- 4.2 Small-Step Semantics -- 4.3 Encoding Horn ILLmix into Debit Nets -- 5 Related Work and Conclusions -- A Proofs -- A.1 Proofs for Sect.4.1 -- A.2 Proofs for Sect.4.2 -- A.3 Proofs for Sect.4.3 -- References -- Alice and Bob Meet Equational Theories -- 1 Introduction -- 2 Alice&Bob Protocol Notation -- 2.1 Overview -- 2.2 Messages and Message Model -- 2.3 Alice&Bob in Detail -- 3 From Equations to Rewriting Rules -- 3.1 Role Scripts for Protocols -- 3.2 Deciding Executability -- 3.3 Checking Received Messages -- 3.4 Putting It All Together -- 4 Automated Translation to Tamarin -- 5 Related Work -- 6 Conclusions -- References -- On First-Order Model-Based Reasoning -- 1 Introduction -- 2 Model-Based Reasoning in First-Order Logic -- 2.1 Semantic Resolution -- 2.2 Hypertableaux -- 2.3 Model-Based Transformation of Clause Sets -- 2.4 The Model Evolution Calculus -- 2.5 SGGS: Semantically-Guided Goal-Sensitive Reasoning -- 3 Model-Based Reasoning in First-Order Theories -- 3.1 Building Theory Axioms into Resolution and Superposition. 3.2 Hierarchical Reasoning by Superposition -- 3.3 Hierarchical Reasoning in Local Theory Extensions -- 3.4 Beyond SMT: Satisfiability Modulo Assignment and MCsat -- 4 Discussion -- References -- A Normal Form for Stateful Connectors -- 1 Introduction -- 2 Petri Calculi -- 2.1 The P/T Petri Calculus -- 2.2 The C/E Petri Calculus -- 3 Nets with Boundaries -- 3.1 P/T Petri Nets with Boundaries -- 3.2 From P/T Nets with Boundaries to P/T Calculus and Back -- 3.3 C/E Nets with Boundaries -- 4 Normal Forms for Finite State P/T terms -- 4.1 Finite (State and Transition) Marking Graphs -- 4.2 Stateless, Infinitely Branching Marking Graphs -- 4.3 Finite State and Infinitely Branching Marking Graph -- 5 Normal Forms for the C/E Petri Calculus -- 6 Concluding Remarks -- References -- Enlightening Ph.D. Students with the Elegance of Logic -- Abstract -- 1 Preface -- 2 My Research Direction Before Knowing Jos00E9 -- 3 Jos00E9's Course on Formal Methods -- 4 Face-to-Face Discussions with Jos00E9 -- 5 Our Collaborations After My Graduation -- 6 Long-Term Influence -- Acknowledgement -- Two Decades of Maude -- 1 The Origins -- 2 The Language -- 2.1 Generalized Rewrite Theories in Maude -- 2.2 Reflection in Maude -- 2.3 Maude's Formal Tools -- 3 The Present: Unification and Narrowing -- 4 The Near Future: Rewriting Modulo SMT -- 4.1 Maude SMT -- 4.2 Symbolic Analysis of Distance-Bounding Protocols -- 5 Pathway Logic -- 5.1 About Pathway Logic -- 5.2 Maude's Role in Pathway Logic -- 6 Further Ahead -- References -- Formal Universes -- 1 Introduction -- 2 Universalism I : Paradise Lost? -- 3 Universalism II : Paradise Regained? -- 4 Reductionism -- 5 Criticism -- 6 Rejoinder -- References -- When Is a Formula a Loop Invariant? -- 1 Introduction -- 2 Examples -- 3 Preliminaries -- 4 Inductive Strengthening Procedure -- 5 Application to Specific Logical Theories. 5.1 Polynomial Equalities -- 5.2 Linear Arithmetic -- 6 k-Induction and Strengthening -- 6.1 Strategy Approximation (IV) Can Often Be Effective -- 7 Related Work -- 8 Conclusions -- References -- Generic Proof Scores for Generate & Check Method in CafeOBJ -- 1 Introduction -- 2 Preliminaries -- 2.1 Transition Systems -- 2.2 Verification of Invariant Properties -- 2.3 Verification of (p Leads-to q) Properties -- 2.4 Generate and Check for st St -- 2.5 Built-in Search Predicate -- 2.6 Generate & Check for tr Tr -- 2.7 Generate&Check for Verification of Invariant Properties -- 2.8 Generate&Check for Verification of (p Leads-to q) Properties -- 2.9 System and Property Specifications, and Proof Scores -- 3 Generic Proof Scores for Generate & Check Method -- 3.1 GENcases: Generating Patterns and Checking on Them -- 3.2 Three Parameterized Modules for Invariant Properties -- 3.3 Four Parameterized Modules for (p Leads-to q) Properties -- 4 QLOCK Specifications -- 4.1 QLOCK System SpecificationsThe specifications explained in this section are in the file qlock-sys.cafe on the web page. -- 4.2 QLOCK Property SpecificationsThe modules in this section is in the file qlock-prop.cafe unless otherwise stated. -- 4.3 Extended State (State % Aid) and Possible Inductive Invariants -- 5 QLOCK Proof Scores -- 5.1 Proof Scores for Invariant Properties -- 5.2 Proof Scores for (p Leads-to q) Property -- 6 Conclusion -- 6.1 Related Works -- 6.2 Some Features of Generic Proof Scores, Generate & Check Method, and CafeOBJ -- 6.3 Future Issues -- References -- Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting -- 1 Introduction -- 2 Preliminaries -- 3 Minimal Non--Terminating Terms at Frozen Positions -- 4 Modeling the Unhiding Process Using Rules -- 4.1 A New Notion of Minimal Non--terminating Term -- 5 From Minimal Terms to the CS-DP Framework. 5.1 Context-Sensitive Dependency Pair Framework -- 6 Usable Rules in the CS-DP Framework -- 6.1 Strongly Minimal Terms -- 6.2 Left-Linearity and -Conservativity -- 6.3 Extended Basic CS Usable Rules -- 7 Experimental Evaluation -- 8 Conclusions -- References -- Model-Checking HELENA Ensembles with Spin -- 1 Introduction -- 2 Foundations on LTLX Preservation -- 3 The Helena Approach -- 4 HelenaLight -- 4.1 Syntax of HelenaLight Ensemble Specifications -- 4.2 Semantics of HelenaLight Ensemble Specifications -- 4.3 LTL for HelenaLight -- 5 PromelaLight -- 5.1 Syntax of PromelaLight Specifications -- 5.2 Semantics of PromelaLight Specifications -- 5.3 LTL for PromelaLight -- 6 Translation of HelenaLight to PromelaLight -- 7 -Stutter Equivalence of the Translation -- 8 Model-Checking HelenaLight with Spin -- 9 Conclusion -- References -- Modularity of Ontologies in an Arbitrary Institution -- 1 Introduction -- 2 Institutions -- 3 Conservative Extensions and Inseparability -- 4 Module Notions -- 5 Conclusions -- References -- Rewriting Strategies and Strategic Rewrite Programs -- 1 Introduction -- 2 Historical Considerations -- 3 What are Strategic Rewriting and Strategic Programs? -- 3.1 Rewriting -- 3.2 Strategic Rewrite Programs -- 3.3 Abstract Reduction System -- 3.4 Strategic Rewriting -- 4 Strategy Description: Different Points of View -- 4.1 Rewriting Logic -- 4.2 Rewriting Calculus -- 4.3 Extensional Strategies -- 4.4 Intensional Strategies -- 4.5 Positional Strategies -- 5 Strategy Languages -- 6 Operational Semantics of Strategic Programs -- 7 Properties of Strategic Rewriting -- 8 Conclusion and Further Work -- References -- Network-on-Chip Firewall: Countering Defective and Malicious System-on-Chip Hardware -- 1 Introduction -- 2 Background -- 3 Threat Model -- 4 Core-Based Isolation -- 5 NoCF Interposer Design -- 6 Prototype Implementation. 7 Constraining a Malicious GPU. |
| Record Nr. | UNISA-996200365103316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Logic, Rewriting, and Concurrency [[electronic resource] ] : Essays Dedicated to José Meseguer on the Occasion of His 65th Birthday / / edited by Narciso Martí-Oliet, Peter Csaba Ölveczky, Carolyn Talcott
| Logic, Rewriting, and Concurrency [[electronic resource] ] : Essays Dedicated to José Meseguer on the Occasion of His 65th Birthday / / edited by Narciso Martí-Oliet, Peter Csaba Ölveczky, Carolyn Talcott |
| Edizione | [1st ed. 2015.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 |
| Descrizione fisica | 1 online resource (XI, 634 p. 103 illus.) |
| Disciplina | 621.395 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Machine theory
Computer science Compilers (Computer programs) Computer programming Software engineering Formal Languages and Automata Theory Computer Science Logic and Foundations of Programming Compilers and Interpreters Programming Techniques Software Engineering |
| ISBN | 3-319-23165-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Contents -- José Meseguer: Scientist and Friend Extraordinaire -- 1 José's Origins and Positions -- 2 José's Research -- 3 José the Person and Scientist -- 4 José's PhD Students -- References -- Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude -- 1 Introduction -- 2 Preliminaries -- 2.1 Search Tree Example -- 2.2 Membership Equational Logic -- 2.3 Unification -- 2.4 Rewriting Logic -- 2.5 Executable Rewrite Theories -- 2.6 Reachability Goals -- 2.7 Narrowing -- 3 Sentence-Normalized Rewriting -- 4 Conditional Narrowing Modulo Unification -- 4.1 Transformations and Calculus Rules for Unification -- 5 Reachability by Conditional Narrowing -- 5.1 Calculus Rules for Reachability -- 6 Example -- 7 Related Work, Conclusions and Future Work -- References -- Combining Runtime Checking and Slicing to Improve Maude Error Diagnosis -- 1 Introduction -- 2 Rewriting Logic and Maude -- 2.1 Preliminaries -- 2.2 Rewrite Theories and Maude Modules -- 2.3 Rewriting and Generalization Modulo Equational Theories -- 3 The Assertion Language -- 3.1 The Assertion Logic -- 3.2 System and Functional Assertions -- 4 Enhancing Trace Slicing -- 5 Integrating Assertion-Checking and Trace Slicing -- 5.1 Dynamic Assertion-Checking -- 5.2 Runtime Assertion-Based Backward Trace Slicing -- 5.3 The ABETS system -- 6 Conclusions and Further Work -- References -- Computer Modeling in Neuroscience: From Imperative to Declarative Programming -- Abstract -- 1 Introduction -- 2 Brief Survey of Imperative Models in Neuroscience -- 3 Declarative Model of Extinction of Fear Conditioning -- 3.1 Neurobiology of the Amygdala -- 3.2 Computational Approach Specifics -- 3.3 Analysis of the Model -- 3.4 Implications of Main Model Findings -- 4 New Approach in Computational Neuroscience -- References -- Hybrid Multirate PALS.
1 Introduction -- 2 Preliminaries on Multirate PALS -- 3 Specifying Physical Environments -- 3.1 Controlled Physical Environments -- 3.2 Correlating Physical Environments -- 4 Hybrid Multirate PALS -- 4.1 Environment-Restricted Synchronous Ensembles -- 4.2 Realizable Transition Sequences -- 4.3 Hybrid Multirate PALS Distributed Models -- 4.4 Relating the Synchronous and Asynchronous Models -- 5 Verifying Invariants Using SMT Solving -- 5.1 Logical Representations -- 5.2 Local Clocks and SMT Solving -- 6 Concluding Remarks -- References -- Debits and Credits in Petri Nets and Linear Logic -- 1 Introduction -- 2 Intuitionistic Linear Logic with Mix -- 2.1 Simple Products and Multisets -- 2.2 Horn ILLmix Sequents -- 3 Debit Nets -- 4 Debit Nets as a Model of Horn ILLmix -- 4.1 Big-Step Semantics -- 4.2 Small-Step Semantics -- 4.3 Encoding Horn ILLmix into Debit Nets -- 5 Related Work and Conclusions -- A Proofs -- A.1 Proofs for Sect.4.1 -- A.2 Proofs for Sect.4.2 -- A.3 Proofs for Sect.4.3 -- References -- Alice and Bob Meet Equational Theories -- 1 Introduction -- 2 Alice&Bob Protocol Notation -- 2.1 Overview -- 2.2 Messages and Message Model -- 2.3 Alice&Bob in Detail -- 3 From Equations to Rewriting Rules -- 3.1 Role Scripts for Protocols -- 3.2 Deciding Executability -- 3.3 Checking Received Messages -- 3.4 Putting It All Together -- 4 Automated Translation to Tamarin -- 5 Related Work -- 6 Conclusions -- References -- On First-Order Model-Based Reasoning -- 1 Introduction -- 2 Model-Based Reasoning in First-Order Logic -- 2.1 Semantic Resolution -- 2.2 Hypertableaux -- 2.3 Model-Based Transformation of Clause Sets -- 2.4 The Model Evolution Calculus -- 2.5 SGGS: Semantically-Guided Goal-Sensitive Reasoning -- 3 Model-Based Reasoning in First-Order Theories -- 3.1 Building Theory Axioms into Resolution and Superposition. 3.2 Hierarchical Reasoning by Superposition -- 3.3 Hierarchical Reasoning in Local Theory Extensions -- 3.4 Beyond SMT: Satisfiability Modulo Assignment and MCsat -- 4 Discussion -- References -- A Normal Form for Stateful Connectors -- 1 Introduction -- 2 Petri Calculi -- 2.1 The P/T Petri Calculus -- 2.2 The C/E Petri Calculus -- 3 Nets with Boundaries -- 3.1 P/T Petri Nets with Boundaries -- 3.2 From P/T Nets with Boundaries to P/T Calculus and Back -- 3.3 C/E Nets with Boundaries -- 4 Normal Forms for Finite State P/T terms -- 4.1 Finite (State and Transition) Marking Graphs -- 4.2 Stateless, Infinitely Branching Marking Graphs -- 4.3 Finite State and Infinitely Branching Marking Graph -- 5 Normal Forms for the C/E Petri Calculus -- 6 Concluding Remarks -- References -- Enlightening Ph.D. Students with the Elegance of Logic -- Abstract -- 1 Preface -- 2 My Research Direction Before Knowing Jos00E9 -- 3 Jos00E9's Course on Formal Methods -- 4 Face-to-Face Discussions with Jos00E9 -- 5 Our Collaborations After My Graduation -- 6 Long-Term Influence -- Acknowledgement -- Two Decades of Maude -- 1 The Origins -- 2 The Language -- 2.1 Generalized Rewrite Theories in Maude -- 2.2 Reflection in Maude -- 2.3 Maude's Formal Tools -- 3 The Present: Unification and Narrowing -- 4 The Near Future: Rewriting Modulo SMT -- 4.1 Maude SMT -- 4.2 Symbolic Analysis of Distance-Bounding Protocols -- 5 Pathway Logic -- 5.1 About Pathway Logic -- 5.2 Maude's Role in Pathway Logic -- 6 Further Ahead -- References -- Formal Universes -- 1 Introduction -- 2 Universalism I : Paradise Lost? -- 3 Universalism II : Paradise Regained? -- 4 Reductionism -- 5 Criticism -- 6 Rejoinder -- References -- When Is a Formula a Loop Invariant? -- 1 Introduction -- 2 Examples -- 3 Preliminaries -- 4 Inductive Strengthening Procedure -- 5 Application to Specific Logical Theories. 5.1 Polynomial Equalities -- 5.2 Linear Arithmetic -- 6 k-Induction and Strengthening -- 6.1 Strategy Approximation (IV) Can Often Be Effective -- 7 Related Work -- 8 Conclusions -- References -- Generic Proof Scores for Generate & Check Method in CafeOBJ -- 1 Introduction -- 2 Preliminaries -- 2.1 Transition Systems -- 2.2 Verification of Invariant Properties -- 2.3 Verification of (p Leads-to q) Properties -- 2.4 Generate and Check for st St -- 2.5 Built-in Search Predicate -- 2.6 Generate & Check for tr Tr -- 2.7 Generate&Check for Verification of Invariant Properties -- 2.8 Generate&Check for Verification of (p Leads-to q) Properties -- 2.9 System and Property Specifications, and Proof Scores -- 3 Generic Proof Scores for Generate & Check Method -- 3.1 GENcases: Generating Patterns and Checking on Them -- 3.2 Three Parameterized Modules for Invariant Properties -- 3.3 Four Parameterized Modules for (p Leads-to q) Properties -- 4 QLOCK Specifications -- 4.1 QLOCK System SpecificationsThe specifications explained in this section are in the file qlock-sys.cafe on the web page. -- 4.2 QLOCK Property SpecificationsThe modules in this section is in the file qlock-prop.cafe unless otherwise stated. -- 4.3 Extended State (State % Aid) and Possible Inductive Invariants -- 5 QLOCK Proof Scores -- 5.1 Proof Scores for Invariant Properties -- 5.2 Proof Scores for (p Leads-to q) Property -- 6 Conclusion -- 6.1 Related Works -- 6.2 Some Features of Generic Proof Scores, Generate & Check Method, and CafeOBJ -- 6.3 Future Issues -- References -- Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting -- 1 Introduction -- 2 Preliminaries -- 3 Minimal Non--Terminating Terms at Frozen Positions -- 4 Modeling the Unhiding Process Using Rules -- 4.1 A New Notion of Minimal Non--terminating Term -- 5 From Minimal Terms to the CS-DP Framework. 5.1 Context-Sensitive Dependency Pair Framework -- 6 Usable Rules in the CS-DP Framework -- 6.1 Strongly Minimal Terms -- 6.2 Left-Linearity and -Conservativity -- 6.3 Extended Basic CS Usable Rules -- 7 Experimental Evaluation -- 8 Conclusions -- References -- Model-Checking HELENA Ensembles with Spin -- 1 Introduction -- 2 Foundations on LTLX Preservation -- 3 The Helena Approach -- 4 HelenaLight -- 4.1 Syntax of HelenaLight Ensemble Specifications -- 4.2 Semantics of HelenaLight Ensemble Specifications -- 4.3 LTL for HelenaLight -- 5 PromelaLight -- 5.1 Syntax of PromelaLight Specifications -- 5.2 Semantics of PromelaLight Specifications -- 5.3 LTL for PromelaLight -- 6 Translation of HelenaLight to PromelaLight -- 7 -Stutter Equivalence of the Translation -- 8 Model-Checking HelenaLight with Spin -- 9 Conclusion -- References -- Modularity of Ontologies in an Arbitrary Institution -- 1 Introduction -- 2 Institutions -- 3 Conservative Extensions and Inseparability -- 4 Module Notions -- 5 Conclusions -- References -- Rewriting Strategies and Strategic Rewrite Programs -- 1 Introduction -- 2 Historical Considerations -- 3 What are Strategic Rewriting and Strategic Programs? -- 3.1 Rewriting -- 3.2 Strategic Rewrite Programs -- 3.3 Abstract Reduction System -- 3.4 Strategic Rewriting -- 4 Strategy Description: Different Points of View -- 4.1 Rewriting Logic -- 4.2 Rewriting Calculus -- 4.3 Extensional Strategies -- 4.4 Intensional Strategies -- 4.5 Positional Strategies -- 5 Strategy Languages -- 6 Operational Semantics of Strategic Programs -- 7 Properties of Strategic Rewriting -- 8 Conclusion and Further Work -- References -- Network-on-Chip Firewall: Countering Defective and Malicious System-on-Chip Hardware -- 1 Introduction -- 2 Background -- 3 Threat Model -- 4 Core-Based Isolation -- 5 NoCF Interposer Design -- 6 Prototype Implementation. 7 Constraining a Malicious GPU. |
| Record Nr. | UNINA-9910484533103321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||