04129nam 2200565 450 991082763510332120230721035318.01-78920-184-510.1515/9781789201840(CKB)4100000007179041(MiAaPQ)EBC5606535(DE-B1597)636686(DE-B1597)9781789201840(EXLCZ)99410000000717904120181222d2007 uy 0engurcnu||||||||txtrdacontentcrdamediacrrdacarrierTelling children about the past an interdisciplinary perspective /edited by Nena Galanidou and Liv Helga DommasnesAnn Arbor, Michigan :International Monographs in Prehistory,2007.1 online resource (x, 324 pages) illustrationsInternational Monographs in Prehistory: Ethnoarchaeology Series ;61-879621-40-1 Introduction: Children and narratives of the past / Liv Helga Dommasnes and Nena Galanidou -- Cognitive and neural developments that make it possible to experience the past as the present / Patricia J. Bauer -- Autobiography, time, and history : children's construction of the past in family reminiscing / Robyn Fivush -- Representing the past in pictures / Alan Costall and Ann Richards -- Children's understanding of authenticity / Susan A. Gelman and Brandy N. Frazier -- Groovin' to ancient Peru : a critical analysis of Disney's The emperor's new groove / Helaine Silverman -- Telling children about the past using electronic games / Maria Economou -- In a child's eyes : human origins and the Paleolithic in children's book llustrations / Nena Galanidou -- Writing prehistory for children : a comparison between author and publisher-edited versions / Pascale Binant -- Museums and archaeological sites as the setting for wondrous tales / Christos Boulotis -- Exhibiting the past to children / Andromache Gazi -- Eviscerating Barbie : telling children about Egyptian mummification / Lauren E. Talalay and Todd Gerring -- Conversations about the past : families in an archaeology museum / Theano Moussouri -- Small people versus big heritage / Liv Helga Dommasnes -- Landscapes and winter counts : Lakota ways of telling children about the past / Craig Howe -- Telling children about the past in Brazil / Ana Pin and Pedro Funari -- From fragments to contexts : teaching prehistory to village children in Romania / Corina Sarbu and Dragos Gheorghiu.This book brings together archeologists, historians, psychologists, and educators from different countries and academic traditions to address the many ways that we tell children about the (distant) past. Knowing the past is fundamentally important for human societies, as well as for individual development. The authors expose many unquestioned assumptions and preformed images in narratives of the past that are routinely presented to children. The contributors both examine the ways in which children come to grips with the past and critically assess the many ways in which contemporary societies and an increasing number of commercial agents construct and use the past.Prehistoric peoplesStudy and teachingArchaeology and historyStudy and teachingArchaeologyStudy and teachingAntiquities, PrehistoricStudy and teachingArchaeology and Children.Individual Development.Teaching History.Teaching the Past.Use of the Past.Prehistoric peoplesStudy and teaching.Archaeology and historyStudy and teaching.ArchaeologyStudy and teaching.Antiquities, PrehistoricStudy and teaching.930.107Dommasnes Liv HelgaGalanidou NenaMiAaPQMiAaPQMiAaPQBOOK9910827635103321Telling children about the past3961949UNINA11511nam 22005535 450 991076359780332120251225193556.03-031-47705-710.1007/978-3-031-47705-8(MiAaPQ)EBC30881083(Au-PeEL)EBL30881083(DE-He213)978-3-031-47705-8(CKB)28817576600041(EXLCZ)992881757660004120231110d2024 u| 0engurcnu||||||||txtrdacontentcrdamediacrrdacarrierIntegrated Formal Methods 18th International Conference, IFM 2023, Leiden, The Netherlands, November 13–15, 2023, Proceedings /edited by Paula Herber, Anton Wijs1st ed. 2024.Cham :Springer Nature Switzerland :Imprint: Springer,2024.1 online resource (405 pages)Lecture Notes in Computer Science,1611-3349 ;143003-031-47704-9 Includes bibliographical references and index.Intro -- Preface -- Organization -- Abstract of Invited Talks -- Formal Signoff Flows -- Industrial Experience with a Verification-Aware Programming Language -- Contents -- Invited Presentations -- SMT: Something You Must Try -- 1 Introduction -- 2 Satisfiability Checking -- 2.1 SAT Solving -- 2.2 SMT Solving -- 3 Applications -- 3.1 A Toy Encoding Example -- 3.2 Planning with Optimization Modulo Theories -- 3.3 Reachability Analysis for Hybrid Systems with HyPro -- 3.4 Parameter Synthesis for Probabilistic Systems -- 4 Hybrid Petri Nets and Rate Adaption -- 4.1 Hybrid Petri Nets -- 4.2 Rate Adaption -- 4.3 Formulation as an SMT Problem -- 5 Some Final Remarks -- References -- Analysis and Verification -- Automated Sensitivity Analysis for Probabilistic Loops -- 1 Introduction -- 2 Preliminaries -- 2.1 Syntax and Semantics of Probabilistic Loops -- 2.2 C-finite Recurrences -- 2.3 Higher Moment Analysis Using Recurrences -- 3 Sensitivity Analysis -- 3.1 Sensitivity Analysis for Admissible Loops -- 3.2 Sensitivity Analysis for Non-admissible Loops -- 4 Experiments and Evaluation -- 5 Related Work -- 6 Conclusion -- References -- diffDP: Using Data Dependencies and Properties in Difference Verification with Conditions -- 1 Introduction -- 2 Foundations of Difference Verification with Conditions -- 3 Dependency and Property Aware Difference Detection -- 4 Evaluation -- 4.1 Experimental Setup -- 4.2 Experimental Results -- 5 Related Work -- 6 Conclusion -- References -- CHC Model Validation with Proof Guarantees -- 1 Introduction -- 2 Background -- 2.1 Constrained Horn Clauses -- 2.2 Related Witness Validation Approaches -- 3 Validation of CHC Models -- 4 Implementation -- 5 Evaluation -- 5.1 Benchmarks and Tools -- 5.2 Model Validation Results -- 5.3 Proof Checking Results -- 6 Conclusions -- References.VerifyThis: Memcached-A Practical Long-Term Challenge for the Integration of Formal Methods -- 1 Introduction -- 2 System Description -- 3 Challenge Goals -- 4 Participation, Time Schedule, Conclusion -- References -- Deductive Verification -- Towards Formal Verification of a TPM Software Stack -- 1 Introduction -- 2 Frama-C Verification Platform -- 3 The TPM Software Stack and the tpm2-tss Library -- 4 Dynamic Memory Allocation -- 5 Memory Management -- 6 Lemmas -- 7 Verification Results -- 8 Related Work -- 9 Conclusion and Future Work -- References -- Reasoning About Exceptional Behavior at the Level of Java Bytecode -- 1 Introduction -- 2 Motivating Example -- 3 Specifying and Verifying Exceptional Behavior -- 3.1 Specifying Exceptional Behavior -- 3.2 The Vimp Intermediate Representation -- 3.3 Modeling Exceptional Control Flow -- 3.4 Transformation Order and Boogie Code Generation -- 3.5 Implementation Details -- 4 Experiments -- 4.1 Programs -- 4.2 Results -- 5 Related Work -- 6 Conclusions -- References -- Analysis and Formal Specification of OpenJDK's BitSet -- 1 Introduction -- 2 The BitSet Class -- 3 Formal Specification -- 3.1 Class Invariant -- 3.2 The wordsToSeq() Model Method -- 3.3 The get(int,int) Method -- 4 Issues in BitSet -- 4.1 A Bug in get(int,int) Caused by a Negative length() -- 4.2 Bugs Caused by valueOf(...) Corrupting length() -- 4.3 Solution Directions -- 5 Towards Formal Verification of the BitSet Class -- 5.1 Background -- 5.2 Proof Sketch of get(int,int) -- 5.3 Required Extensions to KeY -- 6 Conclusion -- References -- Joining Forces! Reusing Contracts for Deductive Verifiers Through Automatic Translation -- 1 Introduction -- 2 Design of the Specification Translator -- 3 Translating Annotations -- 3.1 OpenJML -- 3.2 Krakatoa -- 3.3 VerCors -- 4 Evaluation -- 4.1 Reuse of Specifications -- 4.2 Reuse of Tools.5 Related Work -- 6 Conclusion -- References -- Hardware and Memory Verification -- Lifting the Reasoning Level in Generic Weak Memory Verification -- 1 Introduction -- 2 Program Syntax -- 3 Axiomatic Reasoning -- 3.1 Axioms -- 3.2 Reasoning Example on Axiom Level -- 4 Rules -- 5 Correctness Proof of WRC via Proof Rules -- 6 Related Work -- 7 Conclusion -- References -- Automatic Formal Verification of RISC-V Pipelined Microprocessors with Fault Tolerance by Spatial Redundancy at a High Level of Abstraction -- 1 Introduction -- 2 Background on Using Positive Equality to Formally Verify Pipelined Processors -- 3 Efficient Modeling of the RISC-V Architecture at a High Level of Abstraction -- 3.1 Abstraction of the Register File -- 3.2 Abstraction of the Decoding Logic -- 3.3 Abstraction of the CSR Memory Array -- 3.4 Non-Pipelined Specifications -- 3.5 Formal Verification of Liveness -- 3.6 Invariant Constraints Were Not Needed for the Correct Designs, but Were Proved for Debugging the 4-Stage Pipelined Processor -- 4 Modeling of Spatial Redundancy in Pipelined Processors at a High Level of Abstraction for Formal Verification of Safety -- 5 Results -- 6 Conclusion -- References -- Refinement and Separation: Modular Verification of Wandering Trees -- 1 Introduction -- 2 Wandering Trees -- 3 Structured Specifications of Algebraic Data Types -- 3.1 Algebraic Definitions -- 3.2 Modeling the Heap and Separation Logic -- 4 Modular Software Systems -- 5 Modularization -- 5.1 Specification of the Index -- 5.2 Index Refinement -- 5.3 Tree Refinement -- 5.4 Pointer Structures in the Heap and on Flash -- 6 Verification -- 6.1 Correctness of the Tree Component -- 6.2 Correctness of Wandering Trees -- 6.3 Correctness of Flash Representation -- 7 Conclusion -- References -- Verification and Learning.Performance Fuzzing with Reinforcement-Learning and Well-Defined Constraints for the B Method -- 1 Introduction -- 2 Background -- 2.1 ProB and the B Method -- 2.2 Performance Fuzzing -- 2.3 Thompson Sampling -- 3 The BanditFuzz Algorithm -- 4 Adapting BanditFuzz for ProB -- 4.1 Fuzzing for Classical B Instead of SMT-LIB -- 4.2 Targeted Fuzzing and Mutating -- 4.3 Well-Defined ASTs -- 5 Running the Performance Fuzzer -- 5.1 Fuzzing only -- 5.2 Performance Fuzzing Between ProB's Backends -- 5.3 Performance Fuzzing Between ProB's Settings -- 5.4 Performance Fuzzing Between the SMT-LIB Translations -- 6 Related Work -- 7 Discussion -- 8 Conclusions -- References -- Reinforcement Learning Under Partial Observability Guided by Learned Environment Models -- 1 Introduction -- 2 Preliminaries -- 2.1 Models -- 2.2 Learning MDPs -- 3 QA-Learning: RL Assisted by Automata Learning -- 3.1 Overview -- 3.2 Extended State Space -- 3.3 Partially Observable Q-Learning -- 3.4 Convergence -- 3.5 Generalization and Limitations -- 4 Evaluation -- 5 Related Work -- 6 Conclusion -- References -- Temporal Logics -- Mission-Time LTL (MLTL) Formula Validation via Regular Expressions -- 1 Introduction -- 2 Preliminaries: Mission-Time LTL and Bit String Computations -- 3 MLTL Regular Expressions -- 4 WEST Algorithm and Analysis -- 4.1 Proof of Correctness of WEST -- 4.2 Theoretical Complexity -- 4.3 Experimental Benchmarking -- 5 Correctness of WEST Tool Implementation -- 5.1 Intelligent Fuzzing -- 6 Regular Expression Simplification Theorem (REST) -- 6.1 Theoretical Analysis of REST -- 6.2 Experimental Benchmarking of REST -- 7 Using WEST: An Example -- 8 Closing Remarks -- 8.1 Future Work -- References -- Symbolic Model Checking of Relative Safety LTL Properties -- 1 Introduction -- 2 Motivating Examples -- 2.1 Bounded Response Example -- 2.2 Safety Contracts.2.3 LTL G p vs. Invariant -- 3 Related Work -- 4 Notation and Preliminary Definitions -- 4.1 Notation for Sequences, Concatenation and Prefix -- 4.2 Safety and Relative Safety -- 4.3 LTL and Safety Fragments -- 4.4 Symbolic Transition System and Invariant Checking -- 4.5 Symbolic Techniques Reducing LTL Model Checking to Invariant Checking -- 5 Symbolic Compilation of Safety LTL -- 5.1 Symbolic Compilation of Full LTL -- 5.2 Symbolic Compilation of SafetyLTL -- 5.3 Symbolic Construction of Live Systems -- 6 Algorithm -- 6.1 Simple Algorithm Without Loops -- 6.2 CEGAR Loop Algorithm -- 6.3 Extending Algorithm with Lookahead -- 7 Experimental Evaluation -- 7.1 Benchmarks -- 7.2 Experimental Results and Analysis -- 8 Conclusions and Future Work -- References -- Extending PlusCal for Modeling Distributed Algorithms -- 1 Introduction -- 2 TLA+ and PlusCal -- 2.1 The Specification Language TLA+ -- 2.2 The Algorithmic Langage PlusCal -- 2.3 Translating PlusCal to TLA+ -- 3 Distributed PlusCal -- 3.1 Sub-processes -- 3.2 Communication Channels -- 4 Evaluation -- 4.1 Two Distributed Algorithms Expressed in Distributed PlusCal -- 4.2 Related Work -- 5 Conclusion -- References -- Autonomous Systems -- Formal Modelling and Analysis of a Self-Adaptive Robotic System -- 1 Introduction -- 2 Case Study: Pipeline Inspection by AUV -- 3 Modelling the AUV Case Study with ProFeat -- 3.1 The Feature Model -- 3.2 The Managed Subsystem -- 3.3 The Environment -- 3.4 The Managing Subsystem -- 4 Analysis -- 5 Related Work -- 6 Discussion and Future Work -- References -- CAN-verify: A Verification Tool For BDI Agents -- 1 Introduction -- 2 Can-Overview -- 3 CAN-verify Components and Features -- 4 Examples -- 5 Discussion and Conclusion -- References -- PhD Symposium Presentations -- Scalable and Precise Refinement Types for Imperative Languages -- 1 Introduction.2 Combining Refinement Type Systems and Deductive Verification.This volume LNCS 14300 constitutes the refereed proceedings of the 18th International Conference, IFM 2023, in November 2023, held in Leiden, The Netherlands. The 16 full papers presented together with 2 short papers were carefully reviewed and selected from 51 submissions. The conference focuses on all aspects of the design of integrated techniques, including language design, verification and validation, automated tool support, and the use of such techniques in software engineering practice.Lecture Notes in Computer Science,1611-3349 ;14300Software engineeringSoftware EngineeringSoftware engineering.Software Engineering.004.0151Herber PaulaWijs AntonMiAaPQMiAaPQMiAaPQBOOK9910763597803321Integrated Formal Methods2860239UNINA