Kooperativer Bibliotheksverbund

UID:

Format: 1 online resource (377 pages)

Edition: 1st ed.

ISBN: 9789811365287

Note: Intro -- Preface -- Contents -- 1 Introduction to Computational Thinking Education -- 1.1 Introduction -- 1.2 Conceptual Framework and Chapters in This Book -- 1.2.1 Sub-theme 1: Computational Thinking and Tool Development -- 1.2.2 Sub-theme 2: Student Competency and Assessment -- 1.2.3 Sub-theme 3: Computational Thinking and Programming Education in K-12 -- 1.2.4 Sub-theme 4: Computational Thinking in K-12 STEM Education and Non-formal Learning -- 1.2.5 Sub-theme 5: Teacher and Mentor Development in K-12 Education -- 1.2.6 Sub-theme 6: Computational Thinking in Educational Policy and Implementation -- References -- Computational Thinking and Tool Development -- 2 Computational Thinking-More Than a Variant of Scientific Inquiry! -- 2.1 Introduction -- 2.1.1 Origins of the Current Debate -- 2.1.2 Computational Thinking for K-12 -- 2.1.3 Model Progression: The Use-Modify-Create Scheme -- 2.1.4 The CT Terminology -- 2.2 Basic Concepts and Building Blocks -- 2.2.1 "Computational Models" and "Models of Computation" -- 2.2.2 The Notion of "Abstraction" -- 2.2.3 Languages, Representations, and Microworlds -- 2.2.4 CT from the Perspective of Inquiry Learning in Science -- 2.2.5 Interim Summary -- 2.3 Specific Approaches and Examples -- 2.3.1 From Reactive Rule-Based Programming to Block Structures -- 2.3.2 "Computational Metacognition" -- 2.4 Conclusion -- References -- 3 MIT App Inventor: Objectives, Design, and Development -- 3.1 Introduction -- 3.2 MIT App Inventor Overview -- 3.3 MIT App Inventor Design Goals -- 3.3.1 Component Abstraction for Platform Behavior -- 3.3.2 Blocks as Logic -- 3.3.3 Mental Modeling -- 3.3.4 Fast Iteration and Design Using the Companion -- 3.4 The History of MIT App Inventor -- 3.4.1 Inception at Google -- 3.4.2 Educational Expansion at MIT -- 3.5 MIT App Inventor in Education -- 3.5.1 Massive Open Online Courses. , 3.5.2 MIT Master Trainers Program -- 3.5.3 Extensions -- 3.5.4 Research Projects -- 3.6 Empowerment Through Programming -- 3.6.1 From Theoretical to Practical -- 3.6.2 Computational Thinking -- 3.6.3 Computational Action -- 3.6.4 Supporting a Community Around Computation and App Creation -- 3.7 Discussion -- 3.7.1 Common Misconceptions -- 3.7.2 Limitations -- 3.7.3 Benefits of Visual Programming for Mobile -- 3.8 Conclusions -- 3.8.1 Future Vision -- References -- Student Competency and Assessment -- 4 Measuring Secondary School Students' Competence in Computational Thinking in ICILS 2018-Challenges, Concepts, and Potential Implications for School Systems Around the World -- 4.1 Introduction: The Relevance of Researching Teaching and Learning Computational Thinking in Schools -- 4.2 Researching Students' Achievement in Computational Thinking in the Context of ICILS 2018 -- 4.2.1 ICILS 2018-Assessing Students' Readiness for the Digital World in the Scope of an International Comparative Study -- 4.2.2 Computational Thinking as Part of ICILS 2018 -- 4.3 Relevance and Potential Outcomes for Educational Systems Around the World -- References -- 5 Computational Thinking Processes and Their Congruence with Problem-Solving and Information Processing -- 5.1 Introduction -- 5.2 Current State of Research -- 5.2.1 Computational Thinking and Problem-Solving -- 5.2.2 Computational Thinking and Information Processing -- 5.2.3 Computational Thinking Processes -- 5.2.4 In-School Acquisition of Competences in the Field of Computational Thinking -- 5.3 Research Concept -- 5.3.1 Study and Data Basis -- 5.3.2 Methodology and Expected Outcomes -- 5.4 Summary and Outlook -- References -- 6 Combining Assessment Tools for a Comprehensive Evaluation of Computational Thinking Interventions -- 6.1 Introduction -- 6.2 Computational Thinking Assessment Tools. , 6.3 Convergent Validity Studies -- 6.4 A Comprehensive Evaluation of Computational Thinking Interventions -- 6.5 Conclusions and Further Research -- References -- 7 Introducing and Assessing Computational Thinking in the Secondary Science Classroom -- 7.1 Introduction -- 7.2 Theoretical Orientation -- 7.3 Method -- 7.3.1 Study Design -- 7.3.2 Participants -- 7.3.3 CT-STEM Units -- 7.3.4 Data Collection -- 7.3.5 Analytic Approach -- 7.4 Findings -- 7.4.1 Learning Objective 1: Explore a Model by Changing Parameters -- 7.4.2 Learning Objective 2: Identify Simplifications Made by a Model -- 7.5 Discussion -- References -- 8 Components and Methods of Evaluating Computational Thinking for Fostering Creative Problem-Solvers in Senior Primary School Education -- 8.1 Introduction -- 8.2 Background -- 8.2.1 Computational Thinking -- 8.2.2 The Adopted Framework for Computational Thinking Evaluation -- 8.3 Methodology -- 8.4 Results and Discussion Based on Literature Review -- 8.4.1 CT Concepts -- 8.4.2 CT Practices -- 8.4.3 CT Perspectives -- 8.5 Conclusion -- References -- Computational Thinking and Programming Education in K-12 -- 9 Learning Composite and Prime Numbers Through Developing an App: An Example of Computational Thinking Development Through Primary Mathematics Learning -- 9.1 Introduction -- 9.2 Background -- 9.2.1 CT Framework -- 9.2.2 Block-Based Programming Environments -- 9.2.3 Mathematics Learning and CT Development -- 9.2.4 Learning Composite and Prime Numbers in Primary School Mathematics -- 9.3 Developing an App as Pedagogy for Supporting the Conceptual Understanding of Composite and Prime Numbers -- 9.3.1 Inquiry Activities About Composite and Prime Numbers -- 9.3.2 Developing an App as Pedagogy -- 9.3.3 Problem Decomposition and Algorithmic Thinking -- 9.3.4 Reusing Code from a Simple App to Build an App to Find Factors. , 9.3.5 Testing the App and Connecting the Tasks with the Digital World -- 9.3.6 Using '1' and '0' to Trigger In-depth Discussion of Composite and Prime Numbers -- 9.3.7 Adding a Conditional Statement to the App to Handle the Case of Inputting 0 -- 9.4 Computational Thinking Development -- 9.4.1 CT Concepts Development -- 9.4.2 CT Practices Development -- 9.4.3 CT Perspectives Development -- 9.5 Conclusion -- References -- 10 Teaching Computational Thinking Using Mathematics Gamification in Computer Science Game Tournaments -- 10.1 Introduction -- 10.2 Algebra Gamification -- 10.3 Mathematics Gamification of Algebra Maze -- 10.4 Mathematics Gamification of Algebra Game -- 10.5 Case Study of Computer Science Challenge Game Tournament -- 10.6 Further Discussions -- 10.7 Conclusions -- References -- 11 Mathematics Learning: Perceptions Toward the Design of a Website Based on a Fun Computational Thinking-Based Knowledge Management Framework -- 11.1 Introduction -- 11.1.1 Problem -- 11.1.2 Objectives -- 11.2 Literature Review -- 11.2.1 Computational Thinking (CT) -- 11.2.2 Game-Based Learning and Gamification -- 11.2.3 Knowledge Management -- 11.3 Methodology -- 11.3.1 Website Component Design Based on Computational Thinking (CT) -- 11.4 Pilot Test: Preliminary Design and Analysis -- 11.5 Alpha Testing: Design and Development -- 11.5.1 Alpha User Testing -- 11.6 Beta Testing -- 11.7 Comparison Between Alpha-Beta User Testings -- 11.8 Significance -- 11.9 Conclusion -- References -- Computational Thinking in K-12 STEM Education and Non-formal Learning -- 12 Defining and Assessing Students' Computational Thinking in a Learning by Modeling Environment -- 12.1 Introduction -- 12.2 Related Work -- 12.3 The STEM + CT Framework -- 12.3.1 The STEM + CT Framework -- 12.3.2 The Learning Environment -- 12.3.3 The Assessment Framework -- 12.4 Results and Discussion. , 12.4.1 Overall Learning Gains -- 12.4.2 The Correlations and Synergies in STEM and CT Learning -- 12.4.3 The Use of STEM + CT Practices -- 12.5 Conclusions -- References -- 13 Roles, Collaboration, and the Development of Computational Thinking in a Robotics Learning Environment -- 13.1 Introduction -- 13.1.1 Computational Thinking -- 13.1.2 Educational Robotics and Computational Thinking -- 13.1.3 Collaborative Learning with Robotics: Emergent Roles -- 13.1.4 Research Questions -- 13.2 Methods -- 13.2.1 Phase I-Behavior Analysis: Roles and Collaboration -- 13.2.2 Phase II-Discourse Analysis: Computational Thinking -- 13.2.3 Phase III-Descriptive Statistics: Roles -- 13.2.4 Phase IV-Difficulty Score Calculation: Learning Outcomes -- 13.3 Results -- 13.3.1 Role Transitions -- 13.3.2 Collaboration -- 13.3.3 Computational Thinking -- 13.4 Discussion -- References -- 14 Video Games: A Potential Vehicle for Teaching Computational Thinking -- 14.1 Introduction -- 14.2 Computational Thinking Skills -- 14.3 Methodology -- 14.4 Results and Discussion -- 14.5 Implications for Educators and Researchers -- Appendix 1: Survey-Video Game Experience -- Appendix 2: Homework Exercise-Describing My Favourite Game -- References -- 15 Transforming the Quality of Workforce in the Textile and Apparel Industry Through Computational Thinking Education -- 15.1 Introduction -- 15.1.1 Business Challenges and Opportunities -- 15.1.2 People Challenges -- 15.2 "You Can Code" Campaign (2015−2016) -- 15.2.1 Champaign Design and Implementation -- 15.2.2 Value Created from the Campaign -- 15.2.3 Employee Empowerment-From Reactive to Proactive, from Follower to Owner -- 15.3 From Computational Thinking to Computational Action -- 15.3.1 Development of Esquel Carpool App -- 15.3.2 The Idea of Esquel Carpool App -- 15.3.3 Impact from Esquel Carpool App. , 15.4 From Programming to Internet of Things.

Additional Edition: Print version: Kong, Siu Cheung Computational Thinking Education Singapore : Springer Singapore Pte. Limited,c2019 ISBN 9789811365270

Language: English

Subjects: Computer Science

Keywords: Electronic books. ; Aufsatzsammlung ; Aufsatzsammlung

URL: Click to View

URL: Volltext  (kostenfrei)

URL: Volltext  (kostenfrei)

URL: Volltext  (kostenfrei)

URL: Volltext  (kostenfrei)

URL: kostenfrei

URL: OAPEN

URL: OAPEN

URL: OAPEN

URL: ProQuest Ebook Central

URL: SpringerLink

URL: SpringerLink

URL: SpringerLink

URL: EBSCOhost

URL: lizenzpflichtig

UID:

Format: 330 S.

Language: English

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

Keywords: Formale Sprache ; Programmiersprache ; ALGOL 60 ; Konferenzschrift ; Konferenzschrift ; Konferenzschrift

UID:

Format: 330 S.

Edition: 2. print.

Note: Literaturverz. S. 300 - 330

Language: English

Keywords: ALGOL 60 ; Formale Sprache ; Konferenzschrift ; Konferenzschrift ; Konferenzschrift

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 (597 pages)

Edition: 1st ed.

ISBN: 9783031656330

Series Statement: Lecture Notes in Computer Science Series ; v.14683

Note: Intro -- Preface -- Organization -- Invited Talks -- How to Solve Math Problems Without Talent -- Bridging Formal Mathematics and Software Verification -- The Art of SMT Solving -- Contents - Part III -- Synthesis and Repair -- Syntax-Guided Automated Program Repair for Hyperproperties -- 1 Introduction -- 2 Preliminaries -- 3 Program Repair by Symbolic Execution -- 3.1 Symbolic Execution -- 3.2 Symbolic Paths and Safety Automata -- 3.3 Encoding for HyperLTL -- 3.4 Program Repair Using SyGuS -- 4 Transparent Repair -- 4.1 Transparency -- 4.2 Encoding for Transparent Repair -- 5 Iterative Repair -- 5.1 Encoding for Iterative Repair -- 5.2 Iterative Repair Loop -- 6 Implementation and Evaluation -- 6.1 Iterative Repair for Hyperproperties -- 6.2 Scalability in Solution Size -- 6.3 Evaluation on k-Safety Instances -- 6.4 Evaluation on Functional Properties -- 7 Related Work -- 8 Conclusion -- References -- The SemGuS Toolkit -- 1 Introduction -- 2 The SemGuS Format 1.0 -- 3 A Baseline SemGuS Solver -- 3.1 Verifying Candidate Solutions -- 3.2 Baseline Enumerative Solvers -- 3.3 Extensibility -- 4 Benchmarks and Performance of Baseline Solvers -- 5 Related Work -- References -- Relational Synthesis of Recursive Programs via Constraint Annotated Tree Automata -- 1 Introduction -- 2 Motivating Example -- 3 Preliminaries -- 4 Constraint Annotated Tree Automata -- 4.1 CATA Operations for Synthesis -- 5 Synthesis Algorithm -- 5.1 Problem Statement -- 5.2 Basic Synthesis Algorithm -- 5.3 Lazy Synthesis Algorithm -- 6 Implementation -- 7 Evaluation -- 8 Related Work -- 9 Conclusion -- References -- Information Flow Guided Synthesis with Unbounded Communication -- 1 Introduction -- 2 Running Example: Sequence Transmission -- 3 Preliminaries -- 4 Prefix Information Flow -- 5 Unbounded Communication in Distributed Systems -- 5.1 Receiving Information. , 5.2 Transmitting Information -- 5.3 Safety Hyper Implementations -- 6 Synthesis with Prefix Information Flow Assumptions -- 6.1 Automata for Assume and Guarantee Specifications -- 6.2 Compositional Synthesis -- 7 Experiments -- 8 Related Work -- 9 Conclusion -- References -- Synthesis of Temporal Causality -- 1 Introduction -- 1.1 Temporal Causality -- 1.2 Contributions and Structure -- 2 Preliminaries -- 3 Overview: The Topology of Causality -- 3.1 Actual Causes as Downward Closed Sets of Traces -- 3.2 Causality Without the Limit Assumption -- 4 Generalized Temporal Causality -- 4.1 Similarity Relations and the Limit Assumption -- 4.2 A General Definition of Temporal Causality -- 4.3 Proving Generalization -- 5 Cause Synthesis -- 5.1 Proving Our Characterization -- 5.2 Cause-Synthesis Algorithm for -Regular Effects -- 6 Implementation and Evaluation -- 6.1 Cause Synthesis -- 6.2 Cause Checking -- 7 Related Work -- 8 Conclusion -- References -- Dynamic Programming for Symbolic Boolean Realizability and Synthesis -- 1 Introduction -- 2 Preliminary Definitions -- 2.1 Boolean Formula and Synthesis Concepts -- 2.2 Dynamic Programming Concepts - Project-Join Trees -- 3 Realizability CheckingProofs for All Lemmas and Theorems Can Be Found in the Appendix A. -- 3.1 Theoretical Basis and Valuations in Trees -- 3.2 Determining Nullary, Partial and Full Realizability -- 4 Synthesis of Witness Functions -- 4.1 Monolithic Approach -- 4.2 Synthesis Using Graded Project-Join Trees -- 5 Experimental Evaluation -- 5.1 Realizability-Checking Phase -- 5.2 Synthesis -- 5.3 Tree Widths and Realizability -- 5.4 Comparison with Non-BDD-Based Synthesis -- 6 Concluding Remarks -- References -- Localized Attractor Computations for Infinite-State Games -- 1 Introduction -- 2 Preliminaries -- 3 Attractor Computation with Caching -- 4 Abstract Template-Based Cache Generation. , 4.1 Generating Attractor Caches from Sub-Games -- 4.2 Constructing Sub-games from Abstract Strategy Templates -- 5 Game Solving with Abstract Template-Based Caching -- 6 Experimental Evaluation -- 7 Related Work -- 8 Conclusion -- References -- Learning -- Bisimulation Learning -- 1 Introduction -- 2 Illustrative Example -- 3 Stutter-Insensitive Bisimulations of Deterministic Transition Systems -- 3.1 Model Checking -- 4 Counterexample-Guided Bisimulation Learning -- 4.1 Learner-Verifier Framework for Bisimulation Learning -- 4.2 Binary Decision Tree Partition Templates -- 5 Experimental Evaluation -- 5.1 Discrete-Time Clock Synchronization -- 5.2 Conditional Termination -- 6 Conclusion -- References -- Regular Reinforcement Learning -- 1 Introduction -- 2 Related Work -- 3 Preliminaries -- 3.1 Regular Languages -- 3.2 Rational Transductions -- 3.3 Markov Decision Processes -- 4 Regular Markov Decision Processes -- 4.1 Undecidability of Values -- 4.2 Discounted Optimization -- 4.3 Finiteness Conditions -- 4.4 Q-Learning in RMDPs -- 5 Deep Regular Reinforcement Learning -- 5.1 Token Passing -- 5.2 Duplicating Pebbles -- 5.3 Shunting Yard Algorithm -- 5.4 Modified Tangrams -- 6 Conclusion -- References -- LTL Learning on GPUs -- 1 Introduction -- 2 Formal Preliminaries -- 3 High-Level Structure of the Algorithm -- 4 In-Memory Representation of Search Space -- 5 Correctness and Complexity of the Branch-Free Implementation of Temporal Operators -- 6 Relaxed Uniqueness Checks -- 7 Divide & -- Conquer -- 8 Evaluation of Algorithm Performance -- 9 Conclusion -- References -- Safe Exploration in Reinforcement Learning by Reachability Analysis over Learned Models -- 1 Introduction -- 2 Problem Setup -- 3 Verified Exploration Through Learned Models -- 3.1 Symbolic Environment Models -- 3.2 Shielding for Verified Safe Exploration. , 3.3 Neural Controller Approximation -- 4 Experiments -- 5 Related Work -- 6 Conclusion -- References -- Cyberphysical and Hybrid Systems -- Using Four-Valued Signal Temporal Logic for Incremental Verification of Hybrid Systems -- 1 Introduction -- 1.1 Related Work -- 1.2 Contributions -- 2 Preliminaries and Problem Statement -- 2.1 Intervals -- 2.2 Truth Values -- 2.3 Signals -- 2.4 Reachability Analysis of Hybrid Systems -- 2.5 Signal Temporal Logic with Boolean Semantics -- 2.6 Problem Statement -- 3 Basic Idea and Solution Concept -- 4 Four-Valued Signal Temporal Logic -- 4.1 Computing Boolean Satisfaction Signals -- 4.2 Computing Three-Valued Satisfaction Signals -- 4.3 Computing Four-Valued Satisfaction Signals -- 5 Incremental Verification of Hybrid Systems -- 5.1 Incremental Verification Algorithm -- 5.2 Refinement via Branching the Reachability Analysis -- 6 Evaluation -- 6.1 Bouncing Ball -- 6.2 Autonomous Driving -- 6.3 Genetic Oscillator -- 7 Conclusion -- References -- Optimization-Based Model Checking and Trace Synthesis for Complex STL Specifications -- 1 Introduction -- 2 Preliminaries -- 2.1 Signal Temporal Logic -- 2.2 Finite Variability -- 3 Problem Formulation -- 4 Variable-Interval Encoding of STL to MILP -- 4.1 -Stable Partitions -- 4.2 Variable-Interval MILP Encoding -- 5 System Models and Their MILP Encoding -- 5.1 HAs with Closed-Form Solutions -- 5.2 HAs with Double Integrator Dynamics -- 6 Implementation and Experiments -- References -- Inner-Approximate Reachability Computation via Zonotopic Boundary Analysis -- 1 Introduction -- 2 Preliminaries -- 2.1 Notation -- 2.2 Problem Statement -- 3 Methodology -- 3.1 Inner-Approximation Computation Framework -- 3.2 Extraction of Zonotopes' Boundaries -- 3.3 Zonotopal Tiling and Boundary Refinement -- 3.4 Contracting Computed Outer-Approximation -- 4 Experiments. , 4.1 Advantage in Efficiency and Precision -- 4.2 Advantage in Long Time Horizons -- 4.3 Advantage in Big Initial Sets -- 5 Conclusion -- References -- Scenario-Based Flexible Modeling and Scalable Falsification for Reconfigurable CPSs -- 1 Introduction -- 2 Background -- 2.1 Preliminaries -- 2.2 Motivating Example: A Multi-UAV System -- 3 Scenario-Based Formalism for Reconfigurable Systems -- 3.1 Scenario-Based System Modeling -- 3.2 Specifying System Requirements in Topology-Aware STL -- 4 Path-Oriented Optimization-Based System Falsification -- 4.1 Falsification Framework -- 4.2 Path Generation for Hierarchical Scenario Tasks -- 4.3 Optimization-Based Falsification for Paths -- 5 Implementation and Evaluation -- 5.1 Implementation and Research Questions -- 5.2 Experimental Evaluation and Analysis -- 5.3 Threats to Validity -- 6 Related Work -- 7 Conclusion and Future Work -- References -- Probabilistic Systems -- Playing Games with Your PET: Extending the Partial Exploration Tool to Stochastic Games -- 1 Introduction -- 2 Preliminaries -- 3 Complete-Exploration Algorithm for Solving SGs -- 4 Partial-Exploration Algorithm for Solving SGs -- 5 Tool Description -- 6 Experimental Evaluation -- 6.1 Experimental Setup -- 6.2 Results -- 7 Conclusion -- References -- What Should Be Observed for Optimal Reward in POMDPs? -- 1 Introduction -- 2 Preliminaries -- 2.1 Markov Decision Processes (MDPs) -- 2.2 Partially Observable Markov Decision Processes -- 3 The Optimal Observability Problem -- 3.1 Problem Statement -- 3.2 Undecidability -- 4 Optimal Observability for Positional Strategies -- 4.1 Positional and Deterministic Strategies -- 4.2 Positional Randomized Strategies -- 5 Implementation and Experimental Evaluation -- 5.1 Solving Optimal Observability Problems with Parameter Synthesis Tools -- 5.2 Implementation and Setup -- 5.3 Experimental Results. , 6 Conclusion and Future Work.

Additional Edition: Print version: Gurfinkel, Arie Computer Aided Verification Cham : Springer International Publishing AG,c2024 ISBN 9783031656323

Language: English

Keywords: Electronic books.

URL: Click to View

UID:

Format: 1 online resource (597 pages)

Edition: 1st ed. 2024.

ISBN: 3-031-65633-4

Series Statement: Lecture Notes in Computer Science, 14683

Content: This open access 3-volume set constitutes the proceedings of the 36th International Conference on Computer-Aided Verification, CAV 2024, which took place in Montreal, Canada, during July 24–27, 2024. The primary focus of CAV is to extend the frontiers of verification techniques by expanding to new domains such as security, quantum computing, and machine learning.

Note: Intro -- Preface -- Organization -- Invited Talks -- How to Solve Math Problems Without Talent -- Bridging Formal Mathematics and Software Verification -- The Art of SMT Solving -- Contents - Part III -- Synthesis and Repair -- Syntax-Guided Automated Program Repair for Hyperproperties -- 1 Introduction -- 2 Preliminaries -- 3 Program Repair by Symbolic Execution -- 3.1 Symbolic Execution -- 3.2 Symbolic Paths and Safety Automata -- 3.3 Encoding for HyperLTL -- 3.4 Program Repair Using SyGuS -- 4 Transparent Repair -- 4.1 Transparency -- 4.2 Encoding for Transparent Repair -- 5 Iterative Repair -- 5.1 Encoding for Iterative Repair -- 5.2 Iterative Repair Loop -- 6 Implementation and Evaluation -- 6.1 Iterative Repair for Hyperproperties -- 6.2 Scalability in Solution Size -- 6.3 Evaluation on k-Safety Instances -- 6.4 Evaluation on Functional Properties -- 7 Related Work -- 8 Conclusion -- References -- The SemGuS Toolkit -- 1 Introduction -- 2 The SemGuS Format 1.0 -- 3 A Baseline SemGuS Solver -- 3.1 Verifying Candidate Solutions -- 3.2 Baseline Enumerative Solvers -- 3.3 Extensibility -- 4 Benchmarks and Performance of Baseline Solvers -- 5 Related Work -- References -- Relational Synthesis of Recursive Programs via Constraint Annotated Tree Automata -- 1 Introduction -- 2 Motivating Example -- 3 Preliminaries -- 4 Constraint Annotated Tree Automata -- 4.1 CATA Operations for Synthesis -- 5 Synthesis Algorithm -- 5.1 Problem Statement -- 5.2 Basic Synthesis Algorithm -- 5.3 Lazy Synthesis Algorithm -- 6 Implementation -- 7 Evaluation -- 8 Related Work -- 9 Conclusion -- References -- Information Flow Guided Synthesis with Unbounded Communication -- 1 Introduction -- 2 Running Example: Sequence Transmission -- 3 Preliminaries -- 4 Prefix Information Flow -- 5 Unbounded Communication in Distributed Systems -- 5.1 Receiving Information. , 5.2 Transmitting Information -- 5.3 Safety Hyper Implementations -- 6 Synthesis with Prefix Information Flow Assumptions -- 6.1 Automata for Assume and Guarantee Specifications -- 6.2 Compositional Synthesis -- 7 Experiments -- 8 Related Work -- 9 Conclusion -- References -- Synthesis of Temporal Causality -- 1 Introduction -- 1.1 Temporal Causality -- 1.2 Contributions and Structure -- 2 Preliminaries -- 3 Overview: The Topology of Causality -- 3.1 Actual Causes as Downward Closed Sets of Traces -- 3.2 Causality Without the Limit Assumption -- 4 Generalized Temporal Causality -- 4.1 Similarity Relations and the Limit Assumption -- 4.2 A General Definition of Temporal Causality -- 4.3 Proving Generalization -- 5 Cause Synthesis -- 5.1 Proving Our Characterization -- 5.2 Cause-Synthesis Algorithm for -Regular Effects -- 6 Implementation and Evaluation -- 6.1 Cause Synthesis -- 6.2 Cause Checking -- 7 Related Work -- 8 Conclusion -- References -- Dynamic Programming for Symbolic Boolean Realizability and Synthesis -- 1 Introduction -- 2 Preliminary Definitions -- 2.1 Boolean Formula and Synthesis Concepts -- 2.2 Dynamic Programming Concepts - Project-Join Trees -- 3 Realizability CheckingProofs for All Lemmas and Theorems Can Be Found in the Appendix A. -- 3.1 Theoretical Basis and Valuations in Trees -- 3.2 Determining Nullary, Partial and Full Realizability -- 4 Synthesis of Witness Functions -- 4.1 Monolithic Approach -- 4.2 Synthesis Using Graded Project-Join Trees -- 5 Experimental Evaluation -- 5.1 Realizability-Checking Phase -- 5.2 Synthesis -- 5.3 Tree Widths and Realizability -- 5.4 Comparison with Non-BDD-Based Synthesis -- 6 Concluding Remarks -- References -- Localized Attractor Computations for Infinite-State Games -- 1 Introduction -- 2 Preliminaries -- 3 Attractor Computation with Caching -- 4 Abstract Template-Based Cache Generation. , 4.1 Generating Attractor Caches from Sub-Games -- 4.2 Constructing Sub-games from Abstract Strategy Templates -- 5 Game Solving with Abstract Template-Based Caching -- 6 Experimental Evaluation -- 7 Related Work -- 8 Conclusion -- References -- Learning -- Bisimulation Learning -- 1 Introduction -- 2 Illustrative Example -- 3 Stutter-Insensitive Bisimulations of Deterministic Transition Systems -- 3.1 Model Checking -- 4 Counterexample-Guided Bisimulation Learning -- 4.1 Learner-Verifier Framework for Bisimulation Learning -- 4.2 Binary Decision Tree Partition Templates -- 5 Experimental Evaluation -- 5.1 Discrete-Time Clock Synchronization -- 5.2 Conditional Termination -- 6 Conclusion -- References -- Regular Reinforcement Learning -- 1 Introduction -- 2 Related Work -- 3 Preliminaries -- 3.1 Regular Languages -- 3.2 Rational Transductions -- 3.3 Markov Decision Processes -- 4 Regular Markov Decision Processes -- 4.1 Undecidability of Values -- 4.2 Discounted Optimization -- 4.3 Finiteness Conditions -- 4.4 Q-Learning in RMDPs -- 5 Deep Regular Reinforcement Learning -- 5.1 Token Passing -- 5.2 Duplicating Pebbles -- 5.3 Shunting Yard Algorithm -- 5.4 Modified Tangrams -- 6 Conclusion -- References -- LTL Learning on GPUs -- 1 Introduction -- 2 Formal Preliminaries -- 3 High-Level Structure of the Algorithm -- 4 In-Memory Representation of Search Space -- 5 Correctness and Complexity of the Branch-Free Implementation of Temporal Operators -- 6 Relaxed Uniqueness Checks -- 7 Divide & -- Conquer -- 8 Evaluation of Algorithm Performance -- 9 Conclusion -- References -- Safe Exploration in Reinforcement Learning by Reachability Analysis over Learned Models -- 1 Introduction -- 2 Problem Setup -- 3 Verified Exploration Through Learned Models -- 3.1 Symbolic Environment Models -- 3.2 Shielding for Verified Safe Exploration. , 3.3 Neural Controller Approximation -- 4 Experiments -- 5 Related Work -- 6 Conclusion -- References -- Cyberphysical and Hybrid Systems -- Using Four-Valued Signal Temporal Logic for Incremental Verification of Hybrid Systems -- 1 Introduction -- 1.1 Related Work -- 1.2 Contributions -- 2 Preliminaries and Problem Statement -- 2.1 Intervals -- 2.2 Truth Values -- 2.3 Signals -- 2.4 Reachability Analysis of Hybrid Systems -- 2.5 Signal Temporal Logic with Boolean Semantics -- 2.6 Problem Statement -- 3 Basic Idea and Solution Concept -- 4 Four-Valued Signal Temporal Logic -- 4.1 Computing Boolean Satisfaction Signals -- 4.2 Computing Three-Valued Satisfaction Signals -- 4.3 Computing Four-Valued Satisfaction Signals -- 5 Incremental Verification of Hybrid Systems -- 5.1 Incremental Verification Algorithm -- 5.2 Refinement via Branching the Reachability Analysis -- 6 Evaluation -- 6.1 Bouncing Ball -- 6.2 Autonomous Driving -- 6.3 Genetic Oscillator -- 7 Conclusion -- References -- Optimization-Based Model Checking and Trace Synthesis for Complex STL Specifications -- 1 Introduction -- 2 Preliminaries -- 2.1 Signal Temporal Logic -- 2.2 Finite Variability -- 3 Problem Formulation -- 4 Variable-Interval Encoding of STL to MILP -- 4.1 -Stable Partitions -- 4.2 Variable-Interval MILP Encoding -- 5 System Models and Their MILP Encoding -- 5.1 HAs with Closed-Form Solutions -- 5.2 HAs with Double Integrator Dynamics -- 6 Implementation and Experiments -- References -- Inner-Approximate Reachability Computation via Zonotopic Boundary Analysis -- 1 Introduction -- 2 Preliminaries -- 2.1 Notation -- 2.2 Problem Statement -- 3 Methodology -- 3.1 Inner-Approximation Computation Framework -- 3.2 Extraction of Zonotopes' Boundaries -- 3.3 Zonotopal Tiling and Boundary Refinement -- 3.4 Contracting Computed Outer-Approximation -- 4 Experiments. , 4.1 Advantage in Efficiency and Precision -- 4.2 Advantage in Long Time Horizons -- 4.3 Advantage in Big Initial Sets -- 5 Conclusion -- References -- Scenario-Based Flexible Modeling and Scalable Falsification for Reconfigurable CPSs -- 1 Introduction -- 2 Background -- 2.1 Preliminaries -- 2.2 Motivating Example: A Multi-UAV System -- 3 Scenario-Based Formalism for Reconfigurable Systems -- 3.1 Scenario-Based System Modeling -- 3.2 Specifying System Requirements in Topology-Aware STL -- 4 Path-Oriented Optimization-Based System Falsification -- 4.1 Falsification Framework -- 4.2 Path Generation for Hierarchical Scenario Tasks -- 4.3 Optimization-Based Falsification for Paths -- 5 Implementation and Evaluation -- 5.1 Implementation and Research Questions -- 5.2 Experimental Evaluation and Analysis -- 5.3 Threats to Validity -- 6 Related Work -- 7 Conclusion and Future Work -- References -- Probabilistic Systems -- Playing Games with Your PET: Extending the Partial Exploration Tool to Stochastic Games -- 1 Introduction -- 2 Preliminaries -- 3 Complete-Exploration Algorithm for Solving SGs -- 4 Partial-Exploration Algorithm for Solving SGs -- 5 Tool Description -- 6 Experimental Evaluation -- 6.1 Experimental Setup -- 6.2 Results -- 7 Conclusion -- References -- What Should Be Observed for Optimal Reward in POMDPs? -- 1 Introduction -- 2 Preliminaries -- 2.1 Markov Decision Processes (MDPs) -- 2.2 Partially Observable Markov Decision Processes -- 3 The Optimal Observability Problem -- 3.1 Problem Statement -- 3.2 Undecidability -- 4 Optimal Observability for Positional Strategies -- 4.1 Positional and Deterministic Strategies -- 4.2 Positional Randomized Strategies -- 5 Implementation and Experimental Evaluation -- 5.1 Solving Optimal Observability Problems with Parameter Synthesis Tools -- 5.2 Implementation and Setup -- 5.3 Experimental Results. , 6 Conclusion and Future Work.

Additional Edition: ISBN 3-031-65632-6

Language: English

DOI: 10.1007/978-3-031-65633-0

UID:

Format: 1 online resource (1045 p.)

ISBN: 1-281-77901-6 , 9786611779016 , 0-08-088718-X

Series Statement: Studies in logic and the foundations of mathematics, v. 133

Content: The present volume contains a considered choice of the existing literature on Automath. Many of the papers included in the book have been published in journals or conference proceedings, but a number have only circulated as research reports or have remained unpublished. The aim of the editors is to present a representative selection of existing articles and reports and of material contained in dissertations, giving a compact and more or less complete overview of the work that has been done in the Automath research field, from the beginning to the present day. Six different areas have been dist

Note: Description based upon print version of record. , Front Cover; Selected Papers on Authomath; Copyright Page; Preface; Contents; Hints for the reader; Notation; Introduction; Twenty-five years of Automath research; Part A: Motivation and exposition; Chapter A.1. Verification of mathematical proofs by a computer; Chapter A.2. The mathematical language Automath, its usage, and some of its extensions; Chapter A.3. A description of Automath and some aspects of its language theory; Chapter A.4. Formalization of classical mathematics in Automath; Chapter A.5. A survey of the project Automath; Chapter A.6. The language theory of Automath , Chapter A.7. Reflections on AutomathChapter A.8. Type systems - basic ideas and applications; Part B: Language deflnition and special subjects; Chapter B.1. Description of AUT-68; Chapter B.2. AUT-SL, a single line version of Automath; Chapter B.3. Some extensions of Automath: the AUT-4 family; Chapter B.4. AUT-QE without type inclusion; Chapter B.5. Checking Landau's ''Grundlagen" in the Automath system; Chapter B.6. The language theory of Automath; Chapter B.7. Generalizing Automath by means of a lambda- typed lambda calculus; Chapter B.8. Lambda calculus extended with segments , Part C: TheoryChapter C.1. A normal form theorem in a λ-calculus with types; Chapter C.2. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application t o the Church-Rosser theorem; Chapter C.3. Strong normalization in a typed lambda calculus with lambda structured types; Chapter C.4. Big trees in λ-calculus with λ-expressions as types; Chapter C.5. The language theory of Automath; Chapter C.6. The language theory of A infinty, a typed λ-calculus where terms are types; PART D: Text examples; Chapter D.1. Example of a text written in Automath , Chapter D.2. Checking Landau's "Grundlagen" in the Automath systemChapter D.3. Checking Landau's "Grundlagen" in the Automath system; Chapter D.4. A text fragment from Zucker's "Real Analysis"; Chapter D.5. Checking Landau's "Grundlagen" in the Automath system; PART E: Verification; Chapter E.1. A verifying program for Automath; Chapter E.2. Checking Landau's "Grundlagen'' in the Automath system.; Chapter E.3. An implementation of substitution in λ-calculus with dependent types; PART F: Related topics; Chapter F.1. Set theory with type restrictions , Chapter F.2. Formalisation of constructivity in AuthomathChapter F.3. The Mathematical Vernacular, a language for mathematics with typed sets; Chapter F.4. Relational semantics in an integrated system; Chapter F.5. Computer program semantics in space and time; Bibliography; References; Indexes; Index of Names; Index of Notations; Index of Subjects , English

Additional Edition: ISBN 0-444-89822-0

Language: English

UID:

Format: Online-Ressource

ISBN: 9812389709 , 9789812389701

Series Statement: EBSCOhost eBook Collection

Content: This is the first handbook to cover comprehensively both software engineering and knowledge engineering - two important fields that have become interwoven in recent years. Over 60 international experts have contributed to the book. Each chapter has been written in such a way that a practitioner of software engineering and knowledge engineering can easily understand and obtain useful information. Each chapter covers one topic and can be read independently of other chapters, providing both a general survey of the topic and an in-depth exposition of the state of the art

Note: Includes bibliographical references and index , PREFACE; CONTENTS; MULTIMEDIA SOFTWARE ENGINEERING; OBJECT-ORIENTED MODELING OF MULTIMEDIA APPLICATIONS; EXPLOITING VISUAL LANGUAGES IN SOFTWARE ENGINEERING; SOFTWARE ENGINEERING FOR VISUAL PROGRAMMING LANGUAGES; EVALUATION ISSUES FOR VISUAL PROGRAMMING LANGUAGES; VISUAL PARALLEL PROGRAMMING; SYSTEM AND SOFTWARE VISUALISATION; SITUATED COMPUTING: A PARADIGM TO ENHANCE THE MOBILE USER'S INTERACTION; WEB ENGINEERING: MODELS AND METHODOLOGIES FOR THE DESIGN OF HYPERMEDIA APPLICATIONS; VISUALIZATION OF KNOWLEDGE STRUCTURES; FORMAL DESCRIPTION TECHNIQUES , SOFTWARE SPECIFICATION & DESIGN METHODS AND METHOD ENGINEERINGCOMPONENT-BASED SOFTWARE ENGINEERING; SOFTWARE COST ESTIMATION; DATA MODEL METRICS; HOW MANY TESTS ARE ENOUGH?; VERIFICATION AND VALIDATION; UNCERTAINTY MANAGEMENT; SOFTWARE PROJECT MANAGEMENT; REVERSE ENGINEERING; SYNCHRONIZING INTERACTIVE WEB DOCUMENTS WITH FD-JAVA CONSTRAINTS; VERSIONS OF PROGRAM INTEGRATION; A SURVEY OF SOFTWARE INSPECTION TECHNOLOGIES; SE/KE REUSE RESEARCH: COMMON THEMES AND EMPIRICAL RESULTS; SUPPORTING SOFTWARE PROCESSES USING KNOWLEDGE MANAGEMENT; KNOWLEDGE ELICITATION: THE STATE OF THE ART , NONMONOTONIC REASONING AND CONSISTENCY MANAGEMENT IN SOFTWARE ENGINEERINGSOFTWARE PATTERNS; APPLICATION OF KNOWLEDGE-BASED SYSTEMS FOR SUPERVISION AND CONTROL OF MACHINING PROCESSES; NEW PARADIGM FOR DEVELOPING EVOLUTIONARY SOFTWARE TO SUPPORT E-BUSINESS; A SURVEY OF SYSTEM-LEVEL DESIGN NOTATIONS FOR EMBEDDED SYSTEMS; AGENT-ORIENTED SOFTWARE CONSTRUCTION WITH UML; IMPROVING UML DESIGNS USING AUTOMATIC DESIGN PATTERN DETECTION; INDEX

Additional Edition: ISBN 9810249748

Language: English

Keywords: Softwareentwicklung ; Wissensverarbeitung ; Softwareentwicklung ; Wissensverarbeitung ; Electronic books. ; Electronic books

URL: Volltext  (Deutschlandweit zugänglich)

URL: Inhaltstext

Author information: Zhang, Xiguo 1944-

UID:

Format: XIV, 272 p. 47 illus. , online resource.

ISBN: 9783642396663

Series Statement: Lecture Notes in Computer Science, 7994

Content: This book constitutes the refereed proceedings of the 7th International Conference on Web Reasoning and Rule Systems, RR 2013, held in Manheim, Germany in July 2013. The 19 revised research papers and 4 technical communications presented together with 2 invited talks and 1 tutorial talk were carefully reviewed and selected from 34 submissions. The scope of conference is decision making, planning, and intelligent agents, reasoning, machine learning, knowledge extraction and IR technologies, large-scale data management and reasoning on the web of data, data integration, dataspaces and ontology-based data access, non-standard reasoning, algorithms for distributed, parallelized, and scalable reasoning, and system descriptions and experimentation.

Note: Invited Talks -- Inconsistency Management for Description Logic Programs and Beyond -- Reasoning About Pattern-Based XML Queries -- Answer Set Programming: Language, Applications and Development Tools -- Full Papers -- A Variant of Earley Deduction with Partial Evaluation -- Verification and Synthesis in Description Logic Based Dynamic Systems -- Towards an Efficient Algorithm to Reason over Description Logics -- Extended with Nominal Schemas -- Computing Incoherence Explanations for Learned Ontologies -- An Ontology-Based Reasoning Approach for Electric Power Utilities -- Conjunctive Queries with Negation over DL-Lite: A Closer Look -- On the Exploration of the Query Rewriting Space with Existential Rules -- Incomplete Information in RDF -- RIO: Minimizing User Interaction in Ontology Debugging -- Eliminating Nonmonotonic DL-Atoms in Description Logic Programs -- BUNDLE: A Reasoner for Probabilistic Ontologies -- Technical Communications -- Detection of Inconsistencies in Rules Due to Changes in Ontologies: Let’s Get Formal -- Rule Revision in Normal DL Logic Programs -- OBDA and Intermodal Logistics: Active Projects and Applications -- Semantic Pervasive Advertising -- Semantics for Mapping Relations in SKOS -- From OWL to DL-Lite through Efficient Ontology Approximation -- PQMPMS: A Preference-enabled Querying Mechanism for Personalized Mobile Search -- An Analyzer of Existential Rule Bases -- Stream Rule: A Nonmonotonic Stream Reasoning System for the Semantic Web.-An Integrated Environment for Reasoning over Ontologies via Logic Programming -- Horn-DL: An Expressive Horn Description Logic with PTime Data Complexity -- Parameter Learning for Probabilistic Ontologies.

In: Springer eBooks

Additional Edition: Printed edition: ISBN 9783642396656

Language: English

Subjects: Computer Science

Keywords: Konferenzschrift ; Konferenzschrift ; Konferenzschrift

DOI: 10.1007/978-3-642-39666-3

URL: http://dx.doi.org/10.1007/978-3-642-39666-3

URL: Volltext

URL: Inhaltsverzeichnis

URL: Abstract

URL: Volltext  (lizenzpflichtig)

URL: Volltext  (lizenzpflichtig)

URL: Cover

URL: Inhaltstext

UID:

Format: XVIII, 718 p. 271 illus. , online resource.

ISBN: 9783642334696

Series Statement: Lecture Notes in Computer Science, 7529

Content: The volume LNCS 7529 constitutes the refereed proceedings of the International Conference on Web Information Systems and Mining, WISM 2012, held in Chengdu, China, in October 2012. The 87 revised full papers presented were carefully reviewed and selected from 418 submissions. The papers are organized in topical sections on applications of Web information systems; applications of Web mining; e-government and e-commerce; information security; intelligent networked systems; management information systems; mobile computing; semantic Web and ontologies; Web information extraction; Web intelligence; Web interfaces and applications; and XML and semi-structured data.

Note: Study on the Design of Automatic Cotton Bale Inspecting Management System -- The Smallest Randi´c Index for Trees -- Design of Meridian and Acupoints Compatibility Analysis System -- Invariant Subspaces for Operators with Thick Spectra -- Voronoi Feature Selection Model Considering Variable-Scale Map’s Balance and Legibility -- A Code Dissemination Protocol of Low Energy Consumption -- Dynamic Spectrum Analysis of High-Speed Train Passenger Compartment Luggage Rack Noise -- Port-Based Composable Modeling and Simulation for Safety Critical System Testbed -- Risk Assessment Method of Radio Block Center in Fuzzy Uncertain Environment -- Learning Research in Knowledge Transfer -- A Post-filtering Technique for Enhancing Acoustic Echo Cancelation System -- Packet Dropping Schemes and Quality Evaluation for H.264 Videos at High Packet Loss Rates -- A Blocked Statistics Method Based on Directional Derivative -- Study on Cooperative Game Model of Talent Training through School-Enterprise Coalition -- Research on Internet Public Opinion Detection System Based on Domain Ontology -- A Security Analysis Model Based on Artificial Neural Network -- Social Network Analyses on Knowledge Diffusion of China’s Management Science -- A Parallel Association-Rule Mining Algorithm -- An Algorithm of Parallel Programming Design Based on Problem Domain Model -- Metadata-Aware Small Files Storage Architecture on Hadoop -- Research on the Isomorphism of the Electronic-Government and Electronic-Commerce in Support System -- On the Deployment of Wireless Sensor Networks with Regular Topology Patterns -- An Empirical Study on the Relationship among Trust and the Risky and Non-Risky Components of E-Commerce -- Process Modeling and Reengineering in the Integration Stage of Electronic Government -- Development of Vertical Industrial B2B in China: Based on Cases Study -- Personalized Recommendation System on Massive Content Processing Using Improved MFNN -- A Speaker Recognition Based Approach for Identifying Voice Spammer -- Security Access Authentication System for IPv4/IPv6 Dual-Stack Campus Network Based on IpoE -- Information Encryption Based on Virtual Optical Imaging System and Chen’s Chaos -- A New Scheme with Secure Cookie against SSLStrip Attack -- ID-Based Signatures from Lattices in the Random Oracle Model -- Strongly Secure Attribute-Based Authenticated Key Exchange with Traceability -- A New Public Key Signature Scheme Based on Multivariate Polynomials -- Comments on an Advanced Dynamic ID-Based Authentication Scheme for Cloud Computing -- Research on Security Management in Active Network Node Operating Systems -- An Integrity Verification Scheme for Multiple Replicas in Clouds -- Multi-stage Attack Detection Algorithm Based on Hidden Markov Model -- Security Analysis of a Secure and Practical Dynamic Identity-Based Remote User Authentication Scheme -- Formal Construction of Secure Information Transmission in Office Automation System -- A Novel CBCD Scheme Based on Local Features Category -- Research and Improvement on Association Rule Algorithm Based on FP-Growth -- Encrypted Remote User Authentication Scheme by Using Smart Card -- A Web Visualization System of Cyberinfrastructure Resources -- A Novel Clustering Mechanism Based on Image-Oriented Correlation Coefficient for Wireless Multimedia Sensor Networks -- Design of Underground Miner Positioning System Based on ZigBee Technology -- Metadata Management of Context Resources in Context-Aware Middleware System -- Research on Scientific Data Sharing Platform of Hydrology and Water Resources Based on Service Composition -- Study on the Scheme of Tianjin Area E-commerce Platform Construction -- Research on Chinese Hydrological Data Quality Management -- Using IoT Technologies to Resolve the Food Safety Problem – An Analysis Based on Chinese Food Standards -- Towards Better Cross-Cloud Data Integration: Using P2P and ETL Together -- Design of Intelligent Maintenance Decision-Making System for Fixed Equipment in Petrochemical Plants -- Dimensional Modeling for Landslide Monitoring Data Warehouse -- A New Fuzzy Risk Evaluation Method for Uncertain Network Public Sentiment Emergency -- Service Lifecycle Management in Distributed JBI Environment -- Graded BDI Models for Agent Architectures Based on _Lukasiewicz Logic and Propositional Dynamic Logic -- Energy Model of SARA and Its Performance Analysis -- Data Profiling for Semantic Web Data -- Checking and Handling Inconsistency of DBpedia -- Conceptual Representing of Documents and Query Expansion Based on Ontology -- Robust Web Data Extraction: A Novel Approach Based on Minimum Cost Script Edit Model -- Rule-Based Text Mining of Chinese Herbal Medicines with Patterns in Traditional Chinese Medicine for Chronic Obstructive Pulmonary Disease -- Fault Forecast of Electronic Equipment Based on ε – SVR -- Analysis and Design of Internet Monitoring System on Public Opinion Based on Cloud Computing and NLP -- Using Similes to Extract Basic Sentiments across Languages -- Automatic Summarization for Chinese Text Using Affinity Propagation Clustering and Latent Semantic Analysis -- A Webpage Deletion Algorithm Based on Hierarchical Filtering -- Research in Keyword Extraction -- Tuple Refinement Method Based on Relationship Keyword Extension -- An Agent Based Intelligent Meta Search Engine -- A Novel Image Annotation Feedback Model Based on Internet-Search -- The Design and Application of an Ancient Porcelain Online Identification Analysis System --  Web Crawler in In-Site Search -- A Novel Shark-Search Algorithm for Theme Crawler -- A Framework of Online Proxy-Based Web Prefetching -- Mapping the Intellectual Structure by Co-word: A Case of International Management Science -- Study on Multi-sensor Information Fusion Technology in the Dynamic Monitoring of Coal Mine Roof -- Detecting Hot Topics in Chinese Microblog Streams Based on Frequent Patterns Mining -- KACTL: Knowware Based Automated Construction of a Treelike Library from Web Documents -- Associating Labels and Elements of Deep Web Query Interface Based on DOM -- Design and Implementation of the Online Shopping System -- System Development of Residence Property Management Based on WEB -- An Intelligent Metadata Extraction Approach Based on Programming by Demonstration -- OF-NEDL: An OpenFlow Networking Experiment Description Language Based on XML -- Structural Similarity Evaluation of XML Documents Based on Basic Statistics -- An XML Data Query Method Based on Structure-Encoded.

In: Springer eBooks

Additional Edition: Printed edition: ISBN 9783642334689

Language: English

Subjects: Computer Science

Keywords: Konferenzschrift ; Konferenzschrift ; Konferenzschrift

DOI: 10.1007/978-3-642-33469-6

URL: http://dx.doi.org/10.1007/978-3-642-33469-6

URL: Volltext

URL: Volltext  (lizenzpflichtig)

URL: Volltext  (lizenzpflichtig)

URL: Cover

URL: Inhaltstext