LEADER 04431nam 22006015 450 001 9910983081803321 005 20241101115722.0 010 $a9783031676956 010 $a3031676955 024 7 $a10.1007/978-3-031-67695-6 035 $a(MiAaPQ)EBC31749091 035 $a(Au-PeEL)EBL31749091 035 $a(CKB)36479509800041 035 $a(Exl-AI)31749091 035 $a(DE-He213)978-3-031-67695-6 035 $a(EXLCZ)9936479509800041 100 $a20241101d2025 u| 0 101 0 $aeng 135 $aurcnu|||||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aTOOLympics Challenge 2023 $eUpdates, Results, Successes of the Formal-Methods Competitions /$fedited by Dirk Beyer, Arnd Hartmanns, Fabrice Kordon 205 $a1st ed. 2025. 210 1$aCham :$cSpringer Nature Switzerland :$cImprint: Springer,$d2025. 215 $a1 online resource (180 pages) 225 1 $aLecture Notes in Computer Science,$x1611-3349 ;$v14550 311 08$a9783031676949 311 08$a3031676947 327 $a Preface -- Organization -- Contents -- The ARCH-COMP Friendly Verification Competition for Continuous and Hybrid Systems -- 1 Introduction -- 2 Verification of Continuous, Hybrid, and Stochastic Systems -- 2.1 The Formal Verification Approach -- 2.2 Continuous, Hybrid, and Stochastic Systems -- 2.3 Verification Problems -- 2.4 Synthesis Problems -- 2.5 Problem Instances -- 2.6 Inherent Challenges in Evaluating Results -- 3 Competition Format and Organization -- 3.1 A Friendly Format -- 3.2 Organization and Schedule -- 3.3 Artifacts and Results -- 4 Thematic Groups of the Competition -- 4.1 Piecewise Constant Dynamics -- 4.2 Continuous and Hybrid Systems with Linear Dynamics -- 4.3 Nonlinear Dynamics -- 4.4 Artificial Intelligence and Neural Network Control Systems (AINNCS) -- 4.5 Stochastic Models -- 4.6 Falsification -- 4.7 Hybrid Systems Theorem Proving -- 5 Repeatability -- 6 Overall Achievements and Outlook -- References -- Competition of Solvers for Constrained Horn Clauses (CHC-COMP 2023) -- 1 Introduction -- 2 Organization$7Generated by AI. 330 $aTOOLympics 2023 was the third edition of a series of events to showcase competitions in the area of formal methods, colocated with the European Joint Conferences on Theory and Practice of Software (ETAPS 2023), held in April n Paris, France. The goal is to acknowledge the achievements of the various research competitions and comparative evaluations broadly related to the field of formal methods, to explain to the audience which tools from the field of formal methods they evaluate, and to understand their commonalities and differences. The developers of the participating tools typically participate in the competitions and evaluations, choosing the right parameters for the tools, or the best workflow for the approach. A total of ten competitions joined TOOLympics in 2023 and were presented at the event: CHC-COMP, MCC, QComp, ARCH-COMP, RERS, SL-COMP, SV-COMP, Test-Comp, VerifyThis, and the VT-Long-Term Challenge. Six of these are represented in this proceedings volume as papers: ARCH-COMP, CHC-COMP, MCC, QComp, VerifyThis, and the VerifyThis Long-Term Challenge. Each of these papers was peer-reviewed in single-blind mode. The papers will be of value to researchers and practitioners who employ formal methods approaches such as model checking, program analysis, probabilistic analysis, runtime verification, SAT solving, and SMT solving. 410 0$aLecture Notes in Computer Science,$x1611-3349 ;$v14550 606 $aComputer science 606 $aSoftware engineering 606 $aComputer Science Logic and Foundations of Programming 606 $aSoftware Engineering 606 $aTheory of Computation 615 0$aComputer science. 615 0$aSoftware engineering. 615 14$aComputer Science Logic and Foundations of Programming. 615 24$aSoftware Engineering. 615 24$aTheory of Computation. 676 $a004.0151 700 $aBeyer$b Dirk$01351238 701 $aHartmanns$b Arnd$01785819 701 $aKordon$b Fabrice$0863535 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910983081803321 996 $aTOOLympics Challenge 2023$94317287 997 $aUNINA