LEADER 06973nam 22005535 450 001 9910983388803321 005 20251113180254.0 010 $a3-031-72044-X 024 7 $a10.1007/978-3-031-72044-4 035 $a(MiAaPQ)EBC31654318 035 $a(Au-PeEL)EBL31654318 035 $a(CKB)34975742100041 035 $a(DE-He213)978-3-031-72044-4 035 $a(EXLCZ)9934975742100041 100 $a20240910d2025 u| 0 101 0 $aeng 135 $aurcnu|||||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aTests and Proofs $e18th International Conference, TAP 2024, Milan, Italy, September 9?10, 2024, Proceedings /$fedited by Marieke Huisman, Falk Howar 205 $a1st ed. 2025. 210 1$aCham :$cSpringer Nature Switzerland :$cImprint: Springer,$d2025. 215 $a1 online resource (184 pages) 225 1 $aLecture Notes in Computer Science,$x1611-3349 ;$v15153 311 08$a3-031-72043-1 327 $aIntro -- Preface -- Organization -- Invited Talk -- Formalising Requirements for Verification -- Contents -- Invited Talks -- Efficient Temporal Logic Runtime Monitoring for Tiny Systems -- 1 Introduction -- 2 Related Work -- 3 Linear Temporal Logic Runtime Monitoring on Small-Scale Systems - Step By Step -- 4 Keeping Track of Specification Violation Reasons -- 5 A Specialized Microcontroller Component for Temporal Logic Runtime Monitoring -- 6 Conclusion -- References -- Quality of Tests and Proofs -- Is MCDC Really Better? Lessons from Combining Tests and Proofs -- 1 Overview -- 1.1 Coverage Measures -- 1.2 The Need for MCDC -- 1.3 Precise Definition and Properties of MCDC -- 2 Technology Base -- 2.1 The AutoProof Environment -- 2.2 Seeding Contradiction for Test Generation -- 2.3 SC for Achieving Branch Coverage -- 3 Seeding Contradiction for Achieving MCDC -- 3.1 Approach -- 3.2 Implementation -- 4 Evaluation -- 4.1 Experimental Setup -- 4.2 MCDC-SC Versus Branch-SC -- 4.3 MCDC-SC Versus Branch-SC and Adaptive Random Testing -- 5 Related Work -- 6 Limitations and Threats to Validity -- 7 Conclusions and Future Work -- References -- Refining CEGAR-Based Test-Case Generation with Feasibility Annotations -- 1 Introduction -- 2 Overview of CEGAR-Based Test-Case Generation -- 3 Feasibility Checking with Feasibility Annotations -- 3.1 Integrating Feasibility Annotations Into Satisfiability Checking -- 3.2 Learning from Unsatisfiability Proofs of Model-Guided Checks -- 3.3 Implementation -- 4 Experiments -- 4.1 Experimental Setup -- 4.2 Experimental Results -- 4.3 Threats to Validity -- 5 Related Work -- 6 Conclusion -- References -- No Smoke Without Fire: Detecting Specification Inconsistencies with Frama-C/WP -- 1 Introduction -- 2 Tracked Inconsistencies -- 2.1 Pre-condition Errors -- 2.2 Post-condition Errors -- 2.3 Dead Code Errors. 327 $a2.4 Non-terminating Loops and Other Loop Errors -- 2.5 Exiting Errors -- 2.6 Avoiding Redundant Alarms -- 2.7 Avoiding Spurious Alarms -- 3 Design and Implementation -- 3.1 Reachability Analysis -- 3.2 Protected and Protecting Nodes -- 3.3 Weakest-Precondition Calculus for Smoke Tests -- 3.4 Proof Method -- 3.5 Providing Feedback to Users -- 4 Industrial Experiments -- 5 Related Work -- 6 Conclusion -- References -- Testing and Proving Advanced Properties -- Runtime Verification for High-Level Security Properties: Case Study on the TPM Software Stack -- 1 Introduction -- 2 The Frama-C Verification Platform and Its Wp, E-ACSL and MetAcsl Plug-ins -- 3 Overview of the TPM and its Software Stack -- 4 Companion Memory Modeling for Sensitive Data -- 5 Defining and Verifying High-Level Security Properties -- 6 Evaluation and Key Lessons -- 6.1 Threats to Validity -- 6.2 Key Lessons -- 7 Related Work -- 8 Conclusion and Future Work -- References -- Cyclone: A New Tool for Verifying/Testing Graph-Based Structures -- 1 Introduction -- 2 Architecture -- 2.1 Usage -- 3 Building Graphs -- 3.1 Variables -- 3.2 Conditional Variables -- 3.3 Nodes and Edges -- 3.4 Conditional Transitions -- 3.5 Path Conditions -- 4 Specifying Properties -- 4.1 Assertions -- 4.2 Invariants -- 4.3 Checking Modes -- 5 Preliminary Evaluation -- 6 Related Work -- 6.1 Limitations -- 7 Conclusion -- References -- Applications of Tests and Proofs -- Model-Based Testing of Quantum Computations -- 1 Introduction -- 2 Preliminaries -- 3 Test Models for Quantum Computations -- 3.1 Models of Quantum Computation -- 3.2 Process Models for Testing Quantum Computations -- 4 Test Processes for Quantum Computations -- 4.1 Test Processes and Tested Processes -- 4.2 Non-probabilistic Test Processes -- 4.3 Probabilistic Test Processes -- 5 Related Work -- 6 Conclusion -- References. 327 $aAffinitree: A Compositional Framework for Formal Analysis and Explanation of Deep Neural Networks -- 1 Introduction and Motivation -- 2 Theoretical Background -- 3 Related Work -- 4 Overview and Features -- 5 Design of Affinitree -- 5.1 Core Data Structure -- 5.2 Distillation Process -- 5.3 Modular Composition -- 5.4 Semantics-Preserving Pruning -- 5.5 Preconditions -- 6 Demonstration -- 6.1 Fairness Analysis -- 6.2 Decision Boundaries Near Adversarial Examples -- 6.3 Counterfactual Explanations -- 7 Conclusion -- References -- Exploring Loose Coupling of Slicing with Dynamic Symbolic Execution on the JVM -- 1 Introduction -- 2 Motivating Example -- 3 Analysis Pipeline -- 4 Results -- 5 Conclusion -- References -- Author Index. 330 $aThis book constitutes the proceedings of the 18th International Conference on Tests and Proofs, TAP 2024. TAP 2024 took place in Milan, Italy, on September 9 and 10, 2024 as part of the Formal Methods symposium (FM 2024), which included four more co-located conferences besides TAP: FMICS (Formal Methods in Industrial Critical Systems), LOPSTR (In ternational Symposium on Logic-based Program Synthesis and Transformation), PPDP (International Symposium on Principles and Practice of Declarative Pro gramming), and FACS (International Conference on Formal Aspects of Compo nent Software. The 7 full papers together with 1 short paper included in this volume were carefully reviewed and selected from 14 submissions. TAP?s scope encompasses many aspects of verification technology, including foundational work, tool development, and empirical research. 410 0$aLecture Notes in Computer Science,$x1611-3349 ;$v15153 606 $aReasoning 606 $aComputer science 606 $aInformal Logic 606 $aModels of Computation 615 0$aReasoning. 615 0$aComputer science. 615 14$aInformal Logic. 615 24$aModels of Computation. 676 $a160 700 $aHuisman$b Marieke$0995291 701 $aHowar$b Falk$01785515 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910983388803321 996 $aTests and Proofs$94317028 997 $aUNINA