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

• Pubblicazione: Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015
• Edizione: 1st ed. 2015.
• Descrizione fisica: 1 online resource (XI, 634 p. 103 illus.)
• Disciplina: 621.395
• 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
• Persona (resp. second.): Martí-OlietNarciso; ÖlveczkyPeter Csaba; TalcottCarolyn
• Note generali: Bibliographic Level Mode of Issuance: Monograph
• 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.
• Sommario/riassunto: This Festschrift volume contains 28 refereed papers including personal memories, essays, and regular research papers by close collaborators and friends of José Meseguer to honor him on the occasion of his 65th birthday. These papers were presented at a symposium at the University of Illinois at Urbana-Champaign on September 23-25, 2015. The symposium also featured invited talks by Claude and Hélène Kirchner and by Patrick Lincoln. The foreword of this volume adds a brief overview of some of José's many scientific achievements followed by a bibliography of papers written by José.
• Titolo autorizzato: Logic, Rewriting, and Concurrency
• ISBN: 3-319-23165-0
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Lingua di pubblicazione: Inglese
• Record Nr.: 9910484533103321
• Lo trovi qui: Univ. Federico II
• Serie: Theoretical Computer Science and General Issues, . 2512-2029 ; ; 9200