Kooperativer Bibliotheksverbund

UID:

Umfang: 1 online resource (431 pages)

Ausgabe: 1st ed. 2025.

ISBN: 9789819606023 , 9819606020

Serie: Lecture Notes in Computer Science, 15469

Inhalt: This book constitutes the refereed proceedings of the 10th International Symposium on Dependable Software Engineering. Theories, Tools, and Applications, SETTA 2024, held in Hong Kong, China, during November 26–28, 2024. The 21 full papers included in this book were carefully reviewed and selected from 47 submissions. The purpose of the SETTA symposium series is to bring international researchers together to exchange research results and ideas on bridging the gap between formal methods and software engineering.

Anmerkung: -- Invited Talks. -- Synthesis from LTL with Reward Optimization in Sampled Oblivious Environments. -- Regular Papers. -- An Assertion-Based Separation Logic for Probabilistic Programs with Unbounded Loops. -- Extending Symbolic Heap to Support Shared Ownership. -- Constraint Based Invariant Generation with Modular Operations. -- Data-Dependent WAR Analysis for Efficient Task-Based Intermittent Computing. -- Can Language Models Pretend Solvers? Logic Code Simulation with LLM. -- Enhancing Multi-modal Regular Expression Synthesis via Large Language Models and Semantic Manipulations of Sub-Expressions. -- Formal Verification of RISC-V Processor Chisel Designs. -- The Principle of Staking: Formal Verification of Staking Smart Contract. -- A Contract-based Framework for Formal Verification of Embedded Software. -- Formalizing x86-64 ISA in Isabelle/HOL: A Binary Semantics for eBPF JIT Correctness. -- The Design of Intelligent Temperature Control System of Smart House with MARS. -- Universal Construction for Linearizable but Not Strongly Linearizable Concurrent Objects. -- Cache Behavior Analysis with SP-relative Addressing for WCET Estimation. -- Timing Analysis of Cause-Effect Chains for External Events with Finite Validity Intervals. -- Runtime Verification of Neural-Symbolic Systems. -- Eidos: Efficient, Imperceptible Adversarial 3D Point Clouds. -- MILE: A Mutation Testing Framework of In-Context Learning System. -- A Derivative-based Membership Algorithm for Enhanced Regular Expressions. -- NanoHook: An Efficient System Call Hooking Technique with One-Byte Invasive. -- Faster Lifetime-optimal Speculative Partial Redundancy Elimination for Goto-free Program. -- EDSLog: Efficient Log Anomaly Detection Method Based on Dataset Partitioning.

Weitere Ausg.: ISBN 9789819606016

Weitere Ausg.: ISBN 9819606012

Sprache: Englisch

DOI: 10.1007/978-981-96-0602-3

URL: Volltext  (URL des Erstveröffentlichers)

UID:

Umfang: X, 487 S. : , Ill.

Sprache: Englisch

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

Schlagwort(e): Symbol ; Programmiersprache ; Verarbeitung ; Programmiersprache ; Programmierung ; Nichtnumerische Datenverarbeitung ; ALGOL 68 ; Konferenzschrift ; Konferenzschrift ; Konferenzschrift

UID:

Umfang: X, 487 S.

Ausgabe: 2. print.

ISBN: 0-7204-2020-2

Sprache: Englisch

Schlagwort(e): Symbol ; Programmiersprache ; Verarbeitung ; Nichtnumerische Datenverarbeitung ; ALGOL 68 ; Programmierung ; Konferenzschrift ; Konferenzschrift

UID:

Umfang: 1 online resource (513 pages) : , illustrations.

Ausgabe: Second edition.

ISBN: 1-281-01011-1 , 0-08-047849-2 , 9786611010119

Serie: Morgan Kaufmann Series in Interactive Technologies

Anmerkung: Cover -- Contents -- Figure Credits -- Foreword -- Preface -- Chapter 1 Foundation for a Science of Data Visualisation -- Visualization Stages -- Experimental Semiotics Based on Perception -- Semiotics of Graphics -- Pictures as Sensory Languages -- Sensory versus Arbitrary Symbols -- Properties of Sensory and Arbitrary Representation -- Testing Claims about Sensory Representations -- Arbitrary Conventional Representations -- The Study of Arbitrary Conventional Symbols -- A Model of Perceptual Processing -- Stage 1: Parallel Processing to Extract Low-Level Properties of the Visual Scene -- Stage 2: Pattern Perception -- Stage 3: Sequential Goal-Directed Processing -- Types of Data -- Entities -- Relationships -- Attributes of Entities or Relationships -- Operations Considered as Data -- Metadata -- Conclusion -- Chapter 2 The Environment, Optics, Resolution and the Display -- The Environment -- Visible Light -- Ecological Optics -- Optical Flow -- Textured Surfaces and Texture Gradients -- The Paint Model of Surfaces -- The Eye -- The Visual Angle Defined -- The Lens -- Optics and Augmented-Reality Systems -- Optics in Virtual-Reality Displays -- Chromatic Aberration -- Receptors -- Simple Acuities -- Acuity Distribution and the Visual Field -- Brain Pixels and the Optimal Screen -- Spatial Contrast Sensitivity Function -- Visual Stress -- The Optimal Display -- Aliasing -- Number of Dots -- Superacuities and Displays -- Temporal Requirements of the Perfect Display -- Conclusion -- Chapter 3 Lightness, Brightness, Contrast and Constancy -- Neurons, Receptive Fields, and Brightness Illusions -- Simultaneous Brightness Contrast -- Mach Bands -- The Chevreul Illusion -- Simultaneous Contrast and Errors in Reading Maps -- Contrast Effects and Artifacts in Computer Graphics -- Edge Enhancement -- Luminance, Brightness, Lightness, and Gamma. , Luminance -- Brightness -- Adaptation, Contrast, and Lightness Constancy -- Contrast and Constancy -- Perception of Surface Lightness -- Lightness Differences and the Gray Scale -- Monitor Illumination and Monitor Surrounds -- Conclusion -- Chapter 4 Color -- Trichromacy Theory -- Color Blindness -- Color Measurement -- Change of Primaries -- CIE System of Color Standards -- Chromaticity Coordinates -- Color Differences and Uniform Color Spaces -- Opponent Process Theory -- Naming -- Cross-Cultural Naming -- Unique Hues -- Neurophysiology -- Categorical Colors -- Properties of Color Channels -- Color Appearance -- Color Contrast -- Saturation -- Brown -- Applications of Color in Visualization -- Application 1: Color Specification Interfaces and Color Spaces -- Application 2: Color for Labeling -- Application 3: Color Sequences for Data Maps -- Application 4: Color Reproduction -- Application 5: Color for Exploring Multidimensional Discrete Data -- Conclusion -- Chapter 5 Visual Attention and Information that Pops Out -- Searching the Visual Field -- Useful Field of View -- Tunnel Vision and Stress -- The Role of Motion in Attracting Attention -- Reading from the Iconic Buffer -- Preattentive Processing -- Rapid Area Judgments -- Coding with Combinations of Features -- Conjunctions with Spatial Dimensions -- Highlighting -- Designing a Symbol Set -- Neural Processing, Graphemes, and Tuned Receptors -- The Grapheme -- The Gabor Model and Texture in Visualization -- Texture Segmentation -- Tradeoffs in Information Density: An Uncertainty Principle -- Texture Coding Information -- Primary Perceptual Dimensions of Texture -- Generation of Distinct Textures -- Spatial-Frequency Channels, Orthogonality, and Maps -- Texture Resolution -- Texture Contrast Effects -- Other Dimensions of Visual Texture -- Texture Field Displays. , Glyphs and Multivariate Discrete Data -- Restricted Classification Tasks -- Speeded Classification Tasks -- Integral-Separable Dimension Pairs -- Monotonicity of Visual Attributes -- Multidimensional Discrete Data -- Stars, Whiskers, and Other Glyphs -- Conclusion -- Chapter 6 Static and Moving Patterns -- Gestalt Laws -- Proximity -- Similarity -- Connectedness -- Continuity -- Symmetry -- Closure -- Relative Size -- Figure and Ground -- More on Contours -- Perceiving Direction: Representing Vector Fields -- Comparing 2D Flow Visualization Techniques -- Perception of Transparency: Overlapping Data -- Pattern Learning -- The Perceptual Syntax of Diagrams -- The Grammar of Node-Link Diagrams -- The Grammar of Maps -- Patterns in Motion -- Form and Contour in Motion -- Moving Frames -- Expressive Motion -- Perception of Causality -- Perception of Animate Motion -- Enriching Diagrams with Simple Animation -- Conclusion -- Chapter 7 Visual Objects and Data Objects -- Image-Based Object Recognition -- Applications of Images in User Interfaces -- Structure-Based Object Recognition -- Geon Theory -- Silhouettes -- Faces -- The Object Display and Object-Based Diagrams -- The Geon Diagram -- Perceiving the Surface Shapes of Objects -- Spatial Cues for Representing Scalar Fields -- Integration of Cues for Surface Shape -- Interaction of Shading and Contour -- Guidelines for Displaying Surfaces -- Bivariate Maps: Lighting and Surface Color -- Cushion Maps -- Integration -- Conclusion -- Chapter 8 Space Perception and the Display of Data in Space -- Depth Cue Theory -- Perspective Cues -- Pictures Seen from the Wrong Viewpoint -- Occlusion -- Depth of Focus -- Cast Shadows -- Shape-from-Shading -- Eye Accommodation -- Structure-from-Motion -- Eye Convergence -- Stereoscopic Depth -- Problems with Stereoscopic Displays -- Making Effective Stereoscopic Displays. , Artificial Spatial Cues -- Depth Cues in Combination -- Task-Based Space Perception -- Tracing Data Paths in 3D Graphs -- Judging the Morphology of Surfaces and Surface Target Detection -- Patterns of Points in 3D Space -- Judging Relative Positions of Objects in Space -- Judging the Relative Movement of Self within the Environment -- Reaching for Objects -- Judging the "Up" Direction -- The Aesthetic Impression of 3D Space (Presence) -- Conclusion -- Chapter 9 Images, Worlds and Gestures -- Coding Words and Images -- The Nature of Language -- Visual and Spoken Language -- Images vs. Words -- Links between Images and Words -- Static Links -- Gestures as Linking Devices -- Deixis -- Symbolic Gestures -- Expressive Gestures -- Visual Momentum in Animated Sequences -- Animated Visual Languages -- Conclusion -- Chapter 10 Interacting with Visualizations -- Data Selection and Manipulation Loop -- Choice Reaction Time -- 2D Positioning and Selection -- Hover Queries -- Path Tracing -- Two-Handed Interaction -- Learning -- Control Compatibility -- Vigilance -- Exploration and Navigation Loop -- Locomotion and Viewpoint Control -- Frames of Reference -- Map Orientation -- Focus, Context, and Scale -- Rapid Interaction with Data -- Conclusion -- Chapter 11 Thinking with Visualizations -- Memory Systems -- Visual Working Memory -- Visual Working Memory Capacity -- Rensink's Model -- Eye Movements -- Accommodation -- Eye Movements, Search, and Monitoring -- Long-Term Memory -- Problem Solving with Visualizations -- Visual Problem Solving Processes -- The Problem Solving Strategy -- Visual Query Construction -- The Pattern-Finding Loop -- The Eye Movement Control Loop -- The Intrasaccadic Scanning Loop -- Implications for Interactive Visualization Design -- Interfaces to Knowledge Structures -- Creative Problem Solving -- Conclusion. , Appendix A Changing Primaries -- Appendix B CIE Color Measurement System -- Appendix C The Perceptual Evaluation of Visualization Techniques and Systems -- Research Goals -- Psychophysics -- Detection Methods -- Method of Adjustment -- Cognitive Psychology -- Structural Analysis -- Testbench Application for Discovery -- Structured Interviews -- Rating Scales -- Statistical Exploration -- Principal Components Analysis -- Multidimensional Scaling -- Clustering -- Multiple Regression -- Cross-Cultural Studies -- Child Studies -- Practical Problems in Conducting User Studies -- Experimenter Bias -- How Many Subjects to Use? -- Combinatorial Explosion -- Task Identification -- Controls -- Getting Help -- Bibliography -- Subject Index -- Author Index -- About the Author.

Weitere Ausg.: ISBN 1-55860-819-2

Weitere Ausg.: ISBN 1-4175-3693-4

Sprache: Englisch

Schlagwort(e): Electronic books.

URL: Click to View

UID:

Umfang: 1 online resource (251 p.)

Ausgabe: 1st edition

ISBN: 9786611049645 , 9781281049643 , 1281049646 , 9780080553139 , 0080553133

Serie: The Morgan Kaufmann series in systems on silicon

Inhalt: This book will explain how to verify SoC (Systems on Chip) logic designs using "formal? and "semiformal? verification techniques. The critical issue to be addressed is whether the functionality of the design is the one that the designers intended. Simulation has been used for checking the correctness of SoC designs (as in "functional? verification), but many subtle design errors cannot be caught by simulation. Recently, formal verification, giving mathematical proof of the correctness of designs, has been gaining popularity.For higher design productivity, it is essential to debug desig

Anmerkung: Description based upon print version of record. , Front Cover; Verification Techniques For System-Level Design; Copyright Page; Contents; Acknowledgments; Chapter 1 Introduction; Chapter 2 Higher-Level Design Methodology and Associated Verification Problems; 2.1 Introduction; 2.2 Issues in High-Level Design; 2.3 C/C++-Based Design and Specification Languages; 2.3.1 SpecC Language; 2.3.2 The Semantics of par Statements; 2.3.3 Relationship with Simulation Time; 2.4 System-Level Design Methodology Based on C/C++-Based Design and Specification Languages; 2.5 Verification Problems in High-Level Designs , Chapter 3 Basic Technology for Formal Verification3.1 The Boolean Satisfiability Problem; 3.2 The DPLL Algorithm; 3.3 Enhancements to Modern SAT Solvers; 3.4 Capabilities of Modern SAT Solvers; 3.5 Binary Decision Diagrams; 3.5.1 Manipulation of BDDs; 3.5.2 Variants of BDDs; 3.6 Automatic Test Pattern Generation Engines; 3.6.1 Single Stuck-at Testing for Combinational Circuits; 3.6.2 Stuck-at Testing in Sequential Circuits; 3.7 SAT, BDD, and ATPG Engines for Validation; 3.8 Theorem-Proving and Decision Procedures; References; Chapter 4 Verification Algorithms for FSM Models , 4.1 Combinational Equivalence Checking4.1.1 Sequential Equivalence Checking as Combinational Equivalence Checking; 4.1.2 Latch Mapping Problem; 4.1.3 EC Based on Internal Equivalences; 4.1.4 Anatomy and Capabilities of Modern CEC Tools; 4.2 Model Checking; 4.2.1 Modeling Concurrent Systems; 4.2.2 Temporal Logics; 4.2.3 Types of Properties; 4.2.4 Basic Model-Checking Algorithms; 4.2.5 Symbolic Model Checking; 4.3 Semi-Formal Verification Techniques; 4.3.1 SAT-Based Bounded Model Checking; 4.3.2 Symbolic Simulation; 4.3.3 Enhancing Simulation Using Formal Methods; 4.4 Conclusion; References , Chapter 5 Static Checking of Higher-Level Design Descriptions5.1 Program Slicing; 5.1.1 System Dependence Graph; 5.1.2 Nodes and Edges; 5.1.3 Concurrency; 5.1.4 Synchronization on Concurrent Processes; 5.2 Checking Method and Its Implying Design Flow; 5.2.1 Basic Static Description Checking; 5.2.2 Improvement of Accuracy Using Conditions of Control Nodes; 5.3 Application of the Checking Methods to HW/SW Partitioning and Optimization; 5.4 Case Study; 5.4.1 MPEG2; 5.4.2 JPEG2000; 5.4.3 Experimental Results on Static Checking; References , Chapter 6 Equivalence Checking on Higher-Level Design Descriptions6.1 Introduction; 6.2 High-Level Design Flow from the Viewpoint of Equivalence Checking; 6.3 Symbolic Simulation for Equivalence Checking; 6.4 Equivalence-Checking Methods Based on the Identification of Differences between two Descriptions; 6.4.1 Identification of Differences between Two Descriptions; 6.4.2 Symbolic Simulation Based on Textual Differences; 6.4.3 Example; 6.4.4 Experimental Results; 6.5 Further Improvement on the Use of Differences between Two Descriptions; 6.5.1 Extension of the Verification Area , 6.5.2 Symbolic Simulation on SDGs , English

Weitere Ausg.: ISBN 9780123706164

Weitere Ausg.: ISBN 0123706165

Sprache: Englisch

UID:

Umfang: 1 online resource (705 pages)

ISBN: 9783030720193

Serie: Lecture Notes in Computer Science Ser. ; v.12648

Anmerkung: Intro -- ETAPS Foreword -- Preface -- Organization -- Contents -- The Decidability of Verification under PS 2.0 -- 1 Introduction -- 2 Preliminaries -- 3 The Promising Semantics -- 4 Undecidability of Consistent Reachability in PS 2.0 -- 5 Decidable Fragments of PS 2.0 -- 5.1 Formal Model of LoHoW -- 5.2 Decidability of LoHoW with Bounded Promises -- 6 Source to Source Translation -- 6.1 Translation Maps -- 7 Implementation and Experimental Results -- 8 Related Work and Conclusion -- References -- Data Flow Analysis of Asynchronous Systems using Infinite Abstract Domains -- 1 Introduction -- 1.1 Motivating Example: Leader election -- 1.2 Challenges in property checking -- 1.3 Our Contributions -- 2 Background and Terminology -- 2.1 Modeling of Asynchronous Message Passing Systems as VCFGs -- 2.2 Data flow analysis over iVCFGs -- 3 Backward DFAS Approach -- 3.1 Assumptions and Definitions -- 3.2 Properties of Demand and Covering -- 3.3 Data Flow Analysis Algorithm -- 3.4 Illustration -- 3.5 Properties of the algorithm -- 4 Forward DFAS Approach -- 5 Implementation and Evaluation -- 5.1 Benchmarks and modeling -- 5.2 Data flow analysis results -- 5.3 Limitations and Threats to Validity -- 6 Related Work -- 7 Conclusions and Future Work -- References -- Types for Complexity of Parallel Computation in Pi-Calculus -- 1 Introduction -- 2 The Pi-calculus with Semantics for Work and Span -- 2.1 Syntax, Congruence and Standard Semantics for π-Calculus -- 2.2 Semantics and Complexity -- 2.3 An Example Process -- 3 Size Types for the Work -- 3.1 Size Input/Output Types -- 3.2 Subject Reduction -- 4 Types for Parallel Complexity -- 4.1 Size Types with Time -- 4.2 Examples -- 4.3 Complexity Results -- 5 An Example: Bitonic Sort -- 6 Related Work -- 7 Perspectives -- Acknowledgements -- References. , Checking Robustness Between Weak Transactional Consistency Models-5pt -- 1 Introduction -- 2 Overview -- 3 Consistency Models -- 3.1 Robustness -- 4 Robustness Against CC Relative to PC -- 5 Robustness Against PC Relative to SI -- 6 Proving Robustness Using Commutativity DependencyGraphs -- 7 Experimental Evaluation -- 8 Related Work -- References -- Verified Software Units -- 1 Introduction -- 2 Program verification using VST -- 3 VSU calculus -- 3.1 Components and soundness -- 3.2 Derived rules -- 4 APDs and specification interfaces -- 4.1 Abstract predicate declarations (APDs) -- 4.2 Abstract specification interfaces (ASIs) -- 4.3 Verification of ASI-specified compilation units -- 4.4 A VSU for a malloc-free library -- 4.5 Putting it all together -- 5 Modular verification of the Subject/Observer pattern -- 5.1 Specification and proof reuse -- 5.2 Pattern-level specification -- 6 Verification of object principles -- 7 Discussion -- References -- An Automated Deductive Verification Framework for Circuit-building Quantum Programs -- 1 Introduction -- 1.1 Quantum computing -- 1.2 The hybrid model. -- 1.3 The problem with quantum algorithms. -- 1.4 Goal and challenges. -- 1.5 Proposal. -- 1.6 Contributions. -- 1.7 Discussion. -- 2 Background: Quantum Algorithms and Programs -- 2.1 Quantum data manipulation. -- 2.2 Quantum circuits. -- 2.3 Reasoning on circuits and the matrix semantics. -- 2.4 Path-sum representation. -- 3 Introducing PPS -- 3.1 Motivating example. -- 3.2 Parametrizing path-sums. -- 4 Qbricks-DSL -- 4.1 Syntax of Qbricks-DSL. -- 4.2 Operational semantics. -- 4.3 Properties. -- 4.4 Universality and usability of the chosen circuit constructs. -- 4.5 Validity of circuits. -- 4.6 Denotational semantics. -- 5 Qbricks-Spec -- 5.1 Syntax of Qbricks-Spec. -- 5.2 The types pps and ket. -- 5.3 Denotational semantics of the new types. , 5.4 Regular sequents in Qbricks-Spec. -- 5.5 Parametricity of PPS. -- 5.6 Standard matrix semantics and correctness of PPS semantics. -- 6 Reasoning on Quantum Programs -- 6.1 HQHL judgments. -- 6.2 Deduction rules for term constructs. -- 6.3 Deduction rules for pps. -- 6.4 Equational reasoning. -- 6.5 Additional deductive rules. -- 7 Implementation -- 8 Case studies and experimental evaluation -- 8.1 Examples of formal specifications. -- 8.2 Experimental evaluation. -- 8.3 Prior verification efforts. -- 8.4 Evaluation: benefits of PPS and Qbricks. -- 9 Related works -- 10 Conclusion -- Acknowledgments. -- References -- Nested Session Types -- 1 Introduction -- 2 Overview of Nested Session Types -- 3 Description of Types -- 4 Type Equality -- 4.1 Type Equality Definition -- 4.2 Decidability of Type Equality -- 5 Practical Algorithm for Type Equality -- 5.1 Type Equality Declarations -- 6 Formal Language Description -- 6.1 Basic Session Types -- 6.2 Type Safety -- 7 Relationship to Context-Free Session Types -- 8 Implementation -- 9 More Examples -- 10 Further Related Work -- 11 Conclusion -- References -- Coupled Relational Symbolic Execution for Differential Privacy -- 1 Introduction -- 2 CRSE Informally -- 3 Preliminaries -- 4 Concrete languages -- 4.1 PFOR -- 4.2 RPFOR -- 5 Symbolic languages -- 5.1 SPFOR -- 5.2 SRPFOR -- 6 Metatheory -- 7 Strategies for counterexample finding -- 8 Examples -- 9 Related Works -- 10 Conclusion -- References -- Graded Hoare Logic and its Categorical Semantics -- 1 Introduction -- 2 Overview of GHL and Prospectus of its Model -- 3 Loop Language and Graded Hoare Logic -- 3.1 Preliminaries -- 3.2 The Loop Language -- 3.3 Assertion Logic -- 3.4 Graded Hoare Logic -- 3.5 Example Instantiations of GHL -- 4 Graded Categories -- 4.1 Homogeneous Coproducts in Graded Categories. , 4.2 Graded Freyd Categories with Countable Coproducts -- 4.3 Semantics of The Loop Language in Freyd Categories -- 5 Modelling Graded Hoare Logic -- 5.1 Interpretation of the Assertion Logic using Fibrations -- 5.2 Interpretation of Graded Hoare Logic -- 5.3 Instances of Graded Hoare Logic -- 6 Related Work -- 7 Conclusion -- References -- Do Judge a Test by its Cover -- 1 Introduction -- 2 Classical Combinatorial Testing -- 3 Generalizing Coverage -- 4 Sparse Test Descriptions -- 4.1 Encoding "Eventually" -- 4.2 Defining Coverage -- 5 Thinning Generators with QuickCover -- 5.1 Online Generator Thinning -- 6 Evaluation -- 6.1 Case Study: Normalization Bugs in System F -- 6.2 Case Study: Strictness Analysis Bugs in GHC -- 7 Related Work -- 7.1 Generalizations of Combinatorial Testing -- 7.2 Comparison with Enumerative Property-Based Testing -- 7.3 Comparison with Fuzzing Techniques -- 8 Conclusion and Future Work -- 8.1 Variations -- 8.2 Combinatorial Coverage of More Types -- 8.3 Regular Tree Expressions for Directed Generation -- Acknowledgments -- References -- For a Few Dollars More -- 1 Introduction -- 2 Specification of Algorithms With Resources -- 2.1 Nondeterministic Computations With Resources -- 2.2 Atomic Operations and Control Flow -- 2.3 Refinement on NREST -- 2.4 Refinement Patterns -- 3 LLVM With Cost Semantics -- 3.1 Basic Monad -- 3.2 Shallowly Embedded LLVM Semantics -- 3.3 Cost Model -- 3.4 Reasoning Setup -- 3.5 Primitive Setup -- 4 Automatic Refinement -- 4.1 Heap nondeterminism refinement -- 4.2 The Sepref Tool -- 4.3 Extracting Hoare Triples -- 4.4 Attain Supremum -- 5 Case Study: Introsort -- 5.1 Specification of Sorting -- 5.2 Introsort's Idea -- 5.3 Quicksort Scheme -- 5.4 Final Insertion Sort -- 5.5 Separating Correctness and Complexity Proofs -- 5.6 Refining to LLVM -- 5.7 Benchmarks -- 6 Conclusions -- 6.1 Related Work. , 6.2 Future Work -- References -- Run-time Complexity Bounds Using Squeezers -- 1 Introduction -- 2 Overview -- 3 Complexity Analysis based on Squeezers -- 3.1 Time complexity as a function of rank -- 3.2 Complexity decomposition by partitioned simulation -- 3.3 Extraction of recurrence relations over ranks -- 3.4 Establishing the requirements of the recurrence relations extraction -- 3.5 Trace-length vs. state-size recurrences with squeezers -- 4 Synthesis -- 4.1 SyGuS -- 4.2 Verification -- 5 Empirical Evaluation -- 5.1 Experiments -- 5.2 Case study: Subsets example -- 6 Related Work -- 7 Conclusion -- Acknowledgements. -- References -- Complete trace models of state and control -- 1 Introduction -- 2 HOSC -- 3 HOSC[HOSC] -- 3.1 Names and abstract values -- 3.2 Actions and traces -- 3.3 Extended syntax and reduction -- 3.4 Configurations -- 3.5 Transitions -- 3.6 Correctness and full abstraction -- 4 GOSC[HOSC] -- 5 HOS[HOSC] -- 6 GOS[HOSC] -- 7 Concluding remarks -- 8 Related Work -- References -- Session Coalgebras: A Coalgebraic View on Session Types and Communication Protocols -- 1 Introduction -- 2 Session Types -- 3 Session Coalgebra -- 3.1 Alternative Presentation of Session Coalgebras -- 3.2 Coalgebra of Session Types -- 4 Type Equivalence, Duality and Subtyping -- 4.1 Bisimulation -- 4.2 Duality -- 4.3 Parallelizability -- 4.4 Simulation and Subtyping -- 4.5 Decidability -- 5 Typing Rules -- 5.1 A Session π-calculus -- 5.2 Typing Rules -- 6 Algorithmic Type Checking -- 7 Concluding Remarks -- References -- Correctness of Sequential Monte Carlo Inference for Probabilistic Programming Languages -- 1 Introduction -- 2 A Motivating Example from Phylogenetics -- 3 A Calculus for Probabilistic Programming Languages -- 3.1 Syntax -- 3.2 Semantics -- 3.3 Resampling Semantics -- 4 The Target Measure of a Program -- 4.1 A Measure Space over Traces. , 4.2 A Measurable Space over Terms.

Weitere Ausg.: Print version: Yoshida, Nobuko Programming Languages and Systems Cham : Springer International Publishing AG,c2021 ISBN 9783030720186

Sprache: Englisch

Schlagwort(e): Electronic books. ; Electronic books

URL: Click to View

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

URL: lizenzpflichtig

UID:

Umfang: 1 online resource (ix, 476 pages) : , illustrations.

ISBN: 0-262-27718-2 , 0-585-04844-4 , 9780262277181

Serie: Complex adaptive systems

Inhalt: There is increasing interest in genetic programming by both researchers and professional software developers. These twenty-two invited contributions show how a wide variety of problems across disciplines can be solved using this new paradigm.There is increasing interest in genetic programming by both researchers and professional software developers. These twenty-two invited contributions show how a wide variety of problems across disciplines can be solved using this new paradigm.Advances in Genetic Programming reports significant results in improving the power of genetic programming, presenting techniques that can be employed immediately in the solution of complex problems in many areas, including machine learning and the simulation of autonomous behavior. Popular languages such as C and C++ are used in many of the applications and experiments, illustrating how genetic programming is not restricted to symbolic computing languages such as LISP. Researchers interested in getting started in genetic programming will find information on how to begin, on what public domain code is available, and on how to become part of the active genetic programming community via electronic mail.A major focus of the book is on improving the power of genetic programming. Experimental results are presented in a variety of areas, including adding memory to genetic programming, using locality and "demes" to maintain evolutionary diversity, avoiding the traps of local optima by using coevolution, using noise to increase generality, and limiting the size of evolved solutions to improve generality.Significant theoretical results in the understanding of the processes underlying genetic programming are presented, as are several results in the area of automatic function definition. Performance increases are demonstrated by directly evolving machine code, and implementation and design issues for genetic programming in C++ are discussed.

Anmerkung: "A Bradford book." , Available through MITCogNet. , A perspective on the work in this book / Kenneth E. Kinnear, Jr. -- Introduction to genetic programming / John R. Koza -- The evolution of evolvability in genetic programming / Lee Altenberg -- Genetic programming and emergent intelligence / Peter J. Angeline -- Scalable learning in genetic programming using automatic function definition / John R. Koza -- Alternatives in automatic function definition: a comparison of performance / Kenneth E. Kinnear, Jr. -- The donut problem: scalability, generalization and breeding policies in genetic programming / Walter Alden Tackett, Aviram Carmi -- Effects of locality in individual and population evolution / Patrik D'haeseleer, Jason Bluming -- The evolution of mental models / Astro Teller -- Evolution of obstacle avoidance behavior: using noise to promote robust solutions / Craig W. Reynolds -- Pygmies and civil servants / Conor Ryan -- Genetic programming using a minimum decsription length principle / Hitoshi Iba, Hugo de Garis, Taisuke Sato -- Genetic programming in C++: implementation issues / Mike J. Keith, Martin C. Martin. A compiling genetic programming system that directly manipulates the machine code / Peter Nordin -- Automatic generation of programs for crawling and walking / Graham Spencer -- Genetic programming for the acquisition of double auction market strategies / Martin Andrews, Richard Prager -- Two scientific applications of genetic programming: stack filters and non-linear equation fitting to chaotic data / Howard Oakley -- The automatic generation of plans for a mobile robot via genetic programming with automatically defined functions / Simon G. Handley -- Competitively evolving decision trees against fixed training cases for natural language processing / Eric V. Siegel -- Cracking and co-evolving randomizers / Jan Jannink -- Optimizing confidence of text classification by evolution of symbolic expressions / Brij Masand -- Evolvable 3D modeling for model-based object recognition systems / Thang Nguyen, Thomas Huang. Automatically defined features: the simultaneous evolution of 2-dimensional feature detectors and an algorithm for using them / David Andre -- Genetic micro programming of neural networks / Frédéric Gruau. , English

Weitere Ausg.: ISBN 0-262-51553-9

Weitere Ausg.: ISBN 0-262-11188-8

Sprache: Englisch

URL: lizenzpflichtig

URL: lizenzpflichtig

URL: MIT CogNet

URL: OCLC metadata license agreement

UID:

Umfang: X, 487 S , graph. Darst

Sprache: Englisch

Fachgebiete: Philosophie

Schlagwort(e): Konferenzschrift

UID:

Umfang: X, 487 S. 8"

Anmerkung: [Nebent.:] IFIP Working Conference on Symbol Manipulation Languages , Literaturverz. S. 358-437

Sprache: Unbestimmte Sprache

UID:

Umfang: VIII, 251 p. , online resource.

ISBN: 9781461257493

Serie: Texts and Monographs in Computer Science,

Inhalt: Computability theory is at the heart of theoretical computer science. Yet, ironically, many of its basic results were discovered by mathematical logicians prior to the development of the first stored-program computer. As a result, many texts on computability theory strike today's computer science students as far removed from their concerns. To remedy this, we base our approach to computability on the language of while-programs, a lean subset of PASCAL, and postpone consideration of such classic models as Turing machines, string-rewriting systems, and p. -recursive functions till the final chapter. Moreover, we balance the presentation of un solvability results such as the unsolvability of the Halting Problem with a presentation of the positive results of modern programming methodology, including the use of proof rules, and the denotational semantics of programs. Computer science seeks to provide a scientific basis for the study of information processing, the solution of problems by algorithms, and the design and programming of computers. The last 40 years have seen increasing sophistication in the science, in the microelectronics which has made machines of staggering complexity economically feasible, in the advances in programming methodology which allow immense programs to be designed with increasing speed and reduced error, and in the develop­ ment of mathematical techniques to allow the rigorous specification of program, process, and machine.

Anmerkung: 1 Introduction -- 1.1 Partial Functions and Algorithms -- 1.2 An Invitation to Computability Theory -- 1.3 Diagonalization and the Halting Problem -- 2 The Syntax and Semantics of while-Programs -- 2.1 The Language of while-Programs -- 2.2 Macro Statements -- 2.3 The Computable Functions -- 3 Enumeration and Universality of the Computable Functions -- 3.1 The Effective Enumeration of while-Programs -- 3.2 Universal Functions and Interpreters -- 3.3 String-Processing Functions -- 3.4 Pairing Functions -- 4 Techniques of Elementary Computability Theory -- 4.1 Algorithmic Specifications -- 4.2 The s-m-n Theorem -- 4.3 Undecidable Problems -- 5 Program Methodology -- 5.1 An Invitation to Denotational Semantics -- 5.2 Recursive Programs 110 5.3* Proof Rules for Program Properties -- 6 The Recursion Theorem and Properties of Enumerations -- 6.1 The Recursion Theorem -- 6.2 Model-Independent Properties of Enumerations -- 7 Computable Properties of Sets (Part 1) -- 7.1 Recursive and Recursively Enumerable Sets -- 7.2 Indexing the Recursively Enumerable Sets -- 7.3 Gödel’s Incompleteness Theorem -- 8 Computable Properties of Sets (Part 2) -- 8.1 Rice’s Theorem and Related Results -- 8.2 A Classification of Sets -- 9 Alternative Approaches to Computability -- 9.1 The Turing Characterization -- 9.2 The Kleene Characterization -- 9.3 Symbol-Manipulation Systems and Formal Languages -- References -- Notation Index -- Author Index.

In: Springer eBooks

Weitere Ausg.: Printed edition: ISBN 9781461257516

Sprache: Englisch

DOI: 10.1007/978-1-4612-5749-3

URL: http://dx.doi.org/10.1007/978-1-4612-5749-3

URL: Volltext