Abstract is missing.
- Provable Preimage Under-Approximation for Neural NetworksXiyue Zhang, Benjie Wang, Marta Kwiatkowska. 3-23 [doi]
- Training for Verification: Increasing Neuron Stability to Scale DNN VerificationDong Xu 0021, Nusrat Jahan Mozumder, Hai Duong, Matthew B. Dwyer. 24-44 [doi]
- NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive SynthesisMatthias Cosler, Christopher Hahn, Ayham Omar, Frederik Schmitt. 45-67 [doi]
- sc HaliVer: Deductive Verification and Scheduling Languages Join ForcesLars B. van den Haak, Anton Wijs, Marieke Huisman, Mark van den Brand. 71-89 [doi]
- Gray-Box Fuzzing via Gradient Descent and Boolean Expression CoverageMartin Jonás, Jan Strejcek, Marek Trtík, Lukás Urban. 90-109 [doi]
- Fast Symbolic Computation of Bottom SCCsAnna Blume Jakobsen, Rasmus Skibdahl Melanchton Jørgensen, Jaco van de Pol, Andreas Pavlogiannis. 110-128 [doi]
- Btor2-Cert: A Certifying Hardware-Verification Framework Using Software AnalyzersZsófia Ádám, Dirk Beyer 0001, Po-Chun Chien, Nian-Ze Lee, Nils Sirrenberg. 129-149 [doi]
- Auction-Based SchedulingGuy Avni, Kaushik Mallik, Suman Sadhukhan. 153-172 [doi]
- Most General Winning Secure Equilibria Synthesis in Graph GamesSatya Prakash Nayak, Anne-Kathrin Schmuck. 173-193 [doi]
- On-The-Fly Algorithm for Reachability in Parametric Timed GamesMikael Bisgaard Dahlsen-Jensen, Baptiste Fievet, Laure Petrucci, Jaco van de Pol. 194-212 [doi]
- Rabin Games and Colourful Universal TreesRupak Majumdar, Irmak Saglam, K. S. Thejaswini. 213-231 [doi]
- Decidable Verification under Localized Release-Acquire ConcurrencyAbhishek Kr Singh, Ori Lahav 0001. 235-254 [doi]
- OxiDD - A Safe, Concurrent, Modular, and Performant Decision Diagram Framework in RustNils Husung, Clemens Dubslaff, Holger Hermanns, Maximilian A. Köhl. 255-275 [doi]
- Verification under TSO with an infinite Data DomainParosh Aziz Abdulla, Mohamed Faouzi Atig, Florian Furbach, Shashwat Garg. 276-295 [doi]
- State of the Art in Software Verification and Witness Validation: SV-COMP 2024Dirk Beyer 0001. 299-329 [doi]
- ConcurrentWitness2Test: Test-Harnessing the Power of Concurrency (Competition Contribution)Levente Bajczi, Zsófia Ádám, Zoltán Micskei. 330-334 [doi]
- Goblint Validator: Correctness Witness Validation by Abstract Interpretation - (Competition Contribution)Simmo Saan, Julian Erhard, Michael Schwarz 0007, Stanimir Bozhilov, Karoliine Holter, Sarah Tilscher, Vesal Vojdani, Helmut Seidl. 335-340 [doi]
- Witch 3: Validation of Violation Witnesses in the Witness Format 2.0 - (Competition Contribution)Paulína Ayaziová, Jan Strejcek. 341-346 [doi]
- AISE: A Symbolic Verifier by Synergizing Abstract Interpretation and Symbolic Execution (Competition Contribution)Zhen Wang, Zhenbang Chen. 347-352 [doi]
- Bubaak-SpLit: Split what you cannot verify (Competition contribution)Marek Chalupa, Cedric Richter. 353-358 [doi]
- CPAchecker 2.3 with Strategy Selection - (Competition Contribution)Daniel Baier, Dirk Beyer 0001, Po-Chun Chien, Marek Jankola, Matthias Kettl, Nian-Ze Lee, Thomas Lemberger 0002, Marian Lingsch Rosenfeld, Martin Spiessl, Henrik Wachowitz, Philipp Wendler. 359-364 [doi]
- CPV: A Circuit-Based Program VerifierPo-Chun Chien, Nian-Ze Lee. 365-370 [doi]
- EmergenTheta: Verification Beyond Abstraction Refinement (Competition Contribution)Levente Bajczi, Dániel Szekeres, Milán Mondok, Zsófia Ádám, Márk Somorjai, Csanád Telbisz, Mihály Dobos-Kovács, Vince Molnár. 371-375 [doi]
- ESBMC v7.4: Harnessing the Power of Intervals - (Competition Contribution)Rafael Sá Menezes, Mohannad Aldughaim, Bruno Farias, Xianzhiyu Li, Edoardo Manino, Fedor Shmarov, Kunjian Song, Franz Brauße, Mikhail R. Gadelha, Norbert Tihanyi, Konstantin Korovin, Lucas C. Cordeiro. 376-380 [doi]
- Goblint: Abstract Interpretation for Memory Safety and Termination - (Competition Contribution)Simmo Saan, Julian Erhard, Michael Schwarz 0007, Stanimir Bozhilov, Karoliine Holter, Sarah Tilscher, Vesal Vojdani, Helmut Seidl. 381-386 [doi]
- Mopsa-C: Improved Verification for C Programs, Simple Validation of Correctness Witnesses (Competition Contribution)Raphaël Monat, Marco Milanese, Francesco Parolini, Jérôme Boillot, Abdelraouf Ouadjaout, Antoine Miné. 387-392 [doi]
- PROTON: PRObes for Termination Or Not (Competition Contribution)Ravindra Metta, Hrishikesh Karmarkar, Kumar Madhukar, R. Venkatesh 0001, Supratik Chakraborty. 393-398 [doi]
- SWAT: Modular Dynamic Symbolic Execution for Java Applications using Dynamic Instrumentation (Competition Contribution)Nils Loose, Felix Mächtle, Florian Sieck, Thomas Eisenbarth 0001. 399-405 [doi]
- Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution - (Competition Contribution)Martin Jonás, Kristián Kumor, Jakub Novák, Jindrich Sedlácek, Marek Trtík, Lukás Zaoral, Paulína Ayaziová, Jan Strejcek. 406-411 [doi]
- Theta: Abstraction Based Techniques for Verifying Concurrency (Competition Contribution)Levente Bajczi, Csanád Telbisz, Márk Somorjai, Zsófia Ádám, Mihály Dobos-Kovács, Dániel Szekeres, Milán Mondok, Vince Molnár. 412-417 [doi]
- Ultimate Automizer and the Abstraction of Bitwise Operations - (Competition Contribution)Frank Schüssele, Manuel Bentele, Daniel Dietsch, Matthias Heizmann, Xinyu Jiang, Dominik Klumpp, Andreas Podelski. 418-423 [doi]