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.
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 : 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 : 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 | ||
| ||
Rewriting Logic and Its Applications [[electronic resource] ] : 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Paphos, Cyprus, March 20-21, 2010, Revised Selected Papers / / edited by Peter Csaba Ölveczky
| Rewriting Logic and Its Applications [[electronic resource] ] : 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Paphos, Cyprus, March 20-21, 2010, Revised Selected Papers / / edited by Peter Csaba Ölveczky |
| Edizione | [1st ed. 2010.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010 |
| Descrizione fisica | 1 online resource (X, 264 p. 44 illus.) |
| Disciplina | 005.11 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer programming
Software engineering Compilers (Computer programs) Computer science Machine theory Programming Techniques Software Engineering Compilers and Interpreters Computer Science Logic and Foundations of Programming Formal Languages and Automata Theory |
| ISBN |
1-280-38973-7
9786613567659 3-642-16310-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Rewriting, Inference, and Proof -- Twenty Years of Rewriting Logic -- Termination and Narrowing -- Proving Termination in the Context-Sensitive Dependency Pair Framework -- A Dependency Pair Framework for A???C-Termination -- Folding Variant Narrowing and Optimal Variant Termination -- Tools -- A Church-Rosser Checker Tool for Conditional Order-Sorted Equational Maude Specifications -- A Maude Coherence Checker Tool for Conditional Order-Sorted Rewrite Theories -- The K Framework -- K-Maude: A Rewriting Based Tool for Semantics of Programming Languages -- Collecting Semantics under Predicate Abstraction in the K Framework -- Applications and Semantics -- Concurrent Rewriting Semantics and Analysis of Asynchronous Digital Circuits -- A Formal Pattern Architecture for Safe Medical Systems -- On the Behavioral Semantics of Real-Time Domain Specific Visual Languages -- Multiset Rewriting: A Semantic Framework for Concurrency with Name Binding -- Maude Model Checking and Debugging -- The Linear Temporal Logic of Rewriting Maude Model Checker -- Enhancing the Debugging of Maude Specifications -- Rewrite Engines -- The Third Rewrite Engines Competition. |
| Record Nr. | UNISA-996465822903316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Software Engineering and Formal Methods [[electronic resource] ] : 17th International Conference, SEFM 2019, Oslo, Norway, September 18–20, 2019, Proceedings / / edited by Peter Csaba Ölveczky, Gwen Salaün
| Software Engineering and Formal Methods [[electronic resource] ] : 17th International Conference, SEFM 2019, Oslo, Norway, September 18–20, 2019, Proceedings / / edited by Peter Csaba Ölveczky, Gwen Salaün |
| Edizione | [1st ed. 2019.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
| Descrizione fisica | 1 online resource (XVIII, 550 p. 910 illus., 89 illus. in color.) |
| Disciplina | 005.1 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Compilers (Computer programs) Computer science Electronic digital computers—Evaluation Artificial intelligence Computer simulation Software Engineering Compilers and Interpreters Theory of Computation System Performance and Evaluation Artificial Intelligence Computer Modelling |
| ISBN | 3-030-30446-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISA-996466289003316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Software Engineering and Formal Methods : 17th International Conference, SEFM 2019, Oslo, Norway, September 18–20, 2019, Proceedings / / edited by Peter Csaba Ölveczky, Gwen Salaün
| Software Engineering and Formal Methods : 17th International Conference, SEFM 2019, Oslo, Norway, September 18–20, 2019, Proceedings / / edited by Peter Csaba Ölveczky, Gwen Salaün |
| Edizione | [1st ed. 2019.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
| Descrizione fisica | 1 online resource (XVIII, 550 p. 910 illus., 89 illus. in color.) |
| Disciplina | 005.1 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Compilers (Computer programs) Computer science Electronic digital computers—Evaluation Artificial intelligence Computer simulation Software Engineering Compilers and Interpreters Theory of Computation System Performance and Evaluation Artificial Intelligence Computer Modelling |
| ISBN | 3-030-30446-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910349282603321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
