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 | ||
| ||
Formal Methods: Foundations and Applications [[electronic resource] ] : 17th Brazilian Symposium, SBMF 2014, Maceió, AL, Brazil, September 29--October 1, 2014. Proceedings / / edited by Christiano Braga, Narciso Martí-Oliet
| Formal Methods: Foundations and Applications [[electronic resource] ] : 17th Brazilian Symposium, SBMF 2014, Maceió, AL, Brazil, September 29--October 1, 2014. Proceedings / / edited by Christiano Braga, Narciso Martí-Oliet |
| Edizione | [1st ed. 2015.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 |
| Descrizione fisica | 1 online resource (IX, 179 p. 39 illus.) : online resource |
| Disciplina | 004.0151 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Computer logic Mathematical logic Programming languages (Electronic computers) Management information systems Computer science Software Engineering Logics and Meanings of Programs Mathematical Logic and Formal Languages Programming Languages, Compilers, Interpreters Management of Computing and Information Systems |
| ISBN | 3-319-15075-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | LLVM-based code generation for B -- Equational abstractions in rewriting logic and Maude -- Formalization of ZSyntax to reason about Molecular Pathways in HOL4 -- Test Case Selection Criteria for Symbolic Models of Real-Time Systems -- Model-Driven Engineering in the Heterogeneous Tool Set -- A coinductive animation of Turing Machines -- Towards completeness in Bounded Model Checking through Automatic Recursion Depth Detection -- A Probabilistic Model Checking Analysis of a Realistic Vehicular Networks Mobility Model -- Dynamic logics for every season -- Completeness and decidability results for hybrid(ised) logics -- Parameterisation of Three-Valued Abstractions. |
| Record Nr. | UNINA-9910484674203321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Formal Methods: Foundations and Applications [[electronic resource] ] : 17th Brazilian Symposium, SBMF 2014, Maceió, AL, Brazil, September 29--October 1, 2014. Proceedings / / edited by Christiano Braga, Narciso Martí-Oliet
| Formal Methods: Foundations and Applications [[electronic resource] ] : 17th Brazilian Symposium, SBMF 2014, Maceió, AL, Brazil, September 29--October 1, 2014. Proceedings / / edited by Christiano Braga, Narciso Martí-Oliet |
| Edizione | [1st ed. 2015.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 |
| Descrizione fisica | 1 online resource (IX, 179 p. 39 illus.) : online resource |
| Disciplina | 004.0151 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Computer logic Mathematical logic Programming languages (Electronic computers) Management information systems Computer science Software Engineering Logics and Meanings of Programs Mathematical Logic and Formal Languages Programming Languages, Compilers, Interpreters Management of Computing and Information Systems |
| ISBN | 3-319-15075-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | LLVM-based code generation for B -- Equational abstractions in rewriting logic and Maude -- Formalization of ZSyntax to reason about Molecular Pathways in HOL4 -- Test Case Selection Criteria for Symbolic Models of Real-Time Systems -- Model-Driven Engineering in the Heterogeneous Tool Set -- A coinductive animation of Turing Machines -- Towards completeness in Bounded Model Checking through Automatic Recursion Depth Detection -- A Probabilistic Model Checking Analysis of a Realistic Vehicular Networks Mobility Model -- Dynamic logics for every season -- Completeness and decidability results for hybrid(ised) logics -- Parameterisation of Three-Valued Abstractions. |
| Record Nr. | UNISA-996198832403316 |
| 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. | 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 | ||
| ||
Recent Trends in Algebraic Development Techniques [[electronic resource] ] : 21st International Workshop, WADT 2012, Salamanca, Spain, June 7-10, 2012, Revised Selected Papers / / edited by Narciso Martí-Oliet, Miguel Palomino
| Recent Trends in Algebraic Development Techniques [[electronic resource] ] : 21st International Workshop, WADT 2012, Salamanca, Spain, June 7-10, 2012, Revised Selected Papers / / edited by Narciso Martí-Oliet, Miguel Palomino |
| Edizione | [1st ed. 2013.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 |
| Descrizione fisica | 1 online resource (X, 283 p. 71 illus.) |
| Disciplina | 005.1015113 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Machine theory Computer science—Mathematics Mathematical logic Computer Science Logic and Foundations of Programming Formal Languages and Automata Theory Mathematics of Computing Theory of Computation Mathematical Logic and Foundations |
| ISBN | 3-642-37635-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Open Multiparty Interaction.- Behaviour Protection in Modular Rule-Based System Specifications.- Quantitative Modal Transition Systems.- Bounded Model Checking of Recursive Programs with Pointers in K.- A Probabilistic Strategy Language for Probabilistic Rewrite Theories and Its Application to Cloud Computing.- Adaptable Transition Systems.- Compiling Logics.- Transformation Systems with Incremental Negative Application Conditions.- Statistical Model Checking for Composite Actor Systems.- Barbed Semantics for Open Reactive Systems.- Designing Domain Specific Languages – A Craftsman’s Approach for the Railway Domain Using Casl.- Satisfiability Calculus: The Semantic Counterpart of a Proof Calculus in General Logics.- Semantics of the Distributed Ontology Language: Institutes and Institutions.- Formal Specification of the Kademlia and the Kad Routing Tables in Maude -- A Generic Program Slicing Technique Based on Language Definitions -- Distances between Processes: A Pure Algebraic Approach. |
| Record Nr. | UNISA-996466187903316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Recent Trends in Algebraic Development Techniques [[electronic resource] ] : 21st International Workshop, WADT 2012, Salamanca, Spain, June 7-10, 2012, Revised Selected Papers / / edited by Narciso Martí-Oliet, Miguel Palomino
| Recent Trends in Algebraic Development Techniques [[electronic resource] ] : 21st International Workshop, WADT 2012, Salamanca, Spain, June 7-10, 2012, Revised Selected Papers / / edited by Narciso Martí-Oliet, Miguel Palomino |
| Edizione | [1st ed. 2013.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 |
| Descrizione fisica | 1 online resource (X, 283 p. 71 illus.) |
| Disciplina | 005.1015113 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Machine theory Computer science—Mathematics Mathematical logic Computer Science Logic and Foundations of Programming Formal Languages and Automata Theory Mathematics of Computing Theory of Computation Mathematical Logic and Foundations |
| ISBN | 3-642-37635-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Open Multiparty Interaction.- Behaviour Protection in Modular Rule-Based System Specifications.- Quantitative Modal Transition Systems.- Bounded Model Checking of Recursive Programs with Pointers in K.- A Probabilistic Strategy Language for Probabilistic Rewrite Theories and Its Application to Cloud Computing.- Adaptable Transition Systems.- Compiling Logics.- Transformation Systems with Incremental Negative Application Conditions.- Statistical Model Checking for Composite Actor Systems.- Barbed Semantics for Open Reactive Systems.- Designing Domain Specific Languages – A Craftsman’s Approach for the Railway Domain Using Casl.- Satisfiability Calculus: The Semantic Counterpart of a Proof Calculus in General Logics.- Semantics of the Distributed Ontology Language: Institutes and Institutions.- Formal Specification of the Kademlia and the Kad Routing Tables in Maude -- A Generic Program Slicing Technique Based on Language Definitions -- Distances between Processes: A Pure Algebraic Approach. |
| Record Nr. | UNINA-9910484324803321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||