Kooperativer Bibliotheksverbund

UID:

Format: X, 487 S. : , Ill.

Language: English

Subjects: Computer Science , Economics , Comparative Studies. Non-European Languages/Literatures

Keywords: Symbol ; Programmiersprache ; Verarbeitung ; Programmiersprache ; Programmierung ; Nichtnumerische Datenverarbeitung ; ALGOL 68 ; Konferenzschrift ; Konferenzschrift ; Konferenzschrift

UID:

Format: X, 487 S.

Edition: 2. print.

ISBN: 0-7204-2020-2

Language: English

Keywords: Symbol ; Programmiersprache ; Verarbeitung ; Nichtnumerische Datenverarbeitung ; ALGOL 68 ; Programmierung ; Konferenzschrift ; Konferenzschrift

UID:

Format: 1 online resource (251 p.)

Edition: 1st edition

ISBN: 1-281-04964-6 , 9786611049645 , 0-08-055313-3

Series Statement: The Morgan Kaufmann series in systems on silicon

Content: 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

Note: 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

Additional Edition: ISBN 0-12-370616-5

Language: English

UID:

Format: 1 online resource (705 pages)

ISBN: 9783030720193

Series Statement: Lecture Notes in Computer Science Ser. ; v.12648

Note: 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.

Additional Edition: Print version: Yoshida, Nobuko Programming Languages and Systems Cham : Springer International Publishing AG,c2021 ISBN 9783030720186

Language: English

Keywords: Electronic books. ; Electronic books

URL: Click to View

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

URL: lizenzpflichtig

UID:

Format: 1 online resource (369 pages)

Edition: 1st ed. 2024.

ISBN: 979-88-6880-137-2

Series Statement: Maker Innovations Series,

Content: Gain the skills required to dive into the fundamentals of the RISC-V instruction set architecture. This book explains the basics of code optimization, as well as how to interoperate with C and Python code, thus providing the starting points for your own projects as you develop a working knowledge of assembly language for various RISC-V processors. The RISC-V processor is the new open-source CPU that is quickly gaining popularity and this book serves as an introduction to assembly language programming for the processor in either 32- or 64-bit mode. You’ll see how to write assembly language programs for several single board computers, including the Starfive Visionfive 2 and the Espressif ESP32=C3 32-bit RISC-V microcontroller. The book also covers running RISC-V Linux with the QEMU emulator on and Intel/AMD based PC or laptop and all the tools required to do so. Moving on, you’ll examine the basics of the RISC-V hardware architecture, all the groups of RISC-V assembly language instructions and understand how data is stored in the computer’s memory. In addition, you’ll learn how to interface to hardware such as GPIO ports. With RISC-V Assembly Language Programming you’ll develop enough background to use the official RISC-V reference documentation for your own projects. What You'll Learn See how data is represented and stored in a RISC-V based computer Make operating system calls from assembly language and include other software libraries in projects Interface to various hardware devices Use the official RISC-V reference documentation.

Note: Includes index. , Intro -- Table of Contents -- About the Author -- About the Technical Reviewer -- Acknowledgments -- Introduction -- Chapter 1: Getting Started -- History and Evolution of the RISC-V CPU -- What You Will Learn -- Ten Reasons to Learn Assembly Language Programming -- Running Programs on RISC-V Systems -- Coding a Simple "Hello World" Program -- Hello World on the Starfive Visionfive 2 -- Programming Hello World in the QEMU Emulator -- Install QEMU on Windows -- Install QEMU on Linux -- Compiling in Emulated Linux -- About Hello World on the ESP32-C3 Microcontroller -- Summary -- Exercises -- Chapter 2: Loading and Adding -- Computers and Numbers -- Negative Numbers -- About Two's Complement -- RISC-V Assembly Instructions -- CPU Registers -- RISC-V Instruction Format -- About the GCC Assembler -- Adding Registers -- 32-bits in a 64-bit World -- Moving Registers -- About Pseudoinstructions -- About Immediate Values -- Loading the Top -- Shifting the Bits -- Loading Larger Numbers into Registers -- More Shift Instructions -- About Subtraction -- Summary -- Exercises -- Chapter 3: Tooling Up -- GNU Make -- Rebuild a Project -- Rule for Building .S files -- Define Variables -- Build with CMake -- Debugging with GDB -- Preparation to Debug -- Setup for Linux -- Start GDB -- Set Up gdb for the ESP32-C3 -- Debugging with GDB -- Summary -- Exercises -- Chapter 4: Controlling Program Flow -- Creating Unconditional Jumps -- Understanding Conditional Branches -- Using Branch Pseudoinstructions -- Constructing Loops -- Create FOR Loops -- Code While Loops -- Coding If/Then/Else -- Manipulating Logical Operators -- Using AND -- Using XOR -- Using OR -- Adopting Design Patterns -- Converting Integers to ASCII -- Using Expressions in Immediate Constants -- Storing a Register to Memory -- Why Not Print in Decimal? -- Performance of Branch Instructions. , Using Comparison Instructions -- Summary -- Exercises -- Chapter 5: Thanks for the Memories -- Defining Memory Contents -- Aligning Data -- About Program Sections -- Big vs. Little Endian -- Pros of Little Endian -- About Memory Addresses -- Loading a Register with an Address -- PC Relative Addressing -- Loading Data from Memory -- Combining Loading Addresses and Memory -- Storing a Register -- Optimizing Through Relaxing -- Converting to Uppercase -- Summary -- Exercises -- Chapter 6: Functions and the Stack -- About Stacks -- Jump and Link -- Nesting Function Calls -- Function Parameters and Return Values -- Managing the Registers -- Summary of the Function Call Algorithm -- Uppercase Revisited -- Stack Frames -- Stack Frame Example -- Defining Symbols -- Macros -- Include Directive -- Macro Definition -- Labels -- Why Macros? -- Using Macros to Improve Code -- Summary -- Exercises -- Chapter 7: Linux Operating System Services -- So Many Services -- Calling Convention -- Finding Linux System Call Numbers -- Return Codes -- Structures -- About Wrappers -- Converting a File to Uppercase -- Building .S Files -- Opening a File -- Error Checking -- Looping -- Summary -- Exercises -- Chapter 8: Programming GPIO Pins -- GPIO Overview -- In Linux, Everything is a File -- Flashing LEDs -- Moving Closer to the Metal -- Virtual Memory -- In Devices, Everything is Memory -- Registers in Bits -- GPIO Enable Registers -- GPIO Output Set Registers -- More Flashing LEDs -- GPIOTurnOn in Detail -- Root Access -- Summary -- Exercises -- Chapter 9: Interacting with C and Python -- Calling C Routines -- Printing Debug Information -- Preserving State -- Calling Printf -- Passing a String -- Register Masking Revisited -- Calling Assembly Routines from C -- Packaging the Code -- Static Library -- Shared Library -- Embedding Assembly Language Code inside C Code. , Calling Assembly from Python -- Summary -- Exercises -- Chapter 10: Multiply and Divide -- Multiplication -- Examples -- Division -- Division by Zero and Overflow -- Example -- Example: Matrix Multiplication -- Vectors and Matrices -- Multiplying 3x3 Integer Matrices -- Accessing Matrix Elements -- Register Usage -- Summary -- Exercises -- Chapter 11: Floating-Point Operations -- About Floating Point Numbers -- About Normalization and NaNs -- Recognizing Rounding Errors -- Defining Floating Point Numbers -- About Floating Point Registers -- The Status and Control Register -- Defining the Function Call Protocol -- Loading and Saving FPU Registers -- Performing Basic Arithmetic -- Calculating Distance Between Points -- Performing Floating-Point Conversions -- Floating-Point Sign Injection -- Comparing Floating-Point Numbers -- Example -- Summary -- Exercises -- Chapter 12: Optimizing Code -- Optimizing the Uppercase Routine -- Simplifying the Range Comparison -- Restricting the Problem Domain -- Tips for Optimizing Code -- Avoiding Branch Instructions -- Moving Code Out of Loops -- Avoiding Expensive Instructions -- Use Macros -- Loop Unrolling -- Delay Preserving Registers in Functions -- Keeping Data Small -- Beware of Overheating -- Summary -- Exercises -- Chapter 13: Reading and Understanding Code -- Browsing Linux & -- GCC Code -- Comparing Strings -- About the Algorithm -- Macros and Kernel Options -- Code Created by GCC -- Reverse Engineering and Ghidra -- Summary -- Exercises -- Chapter 14: Hacking Code -- Buffer Overrun Hack -- Causes of Buffer Overrun -- Stealing Credit Card Numbers -- Stepping Through the Stack -- Mitigating Buffer Overrun Vulnerabilities -- Do Not Use strcpy -- PIE Is Good -- Poor Stack Canaries Are the First to Go -- Preventing Code Running on the Stack -- Tradeoffs of Buffer Overflow Mitigation Techniques -- Summary. , Exercises -- Appendix A: The RISC-V Instruction Set -- RV32I Base Integer Instruction Set -- RV64I Base Integer Instruction Set-in Addition to RV32I -- RV32M Standard Extension -- RV64M Standard Extension-in Addition to RV32M -- RV32F Standard Extension -- RV64F Standard Extension-in Addition to RV32F -- RV32D Standard Extension -- RV64D Standard Extension-in Addition to RV32D -- Appendix B: Binary Formats -- Integers -- Floating Point -- Addresses -- Appendix C: Assembler Directives -- Appendix D: ASCII Character Set -- Appendix E: Answers to Exercises -- Chapter 2 -- Chapter 3 -- Chapter 5 -- Chapter 6 -- Chapter 8 -- Chapter 10 -- Chapter 12 -- Index.

Additional Edition: ISBN 979-88-6880-136-5

Language: English

DOI: 10.1007/979-8-8688-0137-2

URL: Volltext  (URL des Erstveröffentlichers)

UID:

Format: X, 487 S , graph. Darst

Language: English

Subjects: Philosophy

Keywords: Konferenzschrift

UID:

Format: X, 487 S. 8"

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

Language: Undetermined

UID:

Format: VIII, 251 p. , online resource.

ISBN: 9781461257493

Series Statement: Texts and Monographs in Computer Science,

Content: 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.

Note: 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

Additional Edition: Printed edition: ISBN 9781461257516

Language: English

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

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

URL: Volltext

UID:

Format: 1 online resource (XI, 590 p.)

Edition: 1st ed. 1981.

Edition: Online edition Springer Lecture Notes Archive ; 041142-5

ISBN: 3-540-38769-2

Series Statement: Lecture Notes in Computer Science, 118

Note: Bibliographic Level Mode of Issuance: Monograph , The complexity of manipulating hierarchically defined sets of rectangles -- The transformational machine: Theme and variations -- Probabilistic two-way machines -- A survey of some recent results on computational complexity in weak theories of arithmetic -- A survey on oracle techniques -- Time and space bounded complexity classes and bandwidth constrained problems -- Representations of graphs by means of products and their complexity -- Parsing strategies: A concise survey -- The art of dynamizing -- Fast parallel computation of polynomials using few processors -- Generalizations of Petri nets -- Partial match retrieval in implicit data structures -- A characterization of Floyd-provable programs -- Semantics of CSP via translation into CCS -- More about the "geography" of context-free languages -- On the power of algebraic specifications -- An application of the theory of free partially commutative monoids: Asymptotic densities of trace languages -- On the complexity of word problems in certain Thue systems -- On the transformation of derivation graphs to derivation trees -- Pushdown automata with restricted use of storage symbols -- Structured nets -- Retraceability, repleteness and busy beaver sets -- Combining T and level-N -- On realization and implementation -- Multiplicative complexity of a bilinear form over a commutative ring -- Making dynamic logic first-order -- Partial interpretations of program schemata -- Closure properties of the family of languages recognized by one-way two-head deterministic finite state automata -- Another hierarchy defined by multihead finite automata -- An extension of Rabin's complete proof concept -- How to find invariants for coloured Petri nets -- Relationships between probabilistic and deterministic tape complexity -- Grammatical levels of the position restricted grammars -- A general framework for comparing sequential and parallel rewriting -- A bin packing algorithm with complexity O(n log n) and performance 1 in the stochastic limit -- Codings of nonnegative integers -- The maximum k-flow in a network -- On the constructive description of graph languages accepted by finite automata -- Weighted multidimensional B-trees used as nearly optimal dynamic dictionaries -- Maximum flow in planar networks -- Probabilistic combinatorial optimization -- Time-processor trade-offs for universal parallel computers -- Negative results on the size of deterministic right parsers -- Key-equivalence of functional dependency statements systems -- On representation of dynamic algebras with reversion -- A framework for studying grammars -- On existence of complete predicate calculus in metamathematics without exponentiation -- On structural similarity of context-free grammars -- Axioms for the term-wise correctness of programs -- Complexity and entropy -- Axiomatic semantics of indirect addressing -- Testing of join dependency preserving by a modified chase method -- A starvation-free solution of the dining philosophers' problem by use of interaction systems -- Admissible representations of effective cpo's -- Preserving total order in constant expected time -- Constructive category theory (No. 1) -- Two pebbles don't suffice. , English

In: Springer eBooks

Additional Edition: ISBN 3-540-10856-4

Language: English

DOI: 10.1007/3-540-10856-4

URL: http://dx.doi.org/10.1007/3-540-10856-4

UID:

Format: 1 online resource (XII, 488 p.)

Edition: 1st ed. 1989.

Edition: Online edition Springer Lecture Notes Archive ; 041142-5

ISBN: 3-540-46153-1

Series Statement: Lecture Notes in Computer Science, 358

Content: The ISSAC'88 is the thirteenth conference in a sequence of international events started in 1966 thanks to the then established ACM Special Interest Group on Symbolic and Algebraic Manipulation (SIGSAM). For the first time the two annual conferences "International Symposium on Symbolic and Algebraic Computation" (ISSAC) and "International Conference on Applied Algebra, Algebraic Algorithms and Error-Correcting Codes" (AAECC) have taken place as a Joint Conference in Rome, July 4-8, 1988. Twelve invited papers on subjects of common interest for the two conferences are included in the proceedings and divided between this volume and the preceding volume of Lecture Notes in Computer Science which is devoted to AAECC-6. This book contains contributions on the following topics: Symbolic, Algebraic and Analytical Algorithms, Automatic Theorem Proving, Automatic Programming, Computational Geometry, Problem Representation and Solution, Languages and Systems for Symbolic Computation, Applications to Sciences, Engineering and Education.

Note: Bibliographic Level Mode of Issuance: Monograph , Dynamic maintenance of paths and path expressions on graphs -- Generic programming -- From a noncomputability result to new interesting definitions and computability results -- Symbolic derivation and automatic generation of parallel routines for finite element analysis -- Liouvillian first integrals of differential equations -- Fast reduction of the Risch differential equation -- An application of reduce to the approximation of F(X,Y) -- The use of symbolic computation in solving some non-relativistic quantum mechanical problems -- Experiments with quadtree representation of matrices -- Discovering inequality conditions in the analytical solution of optimization problems -- Can EXCALC be used to investigate high-dimensional cosmological models with non-linear Lagrangians? -- Gröbner trace algorithms -- Solving systems of algebraic equations -- Groebner bases in non-commutative algebras -- Greater easy common divisor and standard basis completion algorithms -- Experiments with a projection operator for algebraic decomposition -- Rational Newton algorithm for computing formal solutions of linear differential equations -- An ordinary differential equation solver for REDUCE -- A fixed point method for power series computation -- An algorithm for symbolic computation of center manifolds -- Shortest division chains in imaginary quadratic number fields -- Effective tests for cyclotomic polynomials -- The probability of relative primality of Gaussian integers -- Some computational aspects of root finding in GF(qm) -- Symbolic computation for Witt rings -- Computations with algebraic curves -- On the computational complexity of the resolution of plane curve singularities -- Generalized characteristic polynomials -- Decomposition of algebras -- Algebraic transformations of polynomial equations, symmetric polynomials and elimination -- Tetrahedrizing point sets in three dimensions -- A generalization of the roider method to solve the robot collision problem in 3D -- Symbolic analysis of planar drawings -- A geometrical decision algorithm based on the gröbner bases algorithm -- Solving permutation problems using rewriting systems -- Applying rewriting techniques to groups with power-commutation-presentations -- Efficient decision procedures for locally finite theories II -- Aformal approach to some usually informal techniques used in mathematical reasoning -- Decision procedures for elementary sublanguages of set theory. XIV. Three languages involving rank related constructs -- Computer algebra on MIMD machine -- Algebraic extensions and algebraic closure in Scratchpad II -- Software development for computer algebra or from ALDES/SAC-2 to WEB/Modula-2 -- Cayley, version 4: The user language -- Improved sparse multivariate polynomial interpolation algorithms -- Heuristic methods for operations with algebraic numbers -- Asymptotic estimation of oscillating functions using an interval calculus -- A new algorithm for computing symbolic limits using hierarchical series -- Verification of non-identities in algebras -- Equations in words -- Cayley factorization -- Complexity of computing the characters and the genre of a system of exterior differential equations. , English

In: Springer eBooks

Additional Edition: ISBN 3-540-51084-2

Language: English

DOI: 10.1007/3-540-51084-2

URL: http://dx.doi.org/10.1007/3-540-51084-2