Kooperativer Bibliotheksverbund

UID:

Umfang: IX, 442 p. , online resource.

ISBN: 9783540477952

Serie: Lecture Notes in Computer Science, 270

Inhalt: This volume contains 37 invited research papers collected in memory of Dieter Rödding, who is known for his work on the classification of recursive functions, on reduction classes, on the spectrum problem and on the complexity of cardinality quantifiers in predicate logic and in arithmetical hierarchy. He was one of the first to pursue the interaction of logic and computer science. The volume reflects the wide spectrum of Dieter Rödding's scientific interests.

Anmerkung: Minimal pairs for polynomial time reducibilities -- Primitive recursive word-functions of one variable -- Existential fixed-point logic -- Unsolvable decision problems for PROLOG programs -- You have not understood a sentence, unless you can prove it -- On the minimality of K, F, and D or: Why löten is non-trivial -- A 5-color-extension-theorem -- Closure relations, Buchberger's algorithm, and polynomials in infinitely many variables -- The benefit of microworlds in learning computer programming -- Skolem normal forms concerning the least fixpoint -- Spectral representation of recursively enumerable and coenumerable predicates -- Aggregating inductive expertise on partial recursive functions -- Domino threads and complexity -- Modelling of cooperative processes -- A setting for generalized computability -- First-order spectra with one variable -- On the early history of register machines -- Randomness, provability, and the separation of Monte Carlo Time and space -- Representation independent query and update operations on propositional definite Horn formulas -- Direct construction of mutually orthogonal latin squares -- Negative results about the length problem -- Some results on the complexity of powers -- The Turing complexity of AF C*-algebras with lattice-ordered KO -- Remarks on SASL and the verification of functional programming languages -- Numerical stability of simple geometric algorithms in the plane -- Communication with concurrent systems via I/0-procedures -- A class of exp-time machines which can be simulated by polytape machines -- ???-Automata realizing preferences -- Ein einfaches Verfahren zur Normalisierung unendlicher Herleitungen -- Grammars for terms and automata -- Relative konsistenz -- Segment translation systems -- First steps towards a theory of complexity over more general data structures -- On the power of single-valued nondeterministic polynomial time computations -- A concatenation game and the dot-depth hierarchy -- Do there exist languages with an arbitrarily small amount of context-sensitivity? -- The complexity of symmetric boolean functions.

In: Springer eBooks

Weitere Ausg.: Printed edition: ISBN 9783540181705

Sprache: Englisch

Fachgebiete: Informatik

Schlagwort(e): Aufsatzsammlung ; Festschrift

DOI: 10.1007/3-540-18170-9

URL: http://dx.doi.org/10.1007/3-540-18170-9

URL: Volltext

UID:

Umfang: VIII, 463 S. : , graph. Darst.

Sprache: Englisch

Fachgebiete: Informatik , Wirtschaftswissenschaften , Komparatistik. Außereuropäische Sprachen/Literaturen , Mathematik

Schlagwort(e): Programmierung ; Simulationssprache ; Simulationssprache ; Konferenzschrift ; Konferenzschrift ; Konferenzschrift

UID:

Umfang: XVII, 249 p. 11 illus. , online resource.

Ausgabe: 1st ed. 2024.

ISBN: 9783662683132

Inhalt: In recent years, computer science in sport has grown extremely, mainly because more and more new data has become available. Computer science tools in sports, whether used for opponent preparation, competition, or scientific analysis, have become indispensable across various levels of expertise nowadays. A completely new market has emerged through the utilization of these tools in the four major fields of application: clubs and associations, business, science, and the media. This market is progressively gaining importance within university research and educational activities. This textbook aims to live up to the now broad diversity of computer science in sport by having more than 30 authors report from their special field and concisely summarise the latest findings. The book is divided into four main sections: data sets, modelling, simulation and data analysis. In addition to background information on programming languages and visualisation, the textbook is framed by history and an outlook. Students with a connection to sports science are given a comprehensive insight into computer science in sport, supported by a didactically sophisticated concept that makes it easy to convey the learning content. Numerous questions for self-testing underpin the learning effect and ensure optimal exam preparation. For advanced students, the in-depth discussion of time series data mining, artificial neural networks, convolution kernels, transfer learning and random forests offers additional value. The Editor Prof. Dr Daniel Memmert is the executive director and professor at the Institute of Exercise Training and Sport Informatics at the German Sport University Cologne. He is the editor and author of numerous textbooks with a focus on exercise science, sports psychology and informatics. His institute organises two certificate programmes (Game Analysis Team Cologne / Sports Director in Youth and Amateur Soccer) as well as the first international Master's degree programme "Match Analysis".

Anmerkung: I HISTORY -- History -- II DATA -- Artificial data -- Text data -- Video data -- Event data -- Position data -- Online data -- III MODELING -- Modeling -- Predictive models -- Physiological modeling -- IV SIMULATION -- Simulation -- Metabolic simulation -- Simulation of physiological adaptation processes -- V PROGRAMMING LANGUAGES -- An introduction to the programming language R for beginners -- Phyton -- VI DATA ANALYSIS -- Logistic Regression -- Time Series Data Mining -- Process Mining -- Networks Centrality -- Artificial Neural Networks -- Deep Neural Networks -- Convolutional Neural Networks -- Transfer Learning -- Random Forest -- Statistical learning for the modeling of soccer matches -- Open-Set Recognition -- VII VISUALIZATION -- Visualization - Basics and Concepts -- VIII OUTLOOK -- Outlook. .

In: Springer Nature eBook

Weitere Ausg.: Printed edition: ISBN 9783662683125

Weitere Ausg.: Printed edition: ISBN 9783662683149

Sprache: Englisch

Fachgebiete: Sport

Schlagwort(e): Aufsatzsammlung

DOI: 10.1007/978-3-662-68313-2

URL: https://doi.org/10.1007/978-3-662-68313-2

URL: lizenzpflichtig

URL: Volltext  (URL des Erstveröffentlichers)

UID:

Umfang: 1 online resource (375 pages)

Ausgabe: 1st ed.

ISBN: 9783839472422

Serie: Digitale Gesellschaft Series

Anmerkung: Cover -- Contents -- Acknowledgements -- Introduction -- The Three Central Hypotheses -- The Logical Progression of the Three Concepts or Hypotheses -- Part One - Hyper‐Modernism: Digital Media Technologies and Science Fiction -- Part One to Part Two: From Hyper‐Modernism to Hyperreality -- Part Two - Hyperreality: Reevaluation of Jean Baudrillard's Media Theory and the Simulacrum -- Part Two to Part Three: From Hyperreality to Post‐Humanism and Creative Coding -- Part Three - Posthumanism: N. Katherine Hayles' History of Cybernetics, Creative Coding, and the Future of Informatics -- Originally Published Versions -- Methodology -- Thirty Minute Statement at my Ph.D. Oral Defense Alan N. Shapiro, April 12, 2024 -- Part One - Hyper‐Modernism: Digital Media Technologies and Science Fiction -- Overview of Part One -- Short Definitions of Modernity, Postmodernism, and Hyper‐Modernism -- The Three Essays of Part One -- Mobility and Science Fiction -- Introduction -- We Do Not Live in a Society Where Mobility is Encouraged -- The Dream of the Tomorrow‐Car -- Henri Matisse Paints "the Vision Machine" -- The New Vision Machine -- Close Encounters of the Third Kind: The Menace of Verticality -- The "Spinner" Flying Cars of Blade Runner: Simulation and Surveillance -- Blade Runner: We Are All Replicants -- Blade Runner 2049: Android Liberation Between Old and New Informatic Power -- Minority Report: The Utopia/Dystopia of Surveillance Technologies -- The Fifth Element: When Manhattan has no More Ways to Expand -- Back to the Future: A Speed So Fast that the Laws of Spacetime Get Shattered -- Total Recall: You're in a Johnny Cab -- Robots Versus Androids -- Self‐Owning Cars -- Enhance the Physical World -- The Simulacra, Do Androids Dream of Electric Sheep?, and Dr. Bloodmoney -- The "Science Fiction World" of Philip K. Dick's Ubik. , Who Is Jory Miller and What is Ubik? -- Fredric Jameson on Postmodernism -- Sonja Yeh on the Postmodern Media Theorists -- Donna J. Haraway's "A Manifesto for Cyborgs" -- Science Fiction Heterotopia: The Economy of the Future -- Introduction: Foucault's Heterotopia -- The Technologizing of Memory -- Black Mirror: "The Entire History of You" - Scenes from a Marriage -- Similar Technologies in the Real World Today -- Brain‐Computer Interface -- Designing the Brain‐Computer Interface -- Hyper‐Modernist Literature -- The Economy of the Future -- Post‐Capitalism and Technological Anarchism -- Star Trek Replicators and Star Trek Economics -- Ecologically Aware or Sustainable 3D Printers -- Additive Manufacturing and Living Organisms -- Andre Gorz: Human Liberation Beyond Work -- Murray Bookchin, Post‐Scarcity Anarchism -- Yanis Varoufakis' Vision of Post‐Capitalism -- Conclusion -- Geert Lovink on Post‐Capitalism -- Blockchain Decentralized Idealism -- Smart Contracts -- Between Law and Code -- Decentralized Autonomous Organization -- Between Corporate Intellectual Property Rights and the Rights of Users -- Fiction and Power in Postmodernism -- Cornelius Castoriadis, The Imaginary Institution of Society -- Donna J. Haraway on the Informatics of Domination -- Michel Foucault's Analytics of Power -- Jean Baudrillard, Forget Foucault -- Gilles Deleuze, "Postscript on the Societies of Control" -- Fiction, Power, and Codes in Hyper‐Modernism -- John Armitage on Hyper‐Modernism -- Albert Borgmann on Hyper‐Modernism -- Gilles Lipovetsky on Hyper‐Modernism -- What is Hyper‐Modernism? -- Introduction -- Access to History -- The Carnivalesque -- Modernity, Postmodernism, Hyper‐Modernism -- Gustave Flaubert: To Write a Novel About Nothing -- Hyper‐Modernist Creativity -- Body, Self, and Code in Hyper‐Modernism -- Sincerity and Authenticity. , Darko Suvin on Science Fiction Studies -- Carl Freedman on Science Fiction Studies -- Istvan Ciscsery‐Ronay, Jr. on Science Fiction Studies -- Part Two - Hyperreality: Reevaluation of Jean Baudrillard's Media Theory and the Simulacrum -- Overview of Part Two -- Defining the Simulacrum and Hyperreality -- Thinking Hyperreality: From Rhetoric to Code -- Baudrillard's Importance for the Future -- Baudrillard and the Situationists -- Baudrillard and Trump -- Baudrillard's Importance for the Future -- The Controversy Around Baudrillard -- Yes - Everything is Simulation! -- Early Baudrillard: The Consumer Society and For a Critique of the Political Economy of the Sign -- Symbolic Exchange and the Gift Economy -- The First Order of Simulacra: The Student of Prague -- The Second Order of Simulacra: The First Industrial Revolution -- The Third Order of Simulacra: Simulation and Hyperreality -- First‐Wave Digitalization as Interactive Performance -- The Fourth Order of Simulacra: Value Radiates in All Directions -- From Descartes to Baudrillard: The "Evil Demon" of Images -- Arthur C. Clarke, "The Nine Billion Names of God" -- The Trapdoor Escape Hatch Way Out of Hyperreality -- High Life: The Black Hole of Humanity's Extinction and New Hope -- Poetic Resolution in Baudrillard's Thought -- Daniel Boorstin, The Image: Hyperreality Overtakes America -- Umberto Eco, Travels in Hyperreality -- Roland Barthes, Mythologies -- Taking the Side of Objects -- Plato and the Simulacrum -- Plato as Software Designer -- Brian Gogan on Plato, Baudrillard, and Rhetoric -- Deleuze on "Plato and the Simulacrum" -- Upgrading Hyperreality and the Simulacrum for Digitalization -- Personalized Advertising -- Transdisciplinarity is Good for (Post‑)Humanity -- Virtual Reality, Augmented Reality, and the Metaverse -- Baudrillard and the Situationists -- Introduction. , "Taking the Side of Objects" and the Situationists -- Baudrillard's Paradigm Shift -- Is Baudrillard Fair to the Situationists? -- "Baudrillard and the Situationists" Commentators Douglas Kellner and Sadie Plant, and the Tension between Critical Theory and Fatal Theory -- Exhibit A (Baudrillard self‐simplifies): -- Exhibit B (Baudrillard's critique of the Situationists is reductionist): -- Exhibit C (Sadie Plant's critique of Baudrillard is reductionist): -- Situationist Practices -- Wandering or the Drift - Le Dérive -- Psycho‐Geography -- The Diverting of Technologies - Le détournement -- The Making or Creating or Construction of Situations -- The Radical Illusion Beyond Art -- Neo‐Situationism in the Field of Advanced Digital Technologies -- Urban and Street Art Activism -- Augmented Reality versus Wall Street -- Conclusion -- McKenzie Wark on the Situationists -- Play Don't Work -- Existential Encounter with the Object -- From the Subject to the Object in Jean‐Paul Sartre's Nausea -- The Myth of Sisyphus: Albert Camus on the Side of Objects -- Simone de Beauvoir, The Ethics of Ambiguity -- Jean Baudrillard and the Donald: Is Trump a Fascist or is He the Parody of Fascism? -- Epistemology of True and False -- Society of the Spectacle and Hyperreality -- Donald Trump the Empty Signifier -- From Simulation to the Grotesque and the Self‐Parody -- Springtime for Hitler -- Serge Latouche Remembers Baudrillard -- Biosphere 2: The Artificial Paradise of Nature -- Reality TV and Baudrillard's Telemorphosis -- The Truman Show: "The Last Thing That I Would Ever Do is Lie to You" -- My Two Key Differences from Baudrillard -- Part Three - Posthumanism: N. Katherine Hayles' History of Cybernetics, Creative Coding, and the Future of Informatics -- Overview of Part Three -- The Science Fiction of Star Trek. , Star Trek's Spock, Data, and Seven of Nine and the Three Orders of Cybernetics -- What is Posthumanism? -- The Concept of Nature in Whitehead and Merleau‐Ponty -- Rosi Braidotti's Celebratory Posthuman Philosophy -- A Fully Posthuman Situation -- Wendy Chun on Software Code -- Software Code as Expanded Narration -- The Software of the Future -- Star Trek: Technologies of Disappearance -- Technoscience and Storytelling -- From Liberal Humanism to Posthumanism -- Cyborg Spock and NASA's Cyborg -- First Order Cybernetics -- How Information Lost Its Body -- Claus Pias on First‐Order Cybernetics -- Gene Roddenberry Designs His First Alien -- "The Devil in the Dark": Empathy for Radical Otherness -- Second Order Cybernetics -- Bernhard Dotzler on Second‐Order Cybernetics -- The Android Data of Star Trek: The Next Generation -- "The Offspring": Data's Daughter Lal -- Third Order Cybernetics -- "Becoming‐Borg" Seven of Nine -- Star Trek: Picard, "Remembrance" -- "Embodied Informatics" is a Science Fiction Idea -- Hayles on Writing and Software Code -- Hyper‐Modernist Science -- I, Robot and the Moral Dilemmas of the Three Laws of Robotics -- The Zeroth Law of Robotics and the Robot Unconscious -- Hayles on the Cognitive Nonconscious -- Marie‐Luise Angerer Critiques Hayles -- Judith Butler and Gender Theory -- Ex Machina and the Turing Test -- Ex Machina: The Performance of Female and Human -- Monique Wittig, The Straight Mind -- Software Code as Expanded Narration -- Software Code as Expressive Media -- Friedrich Kittler: The Numeric Kernel is Decisive -- Kittler's Media Archaeology -- Wolfgang Hagen on Programming Languages -- Ten Paradigms of Informatics and Programming -- The First Hyper‐Modern Computers -- Enter Software Studies -- Enter Creative Coding -- Alan Turing: The Imitation Game and Befriending the Evil Demon. , Alan Turing: The Scientific and Cultural Levels of Computing.

Weitere Ausg.: Print version: Shapiro, Alan N. Decoding Digital Culture with Science Fiction Bielefeld : transcript Verlag,c2024 ISBN 9783837672428

Sprache: Englisch

Fachgebiete: Allgemeines

Schlagwort(e): Electronic books.

URL: Click to View

URL: lizenzpflichtig

UID:

Umfang: 1 online resource (XV, 772 p. 1 illus.)

Ausgabe: 1st ed. 2020.

ISBN: 3-030-44914-9

Serie: Theoretical Computer Science and General Issues, 12075

Inhalt: This open access book constitutes the proceedings of the 29th European Symposium on Programming, ESOP 2020, which took place in Dublin, Ireland, in April 2020, and was held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020. The papers deal with fundamental issues in the specification, design, analysis, and implementation of programming languages and systems. .

Anmerkung: Intro -- ETAPS Foreword -- Preface -- Organization -- Formal Methods for Evolving Database Applications (Abstract of Keynote Talk) -- Contents -- Trace-Relating Compiler Correctness and Secure Compilation -- Introduction -- Trace-Relating Compiler Correctness -- Property Mappings -- Trace Relations and Property Mappings -- Preservation of Subset-Closed Hyperproperties -- Instances of Trace-Relating Compiler Correctness -- Undefined Behavior -- Resource Exhaustion -- Different Source and Target Values -- Abstraction Mismatches -- Trace-Relating Compilation and Noninterference Preservation -- Trace-Relating Secure Compilation -- Trace-Relating Secure Compilation: A Spectrum of Trinities -- Instance of Trace-Relating Robust Preservation of Trace Properties -- Instances of Trace-Relating Robust Preservation of Safety and Hypersafety -- Related Work -- Conclusion and Future Work -- Acknowledgements -- Bibliography -- Runners in action -- 1 Introduction -- 2 Algebraic effects, handlers, and runners -- 2.1 Algebraic effects and handlers -- 2.2 Runners -- 3 Programming with runners -- 3.1 The user and kernel monads -- 3.2 Runners as a programming construct -- 4 A calculus for programming with runners -- 4.1 Types -- 4.2 Values and computations -- 4.3 Type system -- 4.4 Equational theory -- 5 Denotational semantics -- 5.1 Semantics of types -- 5.2 Semantics of values and computations -- 5.3 Coherence, soundness, and finalisation theorems -- 6 Runners in action -- 7 Implementation -- 8 Related work -- 9 Conclusion and future work -- References -- On the Versatility of Open Logical Relations -- 1 Introduction -- 2 The Playground -- 3 A Fundamental Gap -- 4 Warming Up: A Containment Theorem -- 5 Automatic Differentiation -- 6 On Refinement Types and Local Continuity -- 6.1 A Refinement Type System Ensuring Local Continuity -- 6.2 Basic Typing Rules. , 6.3 Typing Conditionals -- 6.4 Open-logical Predicates for Refinement Types -- 7 Related Work -- 8 Conclusion and Future Work -- References -- Constructive Game Logic -- 1 Introduction -- 2 Related Work -- 3 Syntax -- 3.1 Example Games -- 4 Semantics -- 4.1 Realizers -- 4.2 Formula and Game Semantics -- 4.3 Demonic Semantics -- 5 Proof Calculus -- 6 Theory: Soundness -- 7 Operational Semantics -- 8 Theory: Constructivity -- 9 Conclusion and Future Work -- References -- Optimal and Perfectly Parallel Algorithms for On-demand Data-flow Analysis -- 1 Introduction -- 2 Preliminaries -- 2.1 The IFDS Framework -- 2.2 Trees and Tree Decompositions -- 3 Problem definition -- 4 Treewidth-based Data-ow Analysis -- 4.1 Preprocessing -- 4.2 Word Tricks -- 4.3 Answering Queries -- 4.4 Parallelizability and Optimality -- 5 Experimental Results -- 6 Conclusion -- References -- Concise Read-Only Specifications for Better Synthesis of Programs with Pointers -- 1 Introduction -- 1.1 Correct Programs that Do Strange Things -- 1.2 Towards Simple Read-Only Specifications for Synthesis -- 1.3 Our Contributions -- 2 Program Synthesis with Read-Only Borrows -- 2.1 Basics of SSL-based Deductive Program Synthesis -- 2.2 Reducing Non-Determinism with Read-Only Annotations -- 2.3 Composing Read-Only Borrows -- 2.4 Borrow-Polymorphic Inductive Predicates -- 3 BoSSL: Borrowing Synthetic Separation Logic -- 3.1 BoSSL rules -- 3.2 Memory Model -- 3.3 Soundness -- 4 Implementation and Evaluation -- 4.1 Experimental Setup -- 4.2 Performance and Quality of the Borrowing-Aware Synthesis -- 4.3 Stronger Correctness Guarantees -- 4.4 Robustness under Synthesis Perturbations -- 5 Limitations and Discussion -- 6 Related Work -- 7 Conclusion -- References -- Soundness conditions for big-step semantics -- 1 Introduction -- 2 A meta-theory for big-step semantics -- 3 Extended semantics. , 3.1 Traces -- 3.2 Wrong -- 4 Expressing and proving soundness -- 4.1 Expressing soundness -- 4.2 Conditions ensuring soundness-must -- 4.3 Conditions ensuring soundness-may -- 5 Examples -- 5.1 Simply-typed -calculus with recursive types -- 5.2 MiniFJ& -- -λ -- 5.3 Intersection and union types -- 5.4 MiniFJ& -- O -- 6 The partial evaluation construction -- 7 Related work -- 8 Conclusion and future work -- Acknowledgments -- References -- Liberate Abstract Garbage Collection from the Stack by Decomposing the Heap -- 1 Introduction -- 1.1 Examples -- 1.2 Generalizing the Approach -- 2 A-Normal Form λ- Calculus -- 3 Background -- 3.1 Semantic Domains -- 3.2 Concrete Semantics -- 3.3 Abstracting Abstract Machines with Garbage Collection -- 3.4 Stack-Precise CFA with Garbage Collection -- 3.5 The k-CFA Context Abstraction -- 4 From Threaded to Compositional Stores -- 4.1 Threaded-Store Semantics -- 4.2 Threaded-Store Semantics with Effect Log -- 4.3 Compositional-Store Semantics -- 4.4 Compositional-Store Semantics with Garbage Collection -- 5 Abstract Compositional-Store Semantics with Garbage Collection -- 6 Discussion -- 6.1 The Effects of Treating the Store Compositionally -- 6.2 The Effect of Treating the Time Compositionally -- 7 Related Work -- 8 Conclusion and Future Work -- References -- SMT-Friendly Formalization of the Solidity Memory Model -- 1 Introduction -- 2 Background -- 2.1 Ethereum -- 2.2 Solidity -- 2.3 SMT-Based Programs -- 3 Formalization -- 3.1 Types -- 3.2 Local Storage Pointers -- 3.3 Contracts, State Variables, Functions -- 3.4 Statements -- 3.5 Assignments -- 3.6 Expressions -- 4 Evaluation -- 5 Related Work -- 6 Conclusion -- References -- Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types -- 1 Introduction -- 2 Overview of our Approach -- 3 An MPST Theory with +, ∃, and ll. , 3.1 Types as Process Algebraic Terms -- 3.2 Global Types and Local Types -- 3.3 End-Point Projection: from Global Types to Local Types -- 3.4 Weak Bisimilarity of Global Types, Local Types, and Groups -- 3.5 Well-formedness of Global Types -- 3.6 Correctness of Projection under Well-Formedness -- 3.7 Decidability of Checking Well-Formedness -- 3.8 Discussion of Challenges -- 4 Practical Experience with the Theory -- 4.1 Implementation -- 4.2 Evaluation of the Approach -- 5 Related Work -- 6 Conclusion -- References -- Verifying Visibility-Based Weak Consistency -- 1 Introduction -- 2 Weak Consistency -- 2.1 Weak-Visibility Specifications -- 2.2 Consistency against Weak-Visibility Specifications -- 3 Establishing Consistency with Forward Simulation -- 3.1 Reducing Consistency to Safety Verification -- 3.2 Verifying Implementations -- 4 Proof Methodology -- 5 Implementation and Evaluation -- 6 Related Work -- 7 Conclusion and Future Work -- A Appendix: Proofs to Theorems and Lemmas -- References -- Local Reasoning for Global Graph Properties -- 1 Introduction -- 2 The Foundational Flow Framework -- 2.1 Preliminaries and Notation -- 2.2 Flows -- 2.3 Flow Graph Composition and Abstraction -- 3 Proof Technique -- 3.1 Encoding Flow-based Proofs in SL -- 3.2 Proof of the PIP -- 4 Advanced Flow Reasoning and the Harris List -- 4.1 The Harris List Algorithm -- 4.2 Product Flows for Reasoning about Overlays -- 4.3 Contextual Extensions and the Replacement Theorem -- 4.4 Existence and Uniqueness of Flows -- 4.5 Proof of the Harris List -- 5 Related Work -- 6 Conclusions and Future Work -- References -- Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems -- 1 Introduction -- 2 The Core Concepts of Aneris -- 2.1 Local and Thread-Local Reasoning -- 2.2 Node-Local Reasoning -- 2.3 Example: An Addition Service -- 2.4 Example: A Lock Server. , 3 AnerisLang -- 4 The Aneris Logic -- 4.1 The Program Logic -- 4.2 Adequacy for Aneris -- 5 Case Study 1: A Load Balancer -- 6 Case Study 2: Two-Phase Commit -- 6.1 A Replicated Log -- 7 Related Work -- 8 Conclusion -- Acknowledgments -- Bibliography -- Continualization of Probabilistic Programs With Correction -- 1 Introduction -- 2 Example -- 2.1 Continualization -- 2.2 Parameter Synthesis -- 2.3 Improving Inference -- 3 Syntax and Semantics of Programs -- 3.1 Source Language Syntax -- 3.2 Semantics -- 4 Continualizing Probabilistic Programs -- 4.1 Overview of the Algorithm -- 4.2 Distribution and Expression Transformations -- 4.3 Inuence Analysis and Control-Flow Correction of Predicates -- 4.4 Bringing it all together: Full Program Transformations -- 5 Synthesis of Continuity Correction Parameters -- 5.1 Optimization Framework -- 5.2 Optimization Algorithm -- 6 Methodology -- 6.1 Benchmarks -- 6.2 Experimental Setup -- 7 Evaluation -- 7.1 RQ1: Benefits of Continualization -- 7.2 RQ2: Impact of Smoothing Factors -- 7.3 RQ3: Extending Results to Other Systems -- 8 Related Work -- 9 Conclusion -- References -- Semantic Foundations for Deterministic Dataflow and Stream Processing -- 1 Introduction -- 2 Monoids as Types for Streams -- 3 Stream Transductions -- 4 Model of Computation -- 5 Combinators for Deterministic Dataow -- 6 Algebraic Reasoning for Optimizing Transformations -- 7 Related Work -- 8 Conclusion -- References -- Connecting Higher-Order Separation Logic to a First-Order Outside World -- 1 Introduction -- 2 Background: Ghost State in Separation Logic -- 2.1 Ghost Algebras -- 3 External State as Ghost State -- 4 Verifying C Programs with I/O in VST -- 5 Soundness of External-State Reasoning -- 6 Connecting VST to CertiKOS -- 6.1 CertiKOS Specifications -- 6.2 Relating OS and User State -- 6.3 Soundness of VST + CertiKOS. , 7 From syscall-level to hardware-level interactions. , English

Weitere Ausg.: ISBN 3-030-44913-0

Sprache: Englisch

Fachgebiete: Informatik

Schlagwort(e): Konferenzschrift

DOI: 10.1007/978-3-030-44914-8

URL: kostenfrei

UID:

Umfang: XXVI, 488 p. 129 illus. , online resource.

ISBN: 9783319780542

Serie: Lecture Notes in Computer Science, 10778

Inhalt: The two-volume set LNCS 10777 and 10778 constitutes revised selected papers from the 12th International Conference on Parallel Processing and Applied Mathematics, PPAM 2017, held in Lublin, Poland, in September 2017. The 49 regular papers presented in the proceedings were selected from 98 submissions. For the workshops and special sessions, that were held as integral parts of the PPAM 2017 conference, a total of 51 papers was accepted from 75 submissions. The papers were organized in topical sections named as follows: Part I: numerical algorithms and parallel scientific computing; particle methods in simulations; task-based paradigm of parallel computing; GPU computing; parallel non-numerical algorithms; performance evaluation of parallel algorithms and applications; environments and frameworks for parallel/distributed/cloud computing; applications of parallel computing; soft computing with applications; and special session on parallel matrix factorizations. Part II: workshop on models, algorithms and methodologies for hybrid parallelism in new HPC systems; workshop power and energy aspects of computations (PEAC 2017); workshop on scheduling for parallel computing (SPC 2017); workshop on language-based parallel programming models (WLPP 2017); workshop on PGAS programming; minisymposium on HPC applications in physical sciences; minisymposium on high performance computing interval methods; workshop on complex collective systems.

Anmerkung: Workshop on Models, Algorithms and Methodologies for Hybrid Parallelism in New HPC Systems -- An experience report on (auto-)tuning of mesh-based PDE solvers on shared memory systems -- Using GPGPU accelerated interpolation algorithms for marine bathymetry processing with on-premises and cloud based computational resources -- Relaxing the correctness conditions on concurrent data structures for multicore CPUs. A numerical case study -- Energy analysis of a 4D Variational Data Assimilation algorithm and evaluation on ARM-based HPC systems -- Performance Assessment of the Incremental Strong Constraints 4DVAR Algorithm in ROMS -- Evaluation of HCM: a New Model to Predict the Execution Time of Regular Parallel Applications on a Heterogeneous Cluster -- Workshop on Power and Energy Aspects of Computations (PEAC 2017) -- Applicability of the Empirical Mode Decomposition for Power Traces of Large-Scale Applications -- Efficiency analysis of Intel, AMD and Nvidia 64-bit hardware for memory-bound problems: a case study of ab initio calculations with VASP 75 -- GPU Power Modeling of HPC Applications for the Simulation of Heterogeneous Clouds -- Bi-cluster Parallel Computing in Bioinformatics – Performance and Eco-efficiency -- Performance and energy analysis of scientific workloads executing on LPSoCs -- Energy efficient dynamic load balancing over multiGPU heterogeneous systems -- Workshop on Scheduling for Parallel Computing (SPC 2017) -- Scheduling Data Gathering with Maximum Lateness Objective -- Fair Scheduling in Grid VOs with Anticipation Heuristic -- A Security-Driven Approach to Online Job Scheduling in IaaS Cloud Computing Systems -- Dynamic Load Balancing Algorithm for Heterogeneous Clusters -- Multi-Objective Extremal Optimization in Processor Load Balancing for Distributed Programs -- Workshop on Language-Based Parallel Programming Models (WLPP 2017) -- Pardis: A Process Calculus for Parallel and Distributed Programming in Haskell -- Towards High-Performance Python.-Actor Model of a New Functional Language – Anemone -- Almost Optimal Column-wise Prefix-sum Computation on the GPU -- A Combination of Intra- and Inter-Place Work Stealing for the APGAS Library -- Benchmarking Molecular Dynamics with OpenCL on Many-Core Architectures -- Efficient Language-Based Parallelization of Computational Problems Using Cilk Plus -- A Taxonomy of Task-Based Technologies for High-Performance Computing -- Workshop on PGAS Programming -- Interoperability of GASPI and MPI in Large Scale Scientific Applications -- Evaluation of the parallel performance of the Java and PCJ on the Intel KNL based systems -- Fault-tolerance mechanisms for the Java parallel codes implemented with the PCJ library -- Exploring graph analytics with the PCJ toolbox -- Big Data analytics in Java with PCJ library: performance comparison with Hadoop -- Performance comparison of graph BFS implemented in MapReduce and PGAS programming models.-Minisymposium on HPC Applications in Physical Sciences -- Efficient Parallel Generation of Many-Nucleon Basis for Large-Scale AbInitio Nuclear Structure Calculations -- Parallel Exact Diagonalization Approach to Large Molecular Nanomagnets Modelling -- Application of Numerical Quantum Transfer-matrix Approach in the Randomly Diluted Quantum Spin Chains -- Minisymposium on High Performance Computing Interval Methods -- A new method for solving nonlinear interval and fuzzy equations -- Role of hull-consistency in the HIBA USNE multithreaded solver for nonlinear systems -- Parallel computing of linear systems with linearly dependent intervals in MATLAB -- What Decision to Make In a Conflict Situation under Interval Uncertainty: Efficient Algorithms for the Hurwicz Approach -- Practical Need for Algebraic (Equality-Type) Solutions of Interval Equations and for Extended-Zero Solutions -- Workshop on Complex Collective Systems -- Application of Local Search with Perturbation Inspired by Cellular Automata for Heuristic Optimization of Sensor Network Coverage Problem -- A Fuzzy Logic Inspired Cellular Automata Based Model for Simulating Crowd Evacuation Processes -- Nondeterministic Cellular Automaton for Modelling Urban Traffic with Self-organizing Control -- Towards Multi-Agent simulations accelerated by GPU -- Tournament-Based Convection Selection in Evolutionary Algorithms -- Multi-agent systems programmed visually with Google Blockly.

In: Springer eBooks

Weitere Ausg.: Printed edition: ISBN 9783319780535

Sprache: Englisch

Schlagwort(e): Konferenzschrift

DOI: 10.1007/978-3-319-78054-2

URL: http://dx.doi.org/10.1007/978-3-319-78054-2

URL: Volltext  (URL des Erstveröffentlichers)

URL: Volltext  (lizenzpflichtig)

UID:

Umfang: XXIV, 1831 p. 638 illus., 300 illus. in color. , online resource.

Ausgabe: 1st ed. 2020.

ISBN: 9789811532504

Serie: Lecture Notes in Electrical Engineering, 551

Inhalt: This book gathers the proceedings of the 9th International Conference on Frontier Computing, held in Kyushu, Japan on July 9-12, 2019, and provides comprehensive coverage of the latest advances and trends in information technology, science and engineering. It addresses a number of broad themes, including communication networks, business intelligence and knowledge management, web intelligence, and related fields that inspire the development of information technology. The respective contributions cover a wide range of topics: database and data mining, networking and communications, web and internet of things, embedded systems, soft computing, social network analysis, security and privacy, optical communication, and ubiquitous/pervasive computing. Many of the papers outline promising future research directions, and the book will benefit students, researchers and professionals alike. Further, it offers a useful reference guide for newcomers to the field.

Anmerkung: Chapter 1. Cloud, Ubiquitous, Pervasive, and High Performance Computing -- Chapter 2. Dependable, Reliable and Autonomic Computing -- Chapter 3. Wearable Computing, Mobile Web, and Smart Environment -- Chapter 4. Algorithm, Model, and Framework Programming Languages -- Chapter 5. Communication and Networking -- Chapter 6. Database and Data Mining -- Chapter 7. Big Data and Internet of Things -- Chapter 8. Anticipatory Computing -- Chapter 9. Web and Internet Computing -- Chapter 10. Natural Language Processing Operating Systems -- Chapter 11. Image Processing, Pattern Recognition, Multimedia Technology -- Chapter 12. Embedded System and Software -- Chapter 13. Geographical Information Systems/ Global Navigation Satellite Systems (GIS/GNSS) -- Chapter 14. Intelligent Information & Database Systems -- Chapter 15. Security and Privacy -- Chapter 16. Social Web, Network, and Computing -- Chapter 17. Social, Ethical & Other Issues of Networked World -- Chapter 18. Software Design Patterns & Engineering -- Chapter 19. Information/Business Management, and IT Policy -- Chapter 20. Mobile and Ubiquitous Computing -- Chapter 21. Modeling and Simulation.

In: Springer eBooks

Weitere Ausg.: Printed edition: ISBN 9789811532498

Weitere Ausg.: Printed edition: ISBN 9789811532511

Weitere Ausg.: Printed edition: ISBN 9789811532528

Sprache: Englisch

DOI: 10.1007/978-981-15-3250-4

URL: https://doi.org/10.1007/978-981-15-3250-4

URL: Volltext  (URL des Erstveröffentlichers)

URL: Buchcover

UID:

Umfang: X, 592 p. 204 illus. , online resource.

ISBN: 9783319747811

Serie: Lecture Notes in Computer Science, 10729

Inhalt: This book constitutes revised selected papers from the five workshops collocated with the 15th International Conference on Software Engineering and Formal Methods, SEFM 2017. The 38 papers presented in this volume were carefully reviewed and selected from a total of 55 submissions. They stem from the following workshops: DataMod 2017 -- 6th International Symposium “From Data to Models and Back"; FAACS 2017 --  1st Workshop on Formal Approaches for Advanced Computing Systems; MSE 2017 -- 1st Workshop on Microservices: Science and Engineering; CoSim-CPS 2017 -- 1st Workshop on Formal Co-Simulation of Cyber-Physical Systems; FOCLASA 2017 -- 15th International Workshop on Foundations Of Coordination Languages and Self-Adaptive Systems .

Anmerkung: DataMod -- Temporal Analytics for Software Usage Models -- Sequential Pattern Mining for ICT Risk Assessment and Prevention -- Student performance prediction and optimal course selection: An MDP approach -- An Algorithm for Simulating Human Selective Attention -- Learning Decision Trees from Synthetic Data Models for Human Security Behaviour -- Controlling Production Variances in Complex Business Processes -- A computational model of Internet addiction phenomena in social networks -- What belongs to context? A definition, a criterion and a method for deciding on what context-aware systems should sense and adapt to -- Finding all minimum-size DFA consistent with given examples: SAT-based approach -- FAACS -- Intercepting Blackhole Attacks in MANETs: An ASM-based Model -- Formalizing Monitoring Processes for Large-Scale Distributed Systems using Abstract State Machines -- Design-time to Run-time Verification of Microservices Based Applications -- Generalized Oracle for Testing Machine Learning Computer Programs -- MSE@SEFM 2017 -- A Formal Framework for Specifying and Verifying Microservices Based Process Flows -- Towards a Taxonomy of Microservices Architectures -- Towards a reference dataset of microservice-based applications -- Towards a UML Profile for Domain-driven Design of Microservice Architectures -- A Framework for Modelling Variable Microservices as Software Product Lines -- CoSim-CPS -- A Refinement Approach to Analyse Critical Cyber-Physical Systems -- Injecting Formal Verification in FMI-based Co-Simulations of Cyber-Physical Systems -- Integrated simulation and formal verification of a simple autonomous vehicle -- Co-Simulation between Trnsys and Simulink based on Type155 -- Development of a Driverless Lawn Mower using Co-Simulation -- Approximated Stability Analysis of Bi-Modal Hybrid Co-simulation Scenarios -- Towards Resilience-Explicit Modelling and Co-simulation of Cyber-Physical Systems -- Features of Integrated Model-based Co-modelling and Co-simulation Technology -- A Tool Integration Language to Formalize Co-simulation Tool-chains for Cyber-physical System (CPS) -- A Framework for Analyzing Adaptive Autonomous Aerial Vehicles -- Co-simulation of semi-autonomous systems: the Line Follower Robot case study -- A Framework for the Co-Simulation of Engine Controls and Task Scheduling -- Formalising Cosimulation Models -- FOCLASA -- Towards the performance analysis of elastic systems with e-Motions -- From (incomplete) TOSCA speci_cations to running applications, with Docker -- Combining Trust and Aggregate Computing -- Reasoning about Sensing Uncertainty in Decision-Making for Self-Adaptation -- Lightweight Preprocessing for Agent-Based Simulation of Smart Mobility Initiatives -- Using Coq for Formal Modeling and Verification of Timed Connectors -- An initial user study comparing the readability of a graphical coordination model with Event-B notation. .

In: Springer eBooks

Weitere Ausg.: Printed edition: ISBN 9783319747804

Sprache: Englisch

Fachgebiete: Informatik

Schlagwort(e): Konferenzschrift

DOI: 10.1007/978-3-319-74781-1

URL: http://dx.doi.org/10.1007/978-3-319-74781-1

URL: Volltext  (URL des Erstveröffentlichers)

URL: Volltext  (lizenzpflichtig)

UID:

Umfang: 1 online resource (684 pages)

ISBN: 9783110584998

Anmerkung: Intro -- Contents -- Preface -- Introduction of keynote speakers -- Part IV: Sensors, Instrument and Measurement II -- Design of Remote Real-Time Measuring System of Temperature and Humidity based on Raspberry Pi and Java Language -- Design of Emotional Physiological Signal Acquisition System -- EMC Effects On High-Resolution Spaceborne SAR Image -- Real-time Pupil Detection based on Contour Tracking -- Chip Manufacturing, Data Integration and Transmission -- A DCT-domain-based Research and Application of the Algorithm of Digital Audio Watermark -- Detection of Placido rings fracture based on ECC image registration -- Research on High-precision Calibration and Measurement Method based on Stereo Vision -- Comparison of Three Weak Small Moving Target Detection Methods based on Time Domain Filtering -- Breath Sounds Detection System based on SOPC -- A Novel Fiber-optic Sensor for the Determination of Melting Point of Solids -- Method for Measuring Internal Liquid Level of Sealed Metal Container by Ultrasonic -- Design of Silicon-on-Sapphire Pressure Sensor For High Temperature And High Pressure Applications -- The Federated Filtering Algorithm based on the Asynchronous Multisensor System -- A Kind of Self-tuning Kalman Filter for the High Maneuvering Target Tracking System -- A Multitasking Run Time Prediction Method based on GBDT in Satellite Ground Application System -- Unmanned Ground Vehicle Behavior Decision via Improved Bayesian Inverse Reinforcement Learning -- Analysis of the High Frequency Vibration on Radar Imaging in the Terahertz Band -- Object Tracking for Satellite Video based on Kernelized Correlation Filters and Three Frame Difference -- Noise Removal and Detail Enhancement of Passive Infrared Image Pretreatment Method for Robot Vision. , Failure Mechanism and Support Strategy of Deep Roadway with High Horizontal Stress and Broken Rock Masss -- Design of a Climbing Robot for Nuclear Environmental Monitoring -- Part V: Mechatronics and Electrical Engineering I -- The design and simulation of the new Space Release Device -- The Adjusting Method of Box Girder Pose based on Spatial Coordinate Transformation -- Application of Discrete Element Method in the Analysis of Loader Shovel Loading Process -- Application of Piecewise Catenary Method in Length Calculation of Soft Busbar in Ultra-high Voltage Substation -- Calculation Method of Stiffness Matrix in Non-linear Spline Finite Element for Suspension Cable -- A Load Outage Judgement Method Considering Voltage Sags -- Macro Program Application on Non-circular Curve Machining in CNC Lathe -- Singular Configuration Analysis for the Structure of Hybrid Grinding and Polishing Machine -- Static Analysis and Size Optimization for the Bed of Gantry Milling Machine based on ANSYS Workbench -- Research and Optimization of Clip Type Passive Manipulator -- Research on Material Removal of Belt Polishing for Blade Complex Surface -- Visual Servoing based object pick and place manipulation system -- Research on Wind Loads of Container Ship based on CFD -- Design and Research of Model Sting Support Control System of Icing Wind Tunnel -- Development of Control System of Icing Wind Tunnel -- Railway Track Collapse Monitoring System in Mining Area based on KALMAN Filter -- The Method of Harmonic Source Identification in Power Supply System -- Optimization for the Balancing Cylinder of a 3-DOF Planar Manipulator -- Finite Element Modal Analysis of an Eight-axis Industrial Robot Painting System Applied to Boarding Bridge Painting -- Bayesian based Fault Identification for Nonlinear Mechatronic System with Backlash. , A CAD/CAE Integrated Optimization of Hot Runner System -- Study On Tool Path Design for a Novel Incremental Sheet Metal Bending Process -- Research on Tribological Characteristics of 316L Stainless Steel against PEEKHPV under Water Lubrication -- Turbofan Engine Controller Optimal Design based on Grey Wolf Optimizer -- Part VI: Mechatronics and Electrical Engineering II -- Research of the EMI Suppression Circuit in the ASM Power -- Research on the Relationship Identification and Governance Countermeasures of Stakeholder in Two Phases of Thermoelectric Projects -- Study on the Fluctuating Pressure and Aerodynamic Noise at Car Rearview Mirror Zone -- Model and Simulation of Vehicle Based on Modelica Language -- Research on Asynchronous Starting Characteristics of Synchronous Motors Based on TSC Reactive Power Compensator -- Motorcycle Engine Controller Design and Matlab/ Simulink Simulation -- An Efficient Bilinear Factorization based Method For Motion Capture Data Refinement -- Reliability Evaluation of Embedded Real-time System based on Error Scenario -- Coordinate Transformation on CNC Machining of Quasi-Hypoid-Gear -- Study on the Influence of Rolling Wheels on Car External Flow Field and Aerodynamic Noise -- Hardware/Software Partitioning Algorithm under Multi-Constraints for the Optimization of Power Consumption -- Research of Metering Arithmetic for Distortion Power -- Study of the Influence of the Diode Ideality Factor on the Si Solar Cell -- Application of the Haar Classifier in Obstacle Target Detection -- Virtual Assembly Process Simulation for Hybrid Car Battery based on DELMIA -- Information Flow Integrity of ECPS based on Domain Partition -- Simulating the Time-Domain Response for Monopole Antennas Excited by DC Voltage Source -- Permanent Magnet Brushless DC Motor Driver Base On DSP56F8346. , The Study on the Power Transmission Line Icing Image Edge Detection based on DTW Measure Cluster Analysis.

Weitere Ausg.: Print version: Wang, Shawn X. Current Trends inComputer Science andMechanical Automation Vol. 2 Warschau/Berlin : Walter de Gruyter GmbH,c2018 ISBN 9783110584981

Sprache: Englisch

Schlagwort(e): Electronic books. ; Electronic books. ; Electronic books

URL: Click to View

URL: Click here to view book

URL: Full-text  ((OIS Credentials Required))

URL: lizenzpflichtig

UID:

Umfang: XI, 412 p. 91 illus., 80 illus. in color. , online resource.

Ausgabe: 1st ed. 2023.

ISBN: 9783031480164

Serie: Lecture Notes in Networks and Systems, 829

Inhalt: This book reflects the various dimensions of play. It gathers together experience with role-play, tabletop, and online games and develops and assesses tools. It also reflects the human condition in this world of games as it becomes a digital world. We are living in a World of Games where every game is a world through which we learn about the world. A World of Games is fun and engaging, but it also provides deceptive pleasures. What may seem like fun is far from harmless. And then there are the many ways of learning in the mode of play.

Anmerkung: Part I: From Building Blocks to Augmented Reality Glasses - Technologies for Gaming -- The Metaverse: Changing the Landscape of Media Education -- Application of Phygital Games at the University in the Context of Digitalization -- An EON-XR Augmented Reality Application for Motivation Stimulation and Vocabulary Training of Master's Degree Students Majoring in Civil Engineering -- Game Technologies and High-Fidelity Patient Simulation in the field of Psychology and Medicine -- Video Games in Teaching Audiovisual Translation to University Students -- Development of a Play and Program Mobile Application Based on the Gamification Methodology -- Experience of Non-linguistics Students Creating Online Games on Foreign Language Grammar -- Part II: Games in Various Educational Environments -- Using Game Practices to Identify Teams Capable of Generating Entrepreneurial Ideas -- The Phenomenon of "Social Responsibility" as a Construct of the Humanitarian Educational Ecosystem for the Training of Future Engineers: Perspectives, Forms, Approaches -- The Use of Gamification Elements for the Development of Creativity in Engineering -- Designing Tabletop Games for Individuals with Disabilities through Student Project activity -- Computer Games and Literary Education: Opportunities and Limitations -- A Gamification Conceptual Framework for Marketing Courses -- The Formative Role of "Model UN" in the Development of the Professional Personality of Diplomats -- Unlocking the Power of Gamification: Evaluating the Efficacy of Wizer.me in EFL Vocabulary Acquisition -- Assessment of the Creative Freedom of Students Trained in the Acting Technique "Demidov Études" -- The Development of Ethno-Cultural Empathy within a Multicultural Educational Environment: Peculiarities and Role-Playing Experiences -- Moot Court Competition in a Foreign Language : Developing Professional Competencies through a Business Game -- Gaming Technologies in the Formation of Legal Students' Professional Competencies: Moot Courts -- Technologies for Innovative Potential Development of University Students majoring in Engineering -- Gamification in Teaching Foreign Languages to Economics Students: A Case Study -- Visual Novels as a Means of Business Communication Skills Development for Computer Science Students -- WebQuest as a Means for Students' Soft Skills Development in Engineering Foreign Language Education -- Problem-Based Role Plays in Teaching English to Students of Humanities -- A Business Game Introduction into Foreign Language Training of Materials Science and Engineering Students -- Gamification in Foreign Language Education: Development of Lexical Skills in Teaching a Second Foreign Language at the University -- Gamified Communication as a Didactic tool for Mastering a Professionally Oriented Video Course in a Foreign Language -- The use of role-playing games to develop the skills of constructive communication of healthcare professionals -- The Use of Games in English Language Lessons as a Means of Communication.

In: Springer Nature eBook

Weitere Ausg.: Printed edition: ISBN 9783031480157

Weitere Ausg.: Printed edition: ISBN 9783031480171

Weitere Ausg.: Printed edition: ISBN 9783031480188

Sprache: Englisch

DOI: 10.1007/978-3-031-48016-4

URL: https://doi.org/10.1007/978-3-031-48016-4

URL: Volltext  (URL des Erstveröffentlichers)