TACAS '22
April 7, 2022
Munich

Publications of SV-COMP

SV-COMP 2024

1. D. Beyer. State of the Art in Software Verification and Witness Validation: SV-COMP 2024. In Proc. TACAS (3), LNCS 14572, pages 299-329, 2024. Springer. doi:10.1007/978-3-031-57256-2_15 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{SVCOMP24, author = {D.~Beyer}, title = {State of the Art in Software Verification and Witness Validation: {SV-COMP 2024}}, booktitle = {Proc.\ TACAS~(3)}, pages = {299-329}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_15}, }
2. L. Bajczi, Z. Ádám, and Z. Micskei. ConcurrentWitness2Test (Competition Contribution). In Proc. TACAS (3), LNCS 14572, pages 330-334, 2024. Springer. doi:10.1007/978-3-031-57256-2_16 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{CONCURRENTWITNESSTOTEST-SVCOMP24, author = {L.~Bajczi and Z.~Ádám and Z.~Micskei}, title = {{ConcurrentWitness2Test} (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {330-334}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_16}, }
3. S. Saan, J. Erhard, M. Schwarz, S. Bozhilov, K. Holter, S. Tilscher, V. Vojdani, and H. Seidl. Goblint Validator: Correctness Witness Validation by Abstract Interpretation (Competition Contribution). In Proc. TACAS (3), LNCS 14572, pages 335-340, 2024. Springer. doi:10.1007/978-3-031-57256-2_17 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{GOBLINTVALIDATOR-SVCOMP24, author = {S.~Saan and J.~Erhard and M.~Schwarz and S.~Bozhilov and K.~Holter and S.~Tilscher and V.~Vojdani and H.~Seidl}, title = {{Goblint Validator}: {Correctness} Witness Validation by Abstract Interpretation (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {335-340}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_17}, }
4. P. Ayaziová and J. Strejček. Witch 3: Validation of Violation Witnesses in the Witness Format 2.0 (Competition Contribution). In Proc. TACAS (3), LNCS 14572, pages 341-346, 2024. Springer. doi:10.1007/978-3-031-57256-2_18 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{WITCH-SVCOMP24, author = {P.~Ayaziová and J.~Strejček}, title = {{Witch 3}: {Validation} of Violation Witnesses in the Witness Format~2.0 (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {341-346}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_18}, }
5. Z. Wang and Z. Chen. AISE: A Symbolic Verifier by Synergizing Abstract Interpretation and Symbolic Execution (Competition Contribution). In Proc. TACAS (3), LNCS 14572, pages 347-352, 2024. Springer. doi:10.1007/978-3-031-57256-2_19 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{AISE-SVCOMP24, author = {Z.~Wang and Z.~Chen}, title = {{AISE}: {A} Symbolic Verifier by Synergizing Abstract Interpretation and Symbolic Execution (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {347-352}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_19}, }
6. M. Chalupa and C. Richter. Bubaak-SpLit: Split What You Cannot Verify (Competition Contribution). In Proc. TACAS (3), LNCS 14572, pages 353-358, 2024. Springer. doi:10.1007/978-3-031-57256-2_20 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{BUBAAKSPLIT-SVCOMP24, author = {M.~Chalupa and C.~Richter}, title = {{Bubaak-SpLit}: {Split} What You Cannot Verify (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {353-358}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_20}, }
7. D. Baier, D. Beyer, P.-C. Chien, M. Jankola, M. Kettl, N.-Z. Lee, T. Lemberger, M. Lingsch-Rosenfeld, M. Spiessl, H. Wachowitz, and P. Wendler. CPAchecker 2.3 with Strategy Selection (Competition Contribution). In Proc. TACAS (3), LNCS 14572, pages 359-364, 2024. Springer. doi:10.1007/978-3-031-57256-2_21 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{CPACHECKER-SVCOMP24, author = {D.~Baier and D.~Beyer and P.-C.~Chien and M.~Jankola and M.~Kettl and N.-Z.~Lee and T.~Lemberger and M.~Lingsch-Rosenfeld and M.~Spiessl and H.~Wachowitz and P.~Wendler}, title = {{CPAchecker} 2.3 with Strategy Selection (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {359-364}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_21}, }
8. P.-C. Chien and N.-Z. Lee. CPV: A Circuit-Based Program Verifier (Competition Contribution). In Proc. TACAS (3), LNCS 14572, pages 365-370, 2024. Springer. doi:10.1007/978-3-031-57256-2_22 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{CPV-SVCOMP24, author = {P.-C.~Chien and N.-Z.~Lee}, title = {{CPV}: {A} Circuit-Based Program Verifier (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {365-370}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_22}, }
9. L. Bajczi, D. Szekeres, M. Mondok, Z. Ádám, M. Somorjai, C. Telbisz, M. Dobos-Kovács, and V. Molnár. EmergenTheta (Competition Contribution). In Proc. TACAS (3), LNCS 14572, pages 371-375, 2024. Springer. doi:10.1007/978-3-031-57256-2_23 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{EMERGENTHETA-SVCOMP24, author = {L.~Bajczi and D.~Szekeres and M.~Mondok and Z.~Ádám and M.~Somorjai and C.~Telbisz and M.~Dobos-Kovács and V.~Molnár}, title = {{EmergenTheta} (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {371-375}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_23}, }
10. R. Menezes, M. Aldughaim, B. Farias, X. Li, E. Manino, F. Shmarov, K. Song, F. Brauße, M. R. Gadelha, N. Tihanyi, K. Korovin, and L. Cordeiro. ESBMC v7.4: Harnessing the Power of Intervals (Competition Contribution). In Proc. TACAS (3), LNCS 14572, pages 376-380, 2024. Springer. doi:10.1007/978-3-031-57256-2_24 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{ESBMC-SVCOMP24, author = {R.~Menezes and M.~Aldughaim and B.~Farias and X.~Li and E.~Manino and F.~Shmarov and K.~Song and F.~Brauße and M.~R.~Gadelha and N.~Tihanyi and K.~Korovin and L.~Cordeiro}, title = {{ESBMC v7.4}: {Harnessing} the Power of Intervals (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {376-380}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_24}, }
11. S. Saan, J. Erhard, M. Schwarz, S. Bozhilov, K. Holter, S. Tilscher, V. Vojdani, and H. Seidl. Goblint: Abstract Interpretation for Memory Safety and Termination (Competition Contribution). In Proc. TACAS (3), LNCS 14572, pages 381-386, 2024. Springer. doi:10.1007/978-3-031-57256-2_25 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{GOBLINT-SVCOMP24, author = {S.~Saan and J.~Erhard and M.~Schwarz and S.~Bozhilov and K.~Holter and S.~Tilscher and V.~Vojdani and H.~Seidl}, title = {{Goblint}: {Abstract} Interpretation for Memory Safety and Termination (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {381-386}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_25}, }
12. R. Monat, M. Milanese, F. Parolini, J. Boillot, A. Ouadjaout, and A. Miné. Mopsa-C: Improved Verification for C Programs, Simple Validation of Correctness Witnesses (Competition Contribution). In Proc. TACAS (3), LNCS 14572, pages 387-392, 2024. Springer. doi:10.1007/978-3-031-57256-2_26 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{MOPSAC-SVCOMP24, author = {R.~Monat and M.~Milanese and F.~Parolini and J.~Boillot and A.~Ouadjaout and A.~Miné}, title = {{Mopsa-C}: {Improved} Verification for {C} Programs, Simple Validation of Correctness Witnesses (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {387-392}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_26}, }
13. R. Metta, H. Karmarkar, K. Madhukar, R. Venkatesh, and S. Chakraborty. Proton: Probes for Non-termination and Termination (Competition Contribution). In Proc. TACAS (3), LNCS 14572, pages 393-398, 2024. Springer. doi:10.1007/978-3-031-57256-2_27 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{PROTON-SVCOMP24, author = {R.~Metta and H.~Karmarkar and K.~Madhukar and R.~Venkatesh and S.~Chakraborty}, title = {{Proton}: {Probes} for Non-termination and Termination (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {393-398}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_27}, }
14. N. Loose, F. Mächtle, F. Sieck, and T. Eisenbarth. SWAT: Modular Dynamic Symbolic Execution for Java Applications using Dynamic Instrumentation (Competition Contribution). In Proc. TACAS (3), LNCS 14572, pages 399-405, 2024. Springer. doi:10.1007/978-3-031-57256-2_28 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{SWAT-SVCOMP24, author = {N.~Loose and F.~Mächtle and F.~Sieck and T.~Eisenbarth}, title = {{SWAT}: {Modular} Dynamic Symbolic Execution for Java Applications using Dynamic Instrumentation (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {399-405}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_28}, }
15. M. Jonáš, K. Kumor, J. Novák, J. Sedláček, M. Trtík, L. Zaoral, P. Ayaziová, and J. Strejček. Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution (Competition Contribution). In Proc. TACAS (3), LNCS 14572, pages 406-411, 2024. Springer. doi:10.1007/978-3-031-57256-2_29 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{SYMBIOTIC-SVCOMP24, author = {M.~Jonáš and K.~Kumor and J.~Novák and J.~Sedláček and M.~Trtík and L.~Zaoral and P.~Ayaziová and J.~Strejček}, title = {{Symbiotic 10}: {Lazy} Memory Initialization and Compact Symbolic Execution (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {406-411}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_29}, }
16. L. Bajczi, C. Telbisz, M. Somorjai, Z. Ádám, M. Dobos-Kovács, D. Szekeres, M. Mondok, and V. Molnár. Theta (Competition Contribution). In Proc. TACAS (3), LNCS 14572, pages 412-417, 2024. Springer. doi:10.1007/978-3-031-57256-2_30 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{THETA-SVCOMP24, author = {L.~Bajczi and C.~Telbisz and M.~Somorjai and Z.~Ádám and M.~Dobos-Kovács and D.~Szekeres and M.~Mondok and V.~Molnár}, title = {{Theta} (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {412-417}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_30}, }
17. M. Heizmann, M. Bentele, D. Dietsch, X. Jiang, D. Klumpp, F. Schüssele, and A. Podelski. Ultimate Automizer and the Abstraction of Bitwise Operations (Competition Contribution). In Proc. TACAS (3), LNCS 14572, pages 418-423, 2024. Springer. doi:10.1007/978-3-031-57256-2_31 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{ULTIMATEAUTOMIZER-SVCOMP24, author = {M.~Heizmann and M.~Bentele and D.~Dietsch and X.~Jiang and D.~Klumpp and F.~Schüssele and A.~Podelski}, title = {Ultimate Automizer and the Abstraction of Bitwise Operations (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {418-423}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_31}, }

SV-COMP 2023

1. D. Beyer. Competition on Software Verification and Witness Validation: SV-COMP 2023. In Proc. TACAS (2), LNCS 13994, pages 495-522, 2023. Springer. doi:10.1007/978-3-031-30820-8_29 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{SVCOMP23, author = {D.~Beyer}, title = {Competition on Software Verification and Witness Validation: {SV-COMP 2023}}, booktitle = {Proc.\ TACAS~(2)}, pages = {495-522}, year = {2023}, series = {LNCS~13994}, publisher = {Springer}, doi = {10.1007/978-3-031-30820-8_29}, }
2. P. Ayaziová and J. Strejček. Symbiotic-Witch 2: More Efficient Algorithm and Witness Refutation (Competition Contribution). In Proc. TACAS (2), LNCS 13994, pages 523-528, 2023. Springer. doi:10.1007/978-3-031-30820-8_30 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{SYMBIOTICWITCH-SVCOMP23, author = {P.~Ayaziová and J.~Strejček}, title = {{Symbiotic-Witch 2}: {More} Efficient Algorithm and Witness Refutation (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {523-528}, year = {2023}, series = {LNCS~13994}, publisher = {Springer}, doi = {10.1007/978-3-031-30820-8_30}, }
3. V. Malík, P. Schrammel, T. Vojnar, and F. Nečas. 2LS: Arrays and Loop Unwinding (Competition Contribution). In Proc. TACAS (2), LNCS 13994, pages 529-534, 2023. Springer. doi:10.1007/978-3-031-30820-8_31 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{2LS-SVCOMP23, author = {V.~Malík and P.~Schrammel and T.~Vojnar and F.~Nečas}, title = {{2LS}: {Arrays} and Loop Unwinding (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {529-534}, year = {2023}, series = {LNCS~13994}, publisher = {Springer}, doi = {10.1007/978-3-031-30820-8_31}, }
4. M. Chalupa and T. Henzinger. Bubaak: Runtime Monitoring of Program Verifiers (Competition Contribution). In Proc. TACAS (2), LNCS 13994, pages 535-540, 2023. Springer. doi:10.1007/978-3-031-30820-8_32 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{BUBAAK-SVCOMP23, author = {M.~Chalupa and T.~Henzinger}, title = {{Bubaak}: {Runtime} Monitoring of Program Verifiers (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {535-540}, year = {2023}, series = {LNCS~13994}, publisher = {Springer}, doi = {10.1007/978-3-031-30820-8_32}, }
5. F. Aljaafari, F. Shmarov, E. Manino, R. Menezes, and L. Cordeiro. EBF 4.2: Black-Box Cooperative Verification for Concurrent Programs (Competition Contribution). In Proc. TACAS (2), LNCS 13994, pages 541-546, 2023. Springer. doi:10.1007/978-3-031-30820-8_33 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{EBF-SVCOMP23, author = {F.~Aljaafari and F.~Shmarov and E.~Manino and R.~Menezes and L.~Cordeiro}, title = {{EBF 4.2}: {Black-Box} Cooperative Verification for Concurrent Programs (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {541-546}, year = {2023}, series = {LNCS~13994}, publisher = {Springer}, doi = {10.1007/978-3-031-30820-8_33}, }
6. S. Saan, M. Schwarz, J. Erhard, M. Pietsch, H. Seidl, S. Tilscher, and V. Vojdani. Goblint: Autotuning Thread-Modular Abstract Interpretation (Competition Contribution). In Proc. TACAS (2), LNCS 13994, pages 547-552, 2023. Springer. doi:10.1007/978-3-031-30820-8_34 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{GOBLINT-SVCOMP23, author = {S.~Saan and M.~Schwarz and J.~Erhard and M.~Pietsch and H.~Seidl and S.~Tilscher and V.~Vojdani}, title = {{Goblint}: {Autotuning} Thread-Modular Abstract Interpretation (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {547-552}, year = {2023}, series = {LNCS~13994}, publisher = {Springer}, doi = {10.1007/978-3-031-30820-8_34}, }
7. S. Hussein, Q. Yan, S. McCamant, V. Sharma, and M. Whalen. Java Ranger: Supporting String and Array Operations (Competition Contribution). In Proc. TACAS (2), LNCS 13994, pages 553-558, 2023. Springer. doi:10.1007/978-3-031-30820-8_35 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{JAVARANGER-SVCOMP23, author = {S.~Hussein and Q.~Yan and S.~McCamant and V.~Sharma and M.~Whalen}, title = {{Java Ranger}: {Supporting} String and Array Operations (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {553-558}, year = {2023}, series = {LNCS~13994}, publisher = {Springer}, doi = {10.1007/978-3-031-30820-8_35}, }
8. G. Ernst. Korn: Horn clause based Verification of C programs (Competition Contribution). In Proc. TACAS (2), LNCS 13994, pages 559-564, 2023. Springer. doi:10.1007/978-3-031-30820-8_36 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{KORN-SVCOMP23, author = {G.~Ernst}, title = {{Korn}: {Horn} clause based Verification of {C} programs (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {559-564}, year = {2023}, series = {LNCS~13994}, publisher = {Springer}, doi = {10.1007/978-3-031-30820-8_36}, }
9. R. Monat, A. Ouadjaout, and A. Miné. Mopsa-C: Modular Domains and Relational Abstract Interpretation for C Programs (Competition Contribution). In Proc. TACAS (2), LNCS 13994, pages 565-570, 2023. Springer. doi:10.1007/978-3-031-30820-8_37 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{MOPSA-SVCOMP23, author = {R.~Monat and A.~Ouadjaout and A.~Miné}, title = {{Mopsa-C}: {Modular} Domains and Relational Abstract Interpretation for {C} Programs (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {565-570}, year = {2023}, series = {LNCS~13994}, publisher = {Springer}, doi = {10.1007/978-3-031-30820-8_37}, }
10. J. Su, Z. Yang, H. Xing, J. Yang, C. Tian, and Z. Duan. PIChecker: A POR and Interpolation-Based Verifier for Concurrent Programs (Competition Contribution). In Proc. TACAS (2), LNCS 13994, pages 571-576, 2023. Springer. doi:10.1007/978-3-031-30820-8_38 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{PICHECKER-SVCOMP23, author = {J.~Su and Z.~Yang and H.~Xing and J.~Yang and C.~Tian and Z.~Duan}, title = {{PIChecker}: {A} {POR} and Interpolation-Based Verifier for Concurrent Programs (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {571-576}, year = {2023}, series = {LNCS~13994}, publisher = {Springer}, doi = {10.1007/978-3-031-30820-8_38}, }
11. M. Heizmann, M. Barth, D. Dietsch, L. Fichtner, J. Hoenicke, D. Klumpp, M. Naouar, T. Schindler, F. Schüssele, and A. Podelski. Ultimate Automizer 2023 (Competition Contribution). In Proc. TACAS (2), LNCS 13994, pages 577-581, 2023. Springer. doi:10.1007/978-3-031-30820-8_39 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{UAUTOMIZER-SVCOMP23, author = {M.~Heizmann and M.~Barth and D.~Dietsch and L.~Fichtner and J.~Hoenicke and D.~Klumpp and M.~Naouar and T.~Schindler and F.~Schüssele and A.~Podelski}, title = {{Ultimate Automizer} 2023 (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {577-581}, year = {2023}, series = {LNCS~13994}, publisher = {Springer}, doi = {10.1007/978-3-031-30820-8_39}, }
12. D. Dietsch, M. Heizmann, D. Klumpp, F. Schüssele, and A. Podelski. Ultimate Taipan 2023 (Competition Contribution). In Proc. TACAS (2), LNCS 13994, pages 582-587, 2023. Springer. doi:10.1007/978-3-031-30820-8_40 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{UTAIPAN-SVCOMP23, author = {D.~Dietsch and M.~Heizmann and D.~Klumpp and F.~Schüssele and A.~Podelski}, title = {{Ultimate Taipan} 2023 (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {582-587}, year = {2023}, series = {LNCS~13994}, publisher = {Springer}, doi = {10.1007/978-3-031-30820-8_40}, }
13. P. Darke, B. Chimdyalwar, S. Agrawal, R. Venkatesh, S. Chakraborty, and S. Kumar. VeriAbsL: Scalable Verification by Abstraction and Strategy Prediction (Competition Contribution). In Proc. TACAS (2), LNCS 13994, pages 588-593, 2023. Springer. doi:10.1007/978-3-031-30820-8_41 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{VERIABSL-SVCOMP23, author = {P.~Darke and B.~Chimdyalwar and S.~Agrawal and R.~Venkatesh and S.~Chakraborty and S.~Kumar}, title = {{VeriAbsL}: {Scalable} Verification by Abstraction and Strategy Prediction (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {588-593}, year = {2023}, series = {LNCS~13994}, publisher = {Springer}, doi = {10.1007/978-3-031-30820-8_41}, }
14. R. Metta, P. Yeduru, H. Karmarkar, and R. K. Medicherla. VeriFuzz 1.4: Checking for (Non-)Termination (Competition Contribution). In Proc. TACAS (2), LNCS 13994, pages 594-599, 2023. Springer. doi:10.1007/978-3-031-30820-8_42 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{VERIFUZZ-SVCOMP23, author = {R.~Metta and P.~Yeduru and H.~Karmarkar and R.~K.~Medicherla}, title = {{VeriFuzz 1.4}: {Checking} for (Non-)Termination (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {594-599}, year = {2023}, series = {LNCS~13994}, publisher = {Springer}, doi = {10.1007/978-3-031-30820-8_42}, }
15. M. Gerhold and A. Hartmanns. Reproduction Report for SV-COMP 2023. University of Twente, 2023. doi:10.48550/arXiv.2303.06477 Publisher's Version PDF
    BibTeX Entry

    @techreport{REPRODUCTION-SVCOMP23, author = {M.~Gerhold and A.~Hartmanns}, title = {Reproduction Report for {SV-COMP} 2023}, year = {2023}, doi = {10.48550/arXiv.2303.06477}, institution = {University of Twente}, }

SV-COMP 2022

1. D. Beyer. Progress on Software Verification: SV-COMP 2022. In Proc. TACAS (2), LNCS 13244, pages 375-402, 2022. Springer. doi:10.1007/978-3-030-99527-0_20 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{SVCOMP22, author = {D.~Beyer}, title = {Progress on Software Verification: {SV-COMP 2022}}, booktitle = {Proc.\ TACAS~(2)}, pages = {375-402}, year = {2022}, series = {LNCS~13244}, publisher = {Springer}, doi = {10.1007/978-3-030-99527-0_20}, }
2. H. Ponce-De-Leon, T. Haas, and R. Meyer. Dartagnan: SMT-based Violation Witness Validation (Competition Contribution). In Proc. TACAS (2), LNCS 13244, pages 418-423, 2022. Springer. doi:10.1007/978-3-030-99527-0_24 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{DARTAGNAN-SVCOMP22, author = {H.~Ponce-De-Leon and T.~Haas and R.~Meyer}, title = {{Dartagnan}: SMT-based Violation Witness Validation (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {418-423}, year = {2022}, series = {LNCS~13244}, publisher = {Springer}, doi = {10.1007/978-3-030-99527-0_24}, }
3. F. Howar and M. Mues. GWit (Competition Contribution). In Proc. TACAS (2), LNCS 13244, pages 446-450, 2022. Springer. doi:10.1007/978-3-030-99527-0_29 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{GWIT-SVCOMP22, author = {F.~Howar and M.~Mues}, title = {{GWit} (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {446-450}, year = {2022}, series = {LNCS~13244}, publisher = {Springer}, doi = {10.1007/978-3-030-99527-0_29}, }
4. P. Ayaziová, M. Chalupa, and J. Strejček. Symbiotic-Witch: A Klee-Based Violation Witness Checker (Competition Contribution). In Proc. TACAS (2), LNCS 13244, pages 468-473, 2022. Springer. doi:10.1007/978-3-030-99527-0_33 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{SYMBIOTIC-WITCH-SVCOMP22, author = {P.~Ayaziová and M.~Chalupa and J.~Strejček}, title = {{Symbiotic-Witch}: {A} {Klee}-Based Violation Witness Checker (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {468-473}, year = {2022}, series = {LNCS~13244}, publisher = {Springer}, doi = {10.1007/978-3-030-99527-0_33}, }
5. T. Wu, P. Schrammel, and L. Cordeiro. Wit4Java: A violation-witness validator for Java Verifiers (Competition Contribution). In Proc. TACAS (2), LNCS 13244, pages 484-489, 2022. Springer. doi:10.1007/978-3-030-99527-0_36 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{WIT4JAVA-SVCOMP22, author = {T.~Wu and P.~Schrammel and L.~Cordeiro}, title = {{Wit4Java}: {A} violation-witness validator for {Java} Verifiers (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {484-489}, year = {2022}, series = {LNCS~13244}, publisher = {Springer}, doi = {10.1007/978-3-030-99527-0_36}, }
6. J. Hensel, C. Mensendiek, and J. Giesl. AProVE: Non-termination Witnesses for C Programs (Competition Contribution). In Proc. TACAS (2), LNCS 13244, pages 403-407, 2022. Springer. doi:10.1007/978-3-030-99527-0_21 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{APROVE-SVCOMP22, author = {J.~Hensel and C.~Mensendiek and J.~Giesl}, title = {{AProVE}: {N}on-termination Witnesses for {C} Programs (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {403-407}, year = {2022}, series = {LNCS~13244}, publisher = {Springer}, doi = {10.1007/978-3-030-99527-0_21}, }
7. L. Bu, Z. Xie, L. Lyu, Y. Li, X. Guo, J. Zhao, and X. Li. Brick: Path Enumeration-Based Bounded Reachability Checking of C Programs (Competition Contribution). In Proc. TACAS (2), LNCS 13244, pages 408-412, 2022. Springer. doi:10.1007/978-3-030-99527-0_22 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{BRICK-SVCOMP22, author = {L.~Bu and Z.~Xie and L.~Lyu and Y.~Li and X.~Guo and J.~Zhao and X.~Li}, title = {{Brick}: {P}ath Enumeration-Based Bounded Reachability Checking of {C} Programs (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {408-412}, year = {2022}, series = {LNCS~13244}, publisher = {Springer}, doi = {10.1007/978-3-030-99527-0_22}, }
8. A. Coto, O. Inverso, E. Sales, and E. Tuosto. A Prototype for Data Race Detection in CSeq 3 (Competition Contribution). In Proc. TACAS (2), LNCS 13244, pages 413-417, 2022. Springer. doi:10.1007/978-3-030-99527-0_23 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{CSEQ-SVCOMP22, author = {A.~Coto and O.~Inverso and E.~Sales and E.~Tuosto}, title = {A Prototype for Data Race Detection in {CSeq 3} (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {413-417}, year = {2022}, series = {LNCS~13244}, publisher = {Springer}, doi = {10.1007/978-3-030-99527-0_23}, }
9. F. He, Z. Sun, and H. Fan. Deagle: An SMT-based Verifier for Multi-threaded Programs (Competition Contribution). In Proc. TACAS (2), LNCS 13244, pages 424-428, 2022. Springer. doi:10.1007/978-3-030-99527-0_25 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{DEAGLE-SVCOMP22, author = {F.~He and Z.~Sun and H.~Fan}, title = {{Deagle}: {A}n {SMT}-based Verifier for Multi-threaded Programs (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {424-428}, year = {2022}, series = {LNCS~13244}, publisher = {Springer}, doi = {10.1007/978-3-030-99527-0_25}, }
10. D. Beyer and M. Spiessl. The Static Analyzer Frama-C in SV-COMP (Competition Contribution). In Proc. TACAS (2), LNCS 13244, pages 429-434, 2022. Springer. doi:10.1007/978-3-030-99527-0_26 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{FRAMA-C-SV-SVCOMP22, author = {D.~Beyer and M.~Spiessl}, title = {The Static Analyzer {Frama-C} in {SV-COMP} (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {429-434}, year = {2022}, series = {LNCS~13244}, publisher = {Springer}, doi = {10.1007/978-3-030-99527-0_26}, }
11. M. Mues and F. Howar. GDart (Competition Contribution). In Proc. TACAS (2), LNCS 13244, pages 435-439, 2022. Springer. doi:10.1007/978-3-030-99527-0_27 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{GDART-SVCOMP22, author = {M.~Mues and F.~Howar}, title = {{GDart} (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {435-439}, year = {2022}, series = {LNCS~13244}, publisher = {Springer}, doi = {10.1007/978-3-030-99527-0_27}, }
12. W. Leeson and M. Dwyer. Graves-CPA: A Graph-Attention Verifier Selector (Competition Contribution). In Proc. TACAS (2), LNCS 13244, pages 440-445, 2022. Springer. doi:10.1007/978-3-030-99527-0_28 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{GRAVES-SVCOMP22, author = {W.~Leeson and M.~Dwyer}, title = {{Graves-CPA}: {A} Graph-Attention Verifier Selector (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {440-445}, year = {2022}, series = {LNCS~13244}, publisher = {Springer}, doi = {10.1007/978-3-030-99527-0_28}, }
13. M. Kettl and T. Lemberger. The Static Analyzer Infer in SV-COMP (Competition Contribution). In Proc. TACAS (2), LNCS 13244, pages 451-456, 2022. Springer. doi:10.1007/978-3-030-99527-0_30 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{INFER-SVCOMP22, author = {M.~Kettl and T.~Lemberger}, title = {The Static Analyzer {Infer} in {SV-COMP} (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {451-456}, year = {2022}, series = {LNCS~13244}, publisher = {Springer}, doi = {10.1007/978-3-030-99527-0_30}, }
14. H. Lauko and P. Ročkai. Lart: Compiled Abstract Execution (Competition Contribution). In Proc. TACAS (2), LNCS 13244, pages 457-461, 2022. Springer. doi:10.1007/978-3-030-99527-0_31 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{LART-SVCOMP22, author = {H.~Lauko and P.~Ročkai}, title = {{Lart}: {C}ompiled Abstract Execution (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {457-461}, year = {2022}, series = {LNCS~13244}, publisher = {Springer}, doi = {10.1007/978-3-030-99527-0_31}, }
15. M. Chalupa, A. Řechtáčková, V. Mihalkovič, L. Zaoral, and J. Strejček. Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding (Competition Contribution). In Proc. TACAS (2), LNCS 13244, pages 462-467, 2022. Springer. doi:10.1007/978-3-030-99527-0_32 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{SYMBIOTIC-SVCOMP22, author = {M.~Chalupa and A.~Řechtáčková and V.~Mihalkovič and L.~Zaoral and J.~Strejček}, title = {{Symbiotic~9}: {S}tring Analysis and Backward Symbolic Execution with Loop Folding (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {462-467}, year = {2022}, series = {LNCS~13244}, publisher = {Springer}, doi = {10.1007/978-3-030-99527-0_32}, }
16. Z. Ádám, L. Bajczi, M. Dobos-Kovács, A. Hajdu, and V. Molnár. Theta: Portfolio of CEGAR-Based Analyses with Dynamic Algorithm Selection (Competition Contribution). In Proc. TACAS (2), LNCS 13244, pages 474-478, 2022. Springer. doi:10.1007/978-3-030-99527-0_34 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{THETA-SVCOMP22, author = {Z.~Ádám and L.~Bajczi and M.~Dobos-Kovács and A.~Hajdu and V.~Molnár}, title = {{Theta}: {P}ortfolio of CEGAR-Based Analyses with Dynamic Algorithm Selection (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {474-478}, year = {2022}, series = {LNCS~13244}, publisher = {Springer}, doi = {10.1007/978-3-030-99527-0_34}, }
17. D. Klumpp, D. Dietsch, M. Heizmann, F. Schüssele, M. Ebbinghaus, A. Farzan, and A. Podelski. Ultimate GemCutter and the Axes of Generalization (Competition Contribution). In Proc. TACAS (2), LNCS 13244, pages 479-483, 2022. Springer. doi:10.1007/978-3-030-99527-0_35 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{UGEMCUTTER-SVCOMP22, author = {D.~Klumpp and D.~Dietsch and M.~Heizmann and F.~Schüssele and M.~Ebbinghaus and A.~Farzan and A.~Podelski}, title = {{Ultimate GemCutter} and the Axes of Generalization (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {479-483}, year = {2022}, series = {LNCS~13244}, publisher = {Springer}, doi = {10.1007/978-3-030-99527-0_35}, }
18. R. Scott, R. Dockins, T. Ravitch, and A. Tomb. Crux: Symbolic Execution Meets SMT-based Verification (Competition Contribution). Zenodo, February 2022. doi:10.5281/zenodo.6147218 Publisher's Version
    BibTeX Entry

    @misc{CRUX-SVCOMP22, author = {R.~Scott and R.~Dockins and T.~Ravitch and A.~Tomb}, title = {{Crux}: Symbolic Execution Meets {SMT}-based Verification (Competition Contribution)}, year = {2022}, doi = {10.5281/zenodo.6147218}, howpublished = {Zenodo}, month = {February}, }

SV-COMP 2021

1. D. Beyer. Software Verification: 10th Comparative Evaluation (SV-COMP 2021). In Proc. TACAS (2), LNCS 12652, pages 401-422, 2021. Springer. doi:10.1007/978-3-030-72013-1_24 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{SVCOMP21, author = {D.~Beyer}, title = {Software Verification: 10th Comparative Evaluation ({SV-COMP 2021})}, booktitle = {Proc.\ TACAS~(2)}, pages = {401-422}, year = {2021}, series = {LNCS~12652}, publisher = {Springer}, doi = {10.1007/978-3-030-72013-1_24}, }
2. P. Andrianov, V. Mutilin, and A. Khoroshilov. CPALockator: Thread-Modular Approach with Projections (Competition Contribution). In Proc. TACAS (2), LNCS 12652, pages 423-427, 2021. Springer. doi:10.1007/978-3-030-72013-1_25 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{CPALOCKATOR-SVCOMP21, author = {P.~Andrianov and V.~Mutilin and A.~Khoroshilov}, title = {{CPALockator}: {T}hread-Modular Approach with Projections (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {423-427}, year = {2021}, series = {LNCS~12652}, publisher = {Springer}, doi = {10.1007/978-3-030-72013-1_25}, }
3. H. Ponce-De-Leon, T. Haas, and R. Meyer. Dartagnan: Leveraging Compiler Optimizations and the Price of Precision (Competition Contribution). In Proc. TACAS (2), LNCS 12652, pages 428-432, 2021. Springer. doi:10.1007/978-3-030-72013-1_26 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{DARTAGNAN-SVCOMP21, author = {H.~Ponce-De-Leon and T.~Haas and R.~Meyer}, title = {{Dartagnan}: {L}everaging Compiler Optimizations and the Price of Precision (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {428-432}, year = {2021}, series = {LNCS~12652}, publisher = {Springer}, doi = {10.1007/978-3-030-72013-1_26}, }
4. e̊lax Zs. Ádám, ̊ax Gy. Sallai, and Á. Hajdu. Gazer-Theta: LLVM-Based Verifier Portfolio with BMC/CEGAR (Competition Contribution). In Proc. TACAS (2), LNCS 12652, pages 433-437, 2021. Springer. doi:10.1007/978-3-030-72013-1_27 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{GAZERTHETA-SVCOMP21, author = {{\relax Zs}.~{\'A}dám and {\relax Gy}.~Sallai and {\'A}.~Hajdu}, title = {{Gazer-Theta}: {LLVM}-Based Verifier Portfolio with {BMC/CEGAR} (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {433-437}, year = {2021}, series = {LNCS~12652}, publisher = {Springer}, doi = {10.1007/978-3-030-72013-1_27}, }
5. S. Saan, M. Schwarz, K. Apinis, J. Erhard, H. Seidl, R. Vogler, and V. Vojdani. Goblint: Thread-Modular Abstract Interpretation Using Side-Effecting Constraints (Competition Contribution). In Proc. TACAS (2), LNCS 12652, pages 438-442, 2021. Springer. doi:10.1007/978-3-030-72013-1_28 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{GOBLINT-SVCOMP21, author = {S.~Saan and M.~Schwarz and K.~Apinis and J.~Erhard and H.~Seidl and R.~Vogler and V.~Vojdani}, title = {{Goblint}: {T}hread-Modular Abstract Interpretation Using Side-Effecting Constraints (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {438-442}, year = {2021}, series = {LNCS~12652}, publisher = {Springer}, doi = {10.1007/978-3-030-72013-1_28}, }
6. A. Shamakhi, H. Hojjat, and P. Rümmer. Towards String Support in JayHorn (Competition Contribution). In Proc. TACAS (2), LNCS 12652, pages 443-447, 2021. Springer. doi:10.1007/978-3-030-72013-1_29 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{JAYHORN-SVCOMP21, author = {A.~Shamakhi and H.~Hojjat and P.~Rümmer}, title = {Towards String Support in {JayHorn} (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {443-447}, year = {2021}, series = {LNCS~12652}, publisher = {Springer}, doi = {10.1007/978-3-030-72013-1_29}, }
7. M. Mues and F. Howar. JDart: Portfolio Solving, Breadth-First Search and SMT-Lib Strings (Competition Contribution). In Proc. TACAS (2), LNCS 12652, pages 448-452, 2021. Springer. doi:10.1007/978-3-030-72013-1_30 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{JDART-SVCOMP21, author = {M.~Mues and F.~Howar}, title = {{JDart}: {P}ortfolio Solving, Breadth-First Search and {SMT-Lib} Strings (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {448-452}, year = {2021}, series = {LNCS~12652}, publisher = {Springer}, doi = {10.1007/978-3-030-72013-1_30}, }
8. M. Chalupa, T. Jašek, J. Novák, A. Řechtáčková, V. Šoková, and J. Strejček. Symbiotic 8: Beyond Symbolic Execution (Competition Contribution). In Proc. TACAS (2), LNCS 12652, pages 453-457, 2021. Springer. doi:10.1007/978-3-030-72013-1_31 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{SYMBIOTIC-SVCOMP21, author = {M.~Chalupa and T.~Jašek and J.~Novák and A.~Řechtáčková and V.~Šoková and J.~Strejček}, title = {{Symbiotic 8}: {B}eyond Symbolic Execution (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {453-457}, year = {2021}, series = {LNCS~12652}, publisher = {Springer}, doi = {10.1007/978-3-030-72013-1_31}, }
9. P. Darke, S. Agrawal, and R. Venkatesh. VeriAbs: A Tool for Scalable Verification by Abstraction (Competition Contribution). In Proc. TACAS (2), LNCS 12652, pages 458-462, 2021. Springer. doi:10.1007/978-3-030-72013-1_32 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{VERIABS-SVCOMP21, author = {P.~Darke and S.~Agrawal and R.~Venkatesh}, title = {{VeriAbs}: {A} Tool for Scalable Verification by Abstraction (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {458-462}, year = {2021}, series = {LNCS~12652}, publisher = {Springer}, doi = {10.1007/978-3-030-72013-1_32}, }

SV-COMP 2020

1. D. Beyer. Advances in Automatic Software Verification: SV-COMP 2020. In Proc. TACAS (2), LNCS 12079, pages 347-367, 2020. Springer. doi:10.1007/978-3-030-45237-7_21 Publisher's Version PDF Supplement
   BibTeX Entry

   @inproceedings{SVCOMP20, author = {D.~Beyer}, title = {Advances in Automatic Software Verification: {SV-COMP 2020}}, booktitle = {Proc.\ TACAS~(2)}, pages = {347-367}, year = {2020}, series = {LNCS~12079}, publisher = {Springer}, doi = {10.1007/978-3-030-45237-7_21}, url = {https://www.sosy-lab.org/research/pub/2020-TACAS.Advances_in_Automatic_Software_Verification_SV-COMP_2020.pdf}, }
2. V. Malík, P. Schrammel, and T. Vojnar. 2ls: Heap Analysis and Memory Safety (Competition Contribution). In Proc. TACAS (2), LNCS 12079, pages 368-372, 2020. Springer. doi:10.1007/978-3-030-45237-7_22 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{2LS-SVCOMP20, author = {V.~Malík and P.~Schrammel and T.~Vojnar}, title = {{2ls}: Heap Analysis and Memory Safety (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {368-372}, year = {2020}, series = {LNCS~12079}, publisher = {Springer}, doi = {10.1007/978-3-030-45237-7_22}, }
3. W. Visser and J. Geldenhuys. Coastal: Combining Concolic and Fuzzing for Java (Competition Contribution). In Proc. TACAS (2), LNCS 12079, pages 373-377, 2020. Springer. doi:10.1007/978-3-030-45237-7_23 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{COASTAL-SVCOMP20, author = {W.~Visser and J.~Geldenhuys}, title = {{Coastal}: Combining Concolic and Fuzzing for {Java} (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {373-377}, year = {2020}, series = {LNCS~12079}, publisher = {Springer}, doi = {10.1007/978-3-030-45237-7_23}, }
4. H. Ponce-de-Leon, F. Furbach, K. Heljanko, and R. Meyer. Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution). In Proc. TACAS (2), LNCS 12079, pages 378-382, 2020. Springer. doi:10.1007/978-3-030-45237-7_24 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{DARTAGNAN-SVCOMP20, author = {H.~Ponce-de-Leon and F.~Furbach and K.~Heljanko and R.~Meyer}, title = {{Dartagnan}: Bounded Model Checking for Weak Memory Models (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {378-382}, year = {2020}, series = {LNCS~12079}, publisher = {Springer}, doi = {10.1007/978-3-030-45237-7_24}, }
5. B. Quiring and P. Manolios. Gacal: Conjecture-Based Verification (Competition Contribution). In Proc. TACAS (2), LNCS 12079, pages 388-392, 2020. Springer. doi:10.1007/978-3-030-45237-7_26 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{GACAL-SVCOMP20, author = {B.~Quiring and P.~Manolios}, title = {{Gacal}: Conjecture-Based Verification (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {388-392}, year = {2020}, series = {LNCS~12079}, publisher = {Springer}, doi = {10.1007/978-3-030-45237-7_26}, }
6. V. Sharma, S. Hussein, M. W. Whalen, S. A. McCamant, and W. Visser. Java Ranger at SV-COMP 2020 (Competition Contribution). In Proc. TACAS (2), LNCS 12079, pages 393-397, 2020. Springer. doi:10.1007/978-3-030-45237-7_27 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{JAVARANGER-SVCOMP20, author = {V.~Sharma and S.~Hussein and M.~W.~Whalen and S.~A.~McCamant and W.~Visser}, title = {{Java Ranger} at {SV-COMP 2020} (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {393-397}, year = {2020}, series = {LNCS~12079}, publisher = {Springer}, doi = {10.1007/978-3-030-45237-7_27}, }
7. M. Mues and F. Howar. JDart: Dynamic Symbolic Execution for Java Bytecode (Competition Contribution). In Proc. TACAS (2), LNCS 12079, pages 398-402, 2020. Springer. doi:10.1007/978-3-030-45237-7_28 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{JDART-SVCOMP20, author = {M.~Mues and F.~Howar}, title = {{JDart}: Dynamic Symbolic Execution for {Java} Bytecode (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {398-402}, year = {2020}, series = {LNCS~12079}, publisher = {Springer}, doi = {10.1007/978-3-030-45237-7_28}, }
8. H. O. Rocha, R. Menezes, L. Cordeiro, and R. Barreto. Map2Check: Using Symbolic Execution and Fuzzing (Competition Contribution). In Proc. TACAS (2), LNCS 12079, pages 403-407, 2020. Springer. doi:10.1007/978-3-030-45237-7_29 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{MAP2CHECK-SVCOMP20, author = {H.~O.~Rocha and R.~Menezes and L.~Cordeiro and R.~Barreto}, title = {{Map2Check}: Using Symbolic Execution and Fuzzing (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {403-407}, year = {2020}, series = {LNCS~12079}, publisher = {Springer}, doi = {10.1007/978-3-030-45237-7_29}, }
9. P. Peringer, V. Šoková, and T. Vojnar. PredatorHP Revamped (Not Only) for Interval-Sized Memory Regions and Memory Reallocation (Competition Contribution). In Proc. TACAS (2), LNCS 12079, pages 408-412, 2020. Springer. doi:10.1007/978-3-030-45237-7_30 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{PREDATORHP-SVCOMP20, author = {P.~Peringer and V.~Šoková and T.~Vojnar}, title = {{PredatorHP} Revamped (Not Only) for Interval-Sized Memory Regions and Memory Reallocation (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {408-412}, year = {2020}, series = {LNCS~12079}, publisher = {Springer}, doi = {10.1007/978-3-030-45237-7_30}, }
10. M. Chalupa, T. Jašek, L. Tomovič, M. Hruška, V. Šoková, P. Ayaziová, J. Strejček, and T. Vojnar. Symbiotic 7: Integration of Predator and More (Competition Contribution). In Proc. TACAS (2), LNCS 12079, pages 413-417, 2020. Springer. doi:10.1007/978-3-030-45237-7_31 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{SYMBIOTIC-SVCOMP20, author = {M.~Chalupa and T.~Jašek and L.~Tomovič and M.~Hruška and V.~Šoková and P.~Ayaziová and J.~Strejček and T.~Vojnar}, title = {{Symbiotic 7}: Integration of {Predator} and More (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {413-417}, year = {2020}, series = {LNCS~12079}, publisher = {Springer}, doi = {10.1007/978-3-030-45237-7_31}, }
11. D. Dietsch, M. Heizmann, A. Nutz, C. Schätzle, and F. Schüssele. Ultimate Taipan with Symbolic Interpretation and Fluid Abstractions (Competition Contribution). In Proc. TACAS (2), LNCS 12079, pages 418-422, 2020. Springer. doi:10.1007/978-3-030-45237-7_32 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{UTAIPAN-SVCOMP20, author = {D.~Dietsch and M.~Heizmann and A.~Nutz and C.~Schätzle and F.~Schüssele}, title = {{Ultimate Taipan} with Symbolic Interpretation and Fluid Abstractions (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {418-422}, year = {2020}, series = {LNCS~12079}, publisher = {Springer}, doi = {10.1007/978-3-030-45237-7_32}, }
12. M. Afzal, S. Chakraborty, A. Chauhan, B. Chimdyalwar, P. Darke, A. Gupta, S. Kumar, Charles B. M., D. Unadkat, and R. Venkatesh. VeriAbs: Verification by Abstraction and Test Generation (Competition Contribution). In Proc. TACAS (2), LNCS 12079, pages 383-387, 2020. Springer. doi:10.1007/978-3-030-45237-7_25 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{VERIABS-SVCOMP20, author = {M.~Afzal and S.~Chakraborty and A.~Chauhan and B.~Chimdyalwar and P.~Darke and A.~Gupta and S.~Kumar and Charles~B.~M. and D.~Unadkat and R.~Venkatesh}, title = {{VeriAbs}: Verification by Abstraction and Test Generation (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {383-387}, year = {2020}, series = {LNCS~12079}, publisher = {Springer}, doi = {10.1007/978-3-030-45237-7_25}, }

SV-COMP 2019

1. D. Beyer. Automatic Verification of C and Java Programs: SV-COMP 2019. In Proc. TACAS (3), LNCS 11429, pages 133-155, 2019. Springer. doi:10.1007/978-3-030-17502-3_9 Publisher's Version PDF Supplement
   BibTeX Entry

   @inproceedings{SVCOMP19, author = {D.~Beyer}, title = {Automatic Verification of {C} and {Java} Programs: {SV-COMP} 2019}, booktitle = {Proc.\ TACAS~(3)}, pages = {133-155}, year = {2019}, series = {LNCS~11429}, publisher = {Springer}, doi = {10.1007/978-3-030-17502-3_9}, url = {https://www.sosy-lab.org/research/pub/2019-TACAS.Automatic_Verification_of_C_and_Java_Programs_SV-COMP_2019.pdf}, }
2. K. Khazem and M. Tautschnig. Cbmc Path: A Symbolic Execution Retrofit of the C Bounded Model Checker (Competition Contribution). In Proc. TACAS (3), LNCS 11429, pages 199-203, 2019. Springer. doi:10.1007/978-3-030-17502-3_13 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{CBMCPATH-SVCOMP19, author = {K.~Khazem and M.~Tautschnig}, title = {{Cbmc Path}: A Symbolic Execution Retrofit of the {C} Bounded Model Checker (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {199-203}, year = {2019}, series = {LNCS~11429}, publisher = {Springer}, doi = {10.1007/978-3-030-17502-3_13}, }
3. E. Chaudhary and S. Joshi. Pinaka: Symbolic Execution meets Incremental Solving (Competition Contribution). In Proc. TACAS (3), LNCS 11429, pages 234-238, 2019. Springer. doi:10.1007/978-3-030-17502-3_20 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{PINAKA-SVCOMP19, author = {E.~Chaudhary and S.~Joshi}, title = {{Pinaka}: Symbolic Execution meets Incremental Solving (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {234-238}, year = {2019}, series = {LNCS~11429}, publisher = {Springer}, doi = {10.1007/978-3-030-17502-3_20}, isbnnote = {978-3-030-17501-6}, }
4. C. Richter and H. Wehrheim. PeSCo: Predicting Sequential Combinations of Verifiers (Competition Contribution). In Proc. TACAS (3), LNCS 11429, pages 229-233, 2019. Springer. doi:10.1007/978-3-030-17502-3_19 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{PESCO-SVCOMP19, author = {C.~Richter and H.~Wehrheim}, title = {{PeSCo}: Predicting Sequential Combinations of Verifiers (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {229-233}, year = {2019}, series = {LNCS~11429}, publisher = {Springer}, doi = {10.1007/978-3-030-17502-3_19}, }
5. Y. Noller, C. S. Păsăreanu, X.-B. D. Le, W. Visser, and A. Fromherz. Symbolic Pathfinder for SV-COMP (Competition Contribution). In Proc. TACAS (3), LNCS 11429, pages 239-243, 2019. Springer. doi:10.1007/978-3-030-17502-3_21 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{SPF-SVCOMP19, author = {Y.~Noller and C.~S.~Păsăreanu and X.-B.~D.~Le and W.~Visser and A.~Fromherz}, title = {Symbolic {Pathfinder} for {SV-COMP} (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {239-243}, year = {2019}, series = {LNCS~11429}, publisher = {Springer}, doi = {10.1007/978-3-030-17502-3_21}, isbnnote = {978-3-030-17501-6}, }
6. C. Artho and W. Visser. Java Pathfinder at SV-COMP 2019 (Competition Contribution). In Proc. TACAS (3), LNCS 11429, pages 224-228, 2019. Springer. doi:10.1007/978-3-030-17502-3_18 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{JPF-SVCOMP19, author = {C.~Artho and W.~Visser}, title = {{Java Pathfinder} at {SV-COMP} 2019 (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {224-228}, year = {2019}, series = {LNCS~11429}, publisher = {Springer}, doi = {10.1007/978-3-030-17502-3_18}, }
7. M. Y. R. Gadelha, F. R. Monteiro, L. C. Cordeiro, and D. A. Nicole. Esbmc v6.0: Verifying C Programs using and Invariant Inference (Competition Contribution). In Proc. TACAS (3), LNCS 11429, pages 209-213, 2019. Springer. doi:10.1007/978-3-030-17502-3_15 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{ESBMCKIND-SVCOMP19, author = {M.~Y.~R.~Gadelha and F.~R.~Monteiro and L.~C.~Cordeiro and D.~A.~Nicole}, title = {{Esbmc} v6.0: Verifying {C} Programs using \textit{k}-Induction and Invariant Inference (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {209-213}, year = {2019}, series = {LNCS~11429}, publisher = {Springer}, doi = {10.1007/978-3-030-17502-3_15}, }
8. L. C. Cordeiro, D. Kröning, and P. Schrammel. Jbmc: Bounded Model Checking for Java Bytecode (Competition Contribution). In Proc. TACAS (3), LNCS 11429, pages 219-223, 2019. Springer. doi:10.1007/978-3-030-17502-3_17 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{JBMC-SVCOMP19, author = {L.~C.~Cordeiro and D.~Kröning and P.~Schrammel}, title = {{Jbmc}: Bounded Model Checking for {Java} Bytecode (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {219-223}, year = {2019}, series = {LNCS~11429}, publisher = {Springer}, doi = {10.1007/978-3-030-17502-3_17}, isbnnote = {978-3-030-17501-6}, }
9. A. B. Chowdhury, R. K. Medicherla, and R. Venkatesh. VeriFuzz: Program-Aware Fuzzing (Competition Contribution). In Proc. TACAS (3), LNCS 11429, pages 244-249, 2019. Springer. doi:10.1007/978-3-030-17502-3_22 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{VERIFUZZ-SVCOMP19, author = {A.~B.~Chowdhury and R.~K.~Medicherla and R.~Venkatesh}, title = {{VeriFuzz}: Program-Aware Fuzzing (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {244-249}, year = {2019}, series = {LNCS~11429}, publisher = {Springer}, doi = {10.1007/978-3-030-17502-3_22}, }
10. T. Kahsai, P. Rümmer, and M. Schäf. JayHorn: A Java Model Checker (Competition Contribution). In Proc. TACAS (3), LNCS 11429, pages 214-218, 2019. Springer. doi:10.1007/978-3-030-17502-3_16 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{JAYHORN-SVCOMP19, author = {T.~Kahsai and P.~Rümmer and M.~Schäf}, title = {{JayHorn}: A {Java} Model Checker (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {214-218}, year = {2019}, series = {LNCS~11429}, publisher = {Springer}, doi = {10.1007/978-3-030-17502-3_16}, isbnnote = {978-3-030-17501-6}, }
11. P. Rajkhowa and F. Lin. Viap 1.1 (Competition Contribution). In Proc. TACAS (3), LNCS 11429, pages 250-255, 2019. Springer. doi:10.1007/978-3-030-17502-3_23 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{VIAP-SVCOMP19, author = {P.~Rajkhowa and F.~Lin}, title = {{Viap} 1.1 (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {250-255}, year = {2019}, series = {LNCS~11429}, publisher = {Springer}, doi = {10.1007/978-3-030-17502-3_23}, }
12. H. Lauko, V. Štill, P. Ročkai, and J. Barnat. Extending Divine with Symbolic Verification using SMT (Competition Contribution). In Proc. TACAS (3), LNCS 11429, pages 204-208, 2019. Springer. doi:10.1007/978-3-030-17502-3_14 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{DIVINESMT-SVCOMP19, author = {H.~Lauko and V.~Štill and P.~Ročkai and J.~Barnat}, title = {Extending {Divine} with Symbolic Verification using {SMT} (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {204-208}, year = {2019}, series = {LNCS~11429}, publisher = {Springer}, doi = {10.1007/978-3-030-17502-3_14}, }

SV-COMP 2018

1. M. Chalupa, M. Vitovská, and J. Strejček. Symbiotic 5: Boosted Instrumentation (Competition Contribution). In Proc. TACAS, LNCS 10806, pages 442-446, 2018. Springer. doi:10.1007/978-3-319-89963-3_29 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{SYMBIOTIC5-SVCOMP18, author = {M.~Chalupa and M.~Vitovsk{\'{a}} and J.~Strejček}, title = {{Symbiotic} 5: Boosted Instrumentation (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {442-446}, year = {2018}, series = {LNCS~10806}, publisher = {Springer}, doi = {10.1007/978-3-319-89963-3_29}, }
2. M. Heizmann, Y.-F. Chen, D. Dietsch, M. Greitschus, J. Hoenicke, Y. Li, A. Nutz, B. Musa, C. Schilling, T. Schindler, and A. Podelski. Ultimate Automizer and the Search for Perfect Interpolants (Competition Contribution). In Proc. TACAS (2), LNCS 10806, pages 447-451, 2018. Springer. doi:10.1007/978-3-319-89963-3_30 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{UAUTOMIZER-COMP18, author = {M.~Heizmann and Y.-F.~Chen and D.~Dietsch and M.~Greitschus and J.~Hoenicke and Y.~Li and A.~Nutz and B.~Musa and C.~Schilling and T.~Schindler and A.~Podelski}, title = {{Ultimate Automizer} and the Search for Perfect Interpolants (Competition Contribution)}, booktitle = {Proc.\ TACAS~(2)}, pages = {447-451}, year = {2018}, series = {LNCS~10806}, publisher = {Springer}, doi = {10.1007/978-3-319-89963-3_30}, }
3. L. Yin, W. Dong, W. Liu, Y. Li, and J. Wang. Yogar-Cbmc: Cbmc with Scheduling Constraint Based Abstraction Refinement (Competition Contribution). In Proc. TACAS, LNCS 10806, pages 422-426, 2018. Springer. doi:10.1007/978-3-319-89963-3_25 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{YOGARCBMC-SVCOMP18, author = {L.~Yin and W.~Dong and W.~Liu and Y.~Li and J.~Wang}, title = {{Yogar-Cbmc:} {Cbmc} with Scheduling Constraint Based Abstraction Refinement (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {422--426}, year = {2018}, series = {LNCS~10806}, publisher = {Springer}, doi = {10.1007/978-3-319-89963-3_25}, isbnnote = {978-3-319-89962-6}, }
4. P. Darke, S. Prabhu, B. Chimdyalwar, A. Chauhan, S. Kumar, A. Basak Chowdhury, R. Venkatesh, A. Datar, and M. R. Kumar. VeriAbs: Verification by Abstraction and Test Generation (Competition Contribution). In Proc. TACAS, LNCS 10806, pages 457-462, 2018. Springer. doi:10.1007/978-3-319-89963-3_32 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{VERIABS-SVCOMP18, author = {P.~Darke and S.~Prabhu and B.~Chimdyalwar and A.~Chauhan and S.~Kumar and A.~Basak Chowdhury and R.~Venkatesh and A.~Datar and M.~R.~Kumar}, title = {{VeriAbs}: Verification by Abstraction and Test Generation (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {457--462}, year = {2018}, series = {LNCS~10806}, publisher = {Springer}, doi = {10.1007/978-3-319-89963-3_32}, isbnnote = {978-3-319-89962-6}, }

SV-COMP 2017

1. D. Beyer. Software Verification with Validation of Results (Report on SV-COMP 2017). In Proc. TACAS, LNCS 10206, pages 331-349, 2017. Springer. doi:10.1007/978-3-662-54580-5_20 Publisher's Version PDF Supplement
   BibTeX Entry

   @inproceedings{SVCOMP17, author = {D.~Beyer}, title = {Software Verification with Validation of Results ({R}eport on {SV-COMP} 2017)}, booktitle = {Proc.\ TACAS}, pages = {331-349}, year = {2017}, series = {LNCS~10206}, publisher = {Springer}, doi = {10.1007/978-3-662-54580-5_20}, url = {https://www.sosy-lab.org/~dbeyer/Publications/2017-TACAS.Software_Verification_with_Validation_of_Results.pdf}, }
2. P. Andrianov, K. Friedberger, M. U. Mandrykin, V. S. Mutilin, and A. Volkov. CPA-BAM-BnB: Block-Abstraction Memoization and Region-Based Memory Models for Predicate Abstractions (Competition Contribution). In Proc. TACAS, LNCS 10206, pages 355-359, 2017. Springer. doi:10.1007/978-3-662-54580-5_22 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{CPABAM-SVCOMP17, author = {P.~Andrianov and K.~Friedberger and M.~U.~Mandrykin and V.~S.~Mutilin and A.~Volkov}, title = {{CPA-BAM-BnB}: {Block}-Abstraction Memoization and Region-Based Memory Models for Predicate Abstractions (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {355-359}, year = {2017}, series = {LNCS~10206}, publisher = {Springer}, doi = {10.1007/978-3-662-54580-5_22}, }
3. F. Cassez, A. M. Sloane, M. Roberts, M. Pigram, P. Suvanpong, and P. González de Aledo Marugán. Skink: Static Analysis of Programs in LLVM Intermediate Representation (Competition Contribution). In Proc. TACAS, LNCS 10206, pages 380-384, 2017. Springer. doi:10.1007/978-3-662-54580-5_27 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{SKINK-SVCOMP17, author = {F.~Cassez and A.~M.~Sloane and M.~Roberts and M.~Pigram and P.~Suvanpong and P.~Gonz{\'{a}}lez de Aledo Marug{\'{a}}n}, title = {{Skink}: {Static} Analysis of Programs in {LLVM} Intermediate Representation (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {380-384}, year = {2017}, series = {LNCS~10206}, publisher = {Springer}, doi = {10.1007/978-3-662-54580-5_27}, }
4. M. Chalupa, M. Vitovská, M. Jonáš, J. Slaby, and J. Strejček. Symbiotic 4: Beyond Reachability (Competition Contribution). In Proc. TACAS, LNCS 10206, pages 385-389, 2017. Springer. doi:10.1007/978-3-662-54580-5_28 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{SYMBIOTIC-SVCOMP17, author = {M.~Chalupa and M.~Vitovsk{\'{a}} and M.~Jon{\'{a}}{\v{s}} and J.~Slaby and J.~Strejček}, title = {{Symbiotic} 4: {Beyond} Reachability (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {385-389}, year = {2017}, series = {LNCS~10206}, publisher = {Springer}, doi = {10.1007/978-3-662-54580-5_28}, }
5. B. Chimdyalwar, P. Darke, A. Chauhan, P. Shah, S. Kumar, and R. Venkatesh. VeriAbs: Verification by Abstraction (Competition Contribution). In Proc. TACAS, LNCS 10206, pages 404-408, 2017. Springer. doi:10.1007/978-3-662-54580-5_32 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{VERIABS-SVCOMP17, author = {B.~Chimdyalwar and P.~Darke and A.~Chauhan and P.~Shah and S.~Kumar and R.~Venkatesh}, title = {{VeriAbs}: {Verification} by Abstraction (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {404-408}, year = {2017}, series = {LNCS~10206}, publisher = {Springer}, doi = {10.1007/978-3-662-54580-5_32}, }
6. M. Greitschus, D. Dietsch, M. Heizmann, A. Nutz, C. Schätzle, C. Schilling, F. Schüssele, and A. Podelski. Ultimate Taipan: Trace Abstraction and Abstract Interpretation (Competition Contribution). In Proc. TACAS, LNCS 10206, pages 399-403, 2017. Springer. doi:10.1007/978-3-662-54580-5_31 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{UTAIPAN-SVCOMP17, author = {M.~Greitschus and D.~Dietsch and M.~Heizmann and A.~Nutz and C.~Sch{\"{a}}tzle and C.~Schilling and F.~Sch{\"{u}}ssele and A.~Podelski}, title = {{Ultimate Taipan}: {Trace} Abstraction and Abstract Interpretation (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {399-403}, year = {2017}, series = {LNCS~10206}, publisher = {Springer}, doi = {10.1007/978-3-662-54580-5_31}, }
7. M. Heizmann, Y.-W. Chen, D. Dietsch, M. Greitschus, A. Nutz, B. Musa, C. Schätzle, C. Schilling, F. Schüssele, and A. Podelski. Ultimate Automizer with an On-Demand Construction of Floyd-Hoare Automata (Competition Contribution). In Proc. TACAS, LNCS 10206, pages 394-398, 2017. Springer. doi:10.1007/978-3-662-54580-5_30 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{UAUTOMIZER-SVCOMP17, author = {M.~Heizmann and Y.-W.~Chen and D.~Dietsch and M.~Greitschus and A.~Nutz and B.~Musa and C.~Sch{\"{a}}tzle and C.~Schilling and F.~Sch{\"{u}}ssele and A.~Podelski}, title = {{Ultimate Automizer} with an On-Demand Construction of {Floyd}-{Hoare} Automata (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {394-398}, year = {2017}, series = {LNCS~10206}, publisher = {Springer}, doi = {10.1007/978-3-662-54580-5_30}, }
8. J. Hensel, F. Emrich, F. Frohn, T. Ströder, and J. Giesl. AProVE: Proving and Disproving Termination of Memory-Manipulating C Programs (Competition Contribution). In Proc. TACAS, LNCS 10206, pages 350-354, 2017. Springer. doi:10.1007/978-3-662-54580-5_21 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{APROVE-SVCOMP17, author = {J.~Hensel and F.~Emrich and F.~Frohn and T.~Ströder and J.~Giesl}, title = {{AProVE}: {Proving} and Disproving Termination of Memory-Manipulating {C} Programs (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {350-354}, year = {2017}, series = {LNCS~10206}, publisher = {Springer}, doi = {10.1007/978-3-662-54580-5_21}, }
9. L. Holík, M. Hruška, O. Lengál, A. Rogalewicz, J. Simácek, and T. Vojnar. Forester: From Heap Shapes to Automata Predicates (Competition Contribution). In Proc. TACAS, LNCS 10206, pages 365-369, 2017. Springer. doi:10.1007/978-3-662-54580-5_24 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{FORESTER-SVCOMP17, author = {L.~Hol{\'{\i}}k and M.~Hruška and O.~Leng{\'{a}}l and A.~Rogalewicz and J.~Sim{\'{a}}cek and T.~Vojnar}, title = {{Forester}: {From} Heap Shapes to Automata Predicates (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {365-369}, year = {2017}, series = {LNCS~10206}, publisher = {Springer}, doi = {10.1007/978-3-662-54580-5_24}, }
10. T. Chanh Le, Q.-T. Ta, and W.-N. Chin. HipTNT+: A Termination and Non-termination Analyzer by Second-Order Abduction (Competition Contribution). In Proc. TACAS, LNCS 10206, pages 370-374, 2017. Springer. doi:10.1007/978-3-662-54580-5_25 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{HIPTNT-SVCOMP17, author = {T.~Chanh Le and Q.-T.~Ta and W.-N.~Chin}, title = {{HipTNT+}: {A} Termination and Non-termination Analyzer by Second-Order Abduction (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {370-374}, year = {2017}, series = {LNCS~10206}, publisher = {Springer}, doi = {10.1007/978-3-662-54580-5_25}, }
11. J. Mrázek, M. Jonáš, V. Still, H. Lauko, and J. Barnat. Optimizing and Caching SMT Queries in SymDivine (Competition Contribution). In Proc. TACAS, LNCS 10206, pages 390-393, 2017. Springer. doi:10.1007/978-3-662-54580-5_29 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{SYMDIVINE-SVCOMP17, author = {J.~Mr{\'{a}}zek and M.~Jon{\'{a}}{\v{s}} and V.~Still and H.~Lauko and J.~Barnat}, title = {Optimizing and Caching {SMT} Queries in {SymDivine} (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {390-393}, year = {2017}, series = {LNCS~10206}, publisher = {Springer}, doi = {10.1007/978-3-662-54580-5_29}, }
12. T. L. Nguyen, O. Inverso, B. Fischer, S. La Torre, and G. Parlato. Lazy-CSeq 2.0: Combining Lazy Sequentialization with Abstract Interpretation (Competition Contribution). In Proc. TACAS, LNCS 10206, pages 375-379, 2017. Springer. doi:10.1007/978-3-662-54580-5_26 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{LAZYCSEQ-SVCOMP17, author = {T.~L.~Nguyen and O.~Inverso and B.~Fischer and S.~La~Torre and G.~Parlato}, title = {{Lazy-CSeq} 2.0: {Combining} Lazy Sequentialization with Abstract Interpretation (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {375-379}, year = {2017}, series = {LNCS~10206}, publisher = {Springer}, doi = {10.1007/978-3-662-54580-5_26}, }
13. W. Rocha, H. O. Rocha, H. Ismail, L C. Cordeiro, and B. Fischer. DepthK: A Verifier Based on Invariant Inference for C Programs (Competition Contribution). In Proc. TACAS, LNCS 10206, pages 360-364, 2017. Springer. doi:10.1007/978-3-662-54580-5_23 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{DEPTHK-SVCOMP17, author = {W.~Rocha and H.~O.~Rocha and H.~Ismail and L~C.~Cordeiro and B.~Fischer}, title = {{DepthK}: {A} \textit{k}-Induction Verifier Based on Invariant Inference for {C} Programs (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {360-364}, year = {2017}, series = {LNCS~10206}, publisher = {Springer}, doi = {10.1007/978-3-662-54580-5_23}, }

SV-COMP 2016

1. D. Beyer. Reliable and Reproducible Competition Results with BenchExec and Witnesses (Report on SV-COMP 2016). In Proc. TACAS, LNCS 9636, pages 887-904, 2016. Springer. doi:10.1007/978-3-662-49674-9_55 Publisher's Version PDF Supplement
   BibTeX Entry

   @inproceedings{SVCOMP16, author = {D.~Beyer}, title = {Reliable and Reproducible Competition Results with {BenchExec} and Witnesses ({R}eport on {SV-COMP} 2016)}, booktitle = {Proc.\ TACAS}, pages = {887-904}, year = {2016}, series = {LNCS~9636}, publisher = {Springer}, doi = {10.1007/978-3-662-49674-9_55}, url = {https://www.sosy-lab.org/research/pub/2016-TACAS.Reliable_and_Reproducible_Competition_Results_with_BenchExec_and_Witnesses.pdf}, isbnnote = {978-3-662-49674-9}, }
2. L. Holík, M. Hruška, O. Lengál, A. Rogalewicz, J. Simácek, and T. Vojnar. Run Forester, Run Backwards! (Competition Contribution). In Proc. TACAS, LNCS 9636, pages 923-926, 2016. Springer. doi:10.1007/978-3-662-49674-9_61 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{FORESTER-SVCOMP16, author = {L.~Hol{\'{\i}}k and M.~Hruška and O.~Leng{\'{a}}l and A.~Rogalewicz and J.~Sim{\'{a}}cek and T.~Vojnar}, title = {Run {Forester}, Run Backwards! (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {923-926}, year = {2016}, series = {LNCS~9636}, publisher = {Springer}, doi = {10.1007/978-3-662-49674-9_61}, }
3. M. Kotoun, P. Peringer, V. Šoková, and T. Vojnar. Optimized PredatorHP and the SV-COMP Heap and Memory Safety Benchmark (Competition Contribution). In Proc. TACAS, LNCS 9636, pages 942-945, 2016. Springer. doi:10.1007/978-3-662-49674-9_66 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{PREDATOR-SVCOMP16, author = {M.~Kotoun and P.~Peringer and V.~{\v{S}}okov{\'{a}} and T.~Vojnar}, title = {Optimized {PredatorHP} and the {SV-COMP} Heap and Memory Safety Benchmark (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {942-945}, year = {2016}, series = {LNCS~9636}, publisher = {Springer}, doi = {10.1007/978-3-662-49674-9_66}, }
4. M. Chalupa, M. Jonáš, J. Slaby, J. Strejček, and M. Vitovská. Symbiotic 3: New Slicer and Error-Witness Generation (Competition Contribution). In Proc. TACAS, LNCS 9636, pages 946-949, 2016. Springer. doi:10.1007/978-3-662-49674-9_67 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{SYMBIOTIC-SVCOMP16, author = {M.~Chalupa and M.~Jon{\'{a}}{\v{s}} and J.~Slaby and J.~Strejček and M.~Vitovsk{\'{a}}}, title = {{Symbiotic 3}: New Slicer and Error-Witness Generation (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {946-949}, year = {2016}, series = {LNCS~9636}, publisher = {Springer}, doi = {10.1007/978-3-662-49674-9_67}, }
5. H. O. Rocha, R. Barreto, and L. C. Cordeiro. Hunting Memory Bugs in C Programs with Map2Check (Competition Contribution). In Proc. TACAS, LNCS 9636, pages 934-937, 2016. Springer. doi:10.1007/978-3-662-49674-9_64 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{MAP2CHECK-SVCOMP16, author = {H.~O.~Rocha and R.~Barreto and L.~C.~Cordeiro}, title = {Hunting Memory Bugs in {C} Programs with {Map2Check} (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {934-937}, year = {2016}, series = {LNCS~9636}, publisher = {Springer}, doi = {10.1007/978-3-662-49674-9_64}, }
6. H. Günther, A. Laarman, and G. Weissenbacher. Vienna Verification Tool: IC3 for Parallel Software (Competition Contribution). In Proc. TACAS, LNCS 9636, pages 954-957, 2016. Springer. doi:10.1007/978-3-662-49674-9_69 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{VVT-SVCOMP16, author = {H.~Günther and A.~Laarman and G.~Weissenbacher}, title = {{Vienna Verification Tool}: {IC3} for Parallel Software (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {954-957}, year = {2016}, series = {LNCS~9636}, publisher = {Springer}, doi = {10.1007/978-3-662-49674-9_69}, }
7. P. Schrammel and D. Kröning. 2ls for Program Analysis (Competition Contribution). In Proc. TACAS, LNCS 9636, pages 905-907, 2016. Springer. doi:10.1007/978-3-662-49674-9_56 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{2LS-SVCOMP16, author = {P.~Schrammel and D.~Kröning}, title = {{2ls} for Program Analysis (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {905-907}, year = {2016}, series = {LNCS~9636}, publisher = {Springer}, doi = {10.1007/978-3-662-49674-9_56}, }
8. E. Tomasco, T. L. Nguyen, O. Inverso, B. Fischer, S. La Torre, and G. Parlato. MU-CSeq 0.4: Individual Memory Location Unwindings (Competition Contribution). In Proc. TACAS, LNCS 9636, pages 436-438, 2016. Springer. doi:10.1007/978-3-662-49674-9_65 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{MUCSEQ-SVCOMP16, author = {E.~Tomasco and T.~L.~Nguyen and O.~Inverso and B.~Fischer and S.~La~Torre and G.~Parlato}, title = {{MU-CSeq} 0.4: Individual Memory Location Unwindings (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {436-438}, year = {2016}, series = {LNCS~9636}, publisher = {Springer}, doi = {10.1007/978-3-662-49674-9_65}, }
9. K. Friedberger. CPA-BAM: Block-Abstraction Memoization with Value Analysis and Predicate Analysis (Competition Contribution). In Proc. TACAS, LNCS 9636, pages 912-915, 2016. Springer. doi:10.1007/978-3-662-49674-9_58 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{CPABAM-SVCOMP16, author = {K.~Friedberger}, title = {{CPA-BAM}: Block-Abstraction Memoization with Value Analysis and Predicate Analysis (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {912-915}, year = {2016}, series = {LNCS~9636}, publisher = {Springer}, doi = {10.1007/978-3-662-49674-9_58}, }
10. E. G. Karpenkov. LPI: Software Verification with Local Policy Iteration (Competition Contribution). In Proc. TACAS, LNCS 9636, pages 930-933, 2016. Springer. doi:10.1007/978-3-662-49674-9_63 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{LPI-SVCOMP16, author = {E.~G.~Karpenkov}, title = {{LPI}: Software Verification with Local Policy Iteration (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {930-933}, year = {2016}, series = {LNCS~9636}, publisher = {Springer}, doi = {10.1007/978-3-662-49674-9_63}, }
11. S. Löwe. CPA-RefSel: CPAchecker with Refinement Selection (Competition Contribution). In Proc. TACAS, LNCS 9636, pages 916-919, 2016. Springer. doi:10.1007/978-3-662-49674-9_59 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{CPAREFSEL-SVCOMP16, author = {S.~L{\"{o}}we}, title = {{CPA-RefSel}: {CPAchecker} with Refinement Selection (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {916-919}, year = {2016}, series = {LNCS~9636}, publisher = {Springer}, doi = {10.1007/978-3-662-49674-9_59}, }
12. V. Still, P. Rockai, and J. Barnat. Divine: Explicit-State LTL Model Checker (Competition Contribution). In Proc. TACAS, LNCS 9636, pages 920-922, 2016. Springer. doi:10.1007/978-3-662-49674-9_60 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{DIVINE-SVCOMP16, author = {V.~Still and P.~Rockai and J.~Barnat}, title = {{Divine}: Explicit-State {LTL} Model Checker (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {920-922}, year = {2016}, series = {LNCS~9636}, publisher = {Springer}, doi = {10.1007/978-3-662-49674-9_60}, }
13. M. Zheng, J. G. Edenhofner, Z. Luo, M. J. Gerrard, M. B. Dwyer, and S. F. Siegel. Civl: Applying a General Concurrency Verification Framework to C/Pthreads Programs (Competition Contribution). In Proc. TACAS, LNCS 9636, pages 908-911, 2016. Springer. doi:10.1007/978-3-662-49674-9_57 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{CIVL-SVCOMP16, author = {M.~Zheng and J.~G.~Edenhofner and Z.~Luo and M.~J.~Gerrard and M.~B.~Dwyer and S.~F.~Siegel}, title = {{Civl}: Applying a General Concurrency Verification Framework to {C/Pthreads} Programs (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {908-911}, year = {2016}, series = {LNCS~9636}, publisher = {Springer}, doi = {10.1007/978-3-662-49674-9_57}, }
14. O. Saarikivi and K. Heljanko. LCTD: Tests-Guided Proofs for C Programs on LLVM (Competition Contribution). In Proc. TACAS, LNCS 9636, pages 927-929, 2016. Springer. doi:10.1007/978-3-662-49674-9_62 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{LCTD-SVCOMP16, author = {O.~Saarikivi and K.~Heljanko}, title = {{LCTD}: Tests-Guided Proofs for {C} Programs on {LLVM} (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {927-929}, year = {2016}, series = {LNCS~9636}, publisher = {Springer}, doi = {10.1007/978-3-662-49674-9_62}, }
15. M. Heizmann, D. Dietsch, M. Greitschus, J. Leike, B. Musa, C. Schätzle, and A. Podelski. Ultimate Automizer with Two-track Proofs (Competition Contribution). In Proc. TACAS, LNCS 9636, pages 950-953, 2016. Springer. doi:10.1007/978-3-662-49674-9_68 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{UAUTOMIZER-SVCOMP16, author = {M.~Heizmann and D.~Dietsch and M.~Greitschus and J.~Leike and B.~Musa and C.~Sch{\"{a}}tzle and A.~Podelski}, title = {{Ultimate Automizer} with Two-track Proofs (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {950-953}, year = {2016}, series = {LNCS~9636}, publisher = {Springer}, doi = {10.1007/978-3-662-49674-9_68}, }

SV-COMP 2015

1. D. Beyer. Software Verification and Verifiable Witnesses (Report on SV-COMP 2015). In Proc. TACAS, LNCS 9035, pages 401-416, 2015. Springer. doi:10.1007/978-3-662-46681-0_31 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{SVCOMP15, author = {D.~Beyer}, title = {Software Verification and Verifiable Witnesses ({R}eport on {SV-COMP} 2015)}, booktitle = {Proc.\ TACAS}, pages = {401-416}, year = {2015}, series = {LNCS~9035}, publisher = {Springer}, doi = {10.1007/978-3-662-46681-0_31}, sha256 = {858448ee22256b3ed7f35603d81e942b58652f3b4d2660a22b858dc1c3ac16d0}, }
2. L. Holík, M. Hruška, O. Lengál, A. Rogalewicz, J. Simácek, and T. Vojnar. Forester: Shape Analysis Using Tree Automata. In Proc. TACAS, LNCS 9035, pages 432-435, 2015. Springer. doi:10.1007/978-3-662-46681-0_37 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{FORESTER-SVCOMP15, author = {L.~Hol{\'{\i}}k and M.~Hruška and O.~Leng{\'{a}}l and A.~Rogalewicz and J.~Sim{\'{a}}cek and T.~Vojnar}, title = {{Forester}: {S}hape Analysis Using Tree Automata}, booktitle = {Proc.\ TACAS}, pages = {432-435}, year = {2015}, series = {LNCS~9035}, publisher = {Springer}, doi = {10.1007/978-3-662-46681-0_37}, }
3. T. Ströder, C. Aschermann, F. Frohn, J. Hensel, and J. Giesl. AProVE: Termination and Memory Safety of C Programs (Competition Contribution). In Proc. TACAS, LNCS 9035, pages 417-419, 2015. Springer. doi:10.1007/978-3-662-46681-0_32 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{APROVE-SVCOMP15, author = {T.~Ströder and C.~Aschermann and F.~Frohn and J.~Hensel and J.~Giesl}, title = {{AProVE}: {T}ermination and Memory Safety of {C} Programs (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {417-419}, year = {2015}, series = {LNCS~9035}, publisher = {Springer}, doi = {10.1007/978-3-662-46681-0_32}, }
4. F. Cassez, T. Matsuoka, E. Pierzchalski, and N. Smyth. Perentie: Modular Trace Refinement and Selective Value Tracking (Competition Contribution). In Proc. TACAS, LNCS 9035, pages 439-442, 2015. Springer. doi:10.1007/978-3-662-46681-0_39 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{PERENTIE-SVCOMP15, author = {F.~Cassez and T.~Matsuoka and E.~Pierzchalski and N.~Smyth}, title = {{Perentie}: {M}odular Trace Refinement and Selective Value Tracking (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {439-442}, year = {2015}, series = {LNCS~9035}, publisher = {Springer}, doi = {10.1007/978-3-662-46681-0_39}, }
5. C. Urban. FuncTion: An Abstract Domain Functor for Termination (Competition Contribution). In Proc. TACAS, LNCS 9035, pages 464-466, 2015. Springer. doi:10.1007/978-3-662-46681-0_46 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{FUNCTION-SVCOMP15, author = {C.~Urban}, title = {{FuncTion}: {A}n Abstract Domain Functor for Termination (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {464-466}, year = {2015}, series = {LNCS~9035}, publisher = {Springer}, doi = {10.1007/978-3-662-46681-0_46}, }
6. Y.-F. Chen, C. Hsieh, M.-H. Tsai, B.-Y. Wang, and F. Wang. CPArec: Verifying Recursive Programs via Source-to-Source Program Transformation (Competition Contribution). In Proc. TACAS, LNCS 9035, pages 426-428, 2015. Springer. doi:10.1007/978-3-662-46681-0_35 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{CPAREC-SVCOMP15, author = {Y.-F.~Chen and C.~Hsieh and M.-H.~Tsai and B.-Y.~Wang and F.~Wang}, title = {{CPArec}: {V}erifying Recursive Programs via Source-to-Source Program Transformation (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {426-428}, year = {2015}, series = {LNCS~9035}, publisher = {Springer}, doi = {10.1007/978-3-662-46681-0_35}, }
7. A. Haran, M. Carter, M. Emmi, A. Lal, S. Qadeer, and Z. Rakamarić. Smack+Corral: A Modular Verifier (Competition Contribution). In Proc. TACAS, LNCS 9035, pages 451-454, 2015. Springer. doi:10.1007/978-3-662-46681-0_42 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{SMACKCORRAL-SVCOMP15, author = {A.~Haran and M.~Carter and M.~Emmi and A.~Lal and S.~Qadeer and Z.~Rakamarić}, title = {{Smack+Corral}: {A} Modular Verifier (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {451-454}, year = {2015}, series = {LNCS~9035}, publisher = {Springer}, doi = {10.1007/978-3-662-46681-0_42}, }
8. A. Nutz, D. Dietsch, M. M. Mohamed, and A. Podelski. Ultimate Kojak with Memory Safety Checks (Competition Contribution). In Proc. TACAS, LNCS 9035, pages 458-460, 2015. Springer. doi:10.1007/978-3-662-46681-0_44 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{KOJAK-SVCOMP15, author = {A.~Nutz and D.~Dietsch and M.~M.~Mohamed and A.~Podelski}, title = {{Ultimate Kojak} with Memory Safety Checks (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {458-460}, year = {2015}, series = {LNCS~9035}, publisher = {Springer}, doi = {10.1007/978-3-662-46681-0_44}, }
9. P. Müller, P. Peringer, and T. Vojnar. Predator Hunting Party (Competition Contribution). In Proc. TACAS, LNCS 9035, pages 443-446, 2015. Springer. doi:10.1007/978-3-662-46681-0_40 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{PREDATOR-SVCOMP15, author = {P.~M{\"{u}}ller and P.~Peringer and T.~Vojnar}, title = {{Predator} Hunting Party (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {443-446}, year = {2015}, series = {LNCS~9035}, publisher = {Springer}, doi = {10.1007/978-3-662-46681-0_40}, }
10. P. Gonzalez-de-Aledo and P. Sanchez. FramewORk for Embedded System verificaTion (Competition Contribution). In Proc. TACAS, LNCS 9035, pages 429-431, 2015. Springer. doi:10.1007/978-3-662-46681-0_36 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{FOREST-SVCOMP15, author = {P.~Gonzalez-de-Aledo and P.~Sanchez}, title = {FramewORk for Embedded System verificaTion (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {429-431}, year = {2015}, series = {LNCS~9035}, publisher = {Springer}, doi = {10.1007/978-3-662-46681-0_36}, }
11. W. Wang and C. Barrett. Cascade (Competition Contribution). In Proc. TACAS, LNCS 9035, pages 420-422, 2015. Springer. doi:10.1007/978-3-662-46681-0_33 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{CASCADE-SVCOMP15, author = {W.~Wang and C.~Barrett}, title = {{Cascade} (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {420-422}, year = {2015}, series = {LNCS~9035}, publisher = {Springer}, doi = {10.1007/978-3-662-46681-0_33}, }
12. E. Tomasco, O. Inverso, B. Fischer, S. La Torre, and G. Parlato. MU-CSeq 0.3: Sequentialization by Read-Implicit and Coarse-Grained Memory Unwindings (Competition Contribution). In Proc. TACAS, LNCS 9035, pages 436-438, 2015. Springer. doi:10.1007/978-3-662-46681-0_38 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{MUCSEQ-SVCOMP15, author = {E.~Tomasco and O.~Inverso and B.~Fischer and S.~La~Torre and G.~Parlato}, title = {{MU-CSeq 0.3}: {S}equentialization by Read-Implicit and Coarse-Grained Memory Unwindings (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {436-438}, year = {2015}, series = {LNCS~9035}, publisher = {Springer}, doi = {10.1007/978-3-662-46681-0_38}, }
13. T. L. Nguyen, B. Fischer, S. La Torre, and G. Parlato. Unbounded Lazy-CSeq: A Lazy Sequentialization Tool for C Programs with Unbounded Context Switches (Competition Contribution). In Proc. TACAS, LNCS 9035, pages 461-463, 2015. Springer. doi:10.1007/978-3-662-46681-0_45 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{ULAZYCSEQ-SVCOMP15, author = {T.~L.~Nguyen and B.~Fischer and S.~La~Torre and G.~Parlato}, title = {{Unbounded Lazy-CSeq}: {A} Lazy Sequentialization Tool for {C} Programs with Unbounded Context Switches (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {461-463}, year = {2015}, series = {LNCS~9035}, publisher = {Springer}, doi = {10.1007/978-3-662-46681-0_45}, }
14. M. Dangl, S. Löwe, and P. Wendler. CPAchecker with Support for Recursive Programs and Floating-Point Arithmetic (Competition Contribution). In Proc. TACAS, LNCS 9035, pages 423-425, 2015. Springer. doi:10.1007/978-3-662-46681-0_34 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{CPACHECKER-SVCOMP15, author = {M.~Dangl and S.~L{\"{o}}we and P.~Wendler}, title = {{CPAchecker} with Support for Recursive Programs and Floating-Point Arithmetic (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {423-425}, year = {2015}, series = {LNCS~9035}, publisher = {Springer}, doi = {10.1007/978-3-662-46681-0_34}, }
15. A. Gurfinkel, T. Kahsai, and J. A. Navas. SeaHorn: A Framework for Verifying C Programs (Competition Contribution). In Proc. TACAS, LNCS 9035, pages 447-450, 2015. Springer. doi:10.1007/978-3-662-46681-0_41 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{SEAHORN-SVCOMP15, author = {A.~Gurfinkel and T.~Kahsai and J.~A.~Navas}, title = {{SeaHorn}: {A} Framework for Verifying {C} Programs (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {447-450}, year = {2015}, series = {LNCS~9035}, publisher = {Springer}, doi = {10.1007/978-3-662-46681-0_41}, }
16. M. Heizmann, D. Dietsch, J. Leike, B. Musa, and A. Podelski. Ultimate Automizer with Array Interpolation. In Proc. TACAS, LNCS 9035, pages 455-457, 2015. Springer. doi:10.1007/978-3-662-46681-0_43 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{AUTOMIZER-SVCOMP15, author = {M.~Heizmann and D.~Dietsch and J.~Leike and B.~Musa and A.~Podelski}, title = {{Ultimate Automizer} with Array Interpolation}, booktitle = {Proc.\ TACAS}, pages = {455-457}, year = {2015}, series = {LNCS~9035}, publisher = {Springer}, doi = {10.1007/978-3-662-46681-0_43}, }

SV-COMP 2014

1. D. Beyer. Status Report on Software Verification (Competition Summary SV-COMP 2014). In Proc. TACAS, LNCS 8413, pages 373-388, 2014. Springer. doi:10.1007/978-3-642-54862-8_25 Publisher's Version PDF Supplement
   BibTeX Entry

   @inproceedings{SVCOMP14, author = {D.~Beyer}, title = {Status Report on Software Verification ({C}ompetition Summary {SV-COMP} 2014)}, booktitle = {Proc.\ TACAS}, pages = {373-388}, year = {2014}, series = {LNCS~8413}, publisher = {Springer}, doi = {10.1007/978-3-642-54862-8_25}, url = {https://www.sosy-lab.org/research/pub/2014-TACAS.Status_Report_on_Software_Verification.pdf}, }
2. S. Löwe, M. U. Mandrykin, and P. Wendler. CPAchecker with Sequential Combination of Explicit-Value Analyses and Predicate Analyses (Competition Contribution). In Proc. TACAS, LNCS 8413, pages 392-394, 2014. Springer. doi:10.1007/978-3-642-54862-8_27 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{CPACHECKER-SVCOMP14, author = {S.~L{\"{o}}we and M.~U.~Mandrykin and P.~Wendler}, title = {{CPAchecker} with Sequential Combination of Explicit-Value Analyses and Predicate Analyses (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {392-394}, year = {2014}, series = {LNCS~8413}, publisher = {Springer}, doi = {10.1007/978-3-642-54862-8_27}, }
3. D. Kröning and M. Tautschnig. Cbmc: C Bounded Model Checker (Competition Contribution). In Proc. TACAS, LNCS 8413, pages 389-391, 2014. Springer. doi:10.1007/978-3-642-54862-8_26 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{CBMC-SVCOMP14, author = {D.~Kröning and M.~Tautschnig}, title = {{Cbmc}: {C} Bounded Model Checker (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {389-391}, year = {2014}, series = {LNCS~8413}, publisher = {Springer}, doi = {10.1007/978-3-642-54862-8_26}, isbnnote = {978-3-642-54861-1}, }
4. P. Müller and T. Vojnar. CPAlien: Shape Analyzer for CPAchecker (Competition Contribution). In Proc. TACAS, LNCS 8413, pages 395-397, 2014. Springer. doi:10.1007/978-3-642-54862-8_28 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{CPALIEN-SVCOMP14, author = {P.~Müller and T.~Vojnar}, title = {{CPAlien}: Shape Analyzer for {CPAchecker} (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {395-397}, year = {2014}, series = {LNCS~8413}, publisher = {Springer}, doi = {10.1007/978-3-642-54862-8_28}, }
5. O. Inverso, E. Tomasco, B. Fischer, S. La Torre, and G. Parlato. Lazy-CSeq: A Lazy Sequentialization Tool for C (Competition Contribution). In Proc. TACAS, LNCS 8413, pages 398-401, 2014. Springer. doi:10.1007/978-3-642-54862-8_29 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{CSEQLAZY-SVCOMP14, author = {O.~Inverso and E.~Tomasco and B.~Fischer and S.~{La~Torre} and G.~Parlato}, title = {{Lazy-CSeq}: A Lazy Sequentialization Tool for {C} (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {398-401}, year = {2014}, series = {LNCS~8413}, publisher = {Springer}, doi = {10.1007/978-3-642-54862-8_29}, isbnnote = {978-3-642-54861-1}, }
6. E. Tomasco, O. Inverso, B. Fischer, S. La Torre, and G. Parlato. MU-CSeq: Sequentialization of C Programs by Shared Memory Unwindings (Competition Contribution). In Proc. TACAS, LNCS 8413, pages 402-404, 2014. Springer. doi:10.1007/978-3-642-54862-8_30 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{CSEQMU-SVCOMP14, author = {E.~Tomasco and O.~Inverso and B.~Fischer and S.~{La~Torre} and G.~Parlato}, title = {{MU-CSeq}: Sequentialization of {C} Programs by Shared Memory Unwindings (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {402-404}, year = {2014}, series = {LNCS~8413}, publisher = {Springer}, doi = {10.1007/978-3-642-54862-8_30}, }
7. J. Morse, M. Ramalho, L. C. Cordeiro, D. Nicole, and B. Fischer. Esbmc 1.22 (Competition Contribution). In Proc. TACAS, LNCS 8413, pages 405-407, 2014. Springer. doi:10.1007/978-3-642-54862-8_31 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{ESBMC-SVCOMP14, author = {J.~Morse and M.~Ramalho and L.~C.~Cordeiro and D.~Nicole and B.~Fischer}, title = {{Esbmc} 1.22 (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {405-407}, year = {2014}, series = {LNCS~8413}, publisher = {Springer}, doi = {10.1007/978-3-642-54862-8_31}, }
8. A. Gurfinkel and A. Belov. FrankenBit: Bit-Precise Verification with Many Bits (Competition Contribution). In Proc. TACAS, LNCS 8413, pages 408-411, 2014. Springer. doi:10.1007/978-3-642-54862-8_32 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{FBIT-SVCOMP14, author = {A.~Gurfinkel and A.~Belov}, title = {{FrankenBit}: Bit-Precise Verification with Many Bits (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {408-411}, year = {2014}, series = {LNCS~8413}, publisher = {Springer}, doi = {10.1007/978-3-642-54862-8_32}, }
9. K. Dudka, P. Peringer, and T. Vojnar. Predator: A Shape Analyzer Based on Symbolic Memory Graphs (Competition Contribution). In Proc. TACAS, LNCS 8413, pages 412-414, 2014. Springer. doi:10.1007/978-3-642-54862-8_33 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{PREDATOR-SVCOMP14, author = {K.~Dudka and P.~Peringer and T.~Vojnar}, title = {{Predator}: A Shape Analyzer Based on Symbolic Memory Graphs (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {412-414}, year = {2014}, series = {LNCS~8413}, publisher = {Springer}, doi = {10.1007/978-3-642-54862-8_33}, }
10. J. Slaby and J. Strejček. Symbiotic 2: More Precise Slicing (Competition Contribution). In Proc. TACAS, LNCS 8413, pages 415-417, 2014. Springer. doi:10.1007/978-3-642-54862-8_34 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{SYMBIOTIC-SVCOMP14, author = {J.~Slaby and J.~Strejček}, title = {{Symbiotic} 2: More Precise Slicing (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {415-417}, year = {2014}, series = {LNCS~8413}, publisher = {Springer}, doi = {10.1007/978-3-642-54862-8_34}, }
11. M. Heizmann, J. Christ, D. Dietsch, J. Hoenicke, M. Lindenmann, B. Musa, C. Schilling, S. Wissert, and A. Podelski. Ultimate Automizer with Unsatisfiable Cores (Competition Contribution). In Proc. TACAS, LNCS 8413, pages 418-420, 2014. Springer. doi:10.1007/978-3-642-54862-8_35 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{AUTOMIZER-SVCOMP14, author = {M.~Heizmann and J.~Christ and D.~Dietsch and J.~Hoenicke and M.~Lindenmann and B.~Musa and C.~Schilling and S.~Wissert and A.~Podelski}, title = {{Ultimate Automizer} with Unsatisfiable Cores (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {418-420}, year = {2014}, series = {LNCS~8413}, publisher = {Springer}, doi = {10.1007/978-3-642-54862-8_35}, }
12. E. Ermis, A. Nutz, D. Dietsch, J. Hoenicke, and A. Podelski. Ultimate Kojak (Competition Contribution). In Proc. TACAS, LNCS 8413, pages 421-423, 2014. Springer. doi:10.1007/978-3-642-54862-8_36 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{KOJAK-SVCOMP14, author = {E.~Ermis and A.~Nutz and D.~Dietsch and J.~Hoenicke and A.~Podelski}, title = {{Ultimate Kojak} (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {421-423}, year = {2014}, series = {LNCS~8413}, publisher = {Springer}, doi = {10.1007/978-3-642-54862-8_36}, }

SV-COMP 2013

1. D. Beyer. Second Competition on Software Verification (Summary of SV-COMP 2013). In Proc. TACAS, LNCS 7795, pages 594-609, 2013. Springer. doi:10.1007/978-3-642-36742-7_43 Publisher's Version PDF Supplement
   BibTeX Entry

   @inproceedings{SVCOMP13, author = {D.~Beyer}, title = {Second Competition on Software Verification ({S}ummary of {SV-COMP} 2013)}, booktitle = {Proc.\ TACAS}, pages = {594-609}, year = {2013}, series = {LNCS~7795}, publisher = {Springer}, doi = {10.1007/978-3-642-36742-7_43}, url = {https://www.sosy-lab.org/research/pub/2013-TACAS.Second_Competition_on_Software_Verification.pdf}, }
2. S. Löwe. CPAchecker with Explicit-Value Analysis Based on CEGAR and Interpolation (Competition Contribution). In Proc. TACAS, LNCS 7795, pages 610-612, 2013. Springer. doi:10.1007/978-3-642-36742-7_44 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{CPACHECKEREXPLICIT-SVCOMP13, author = {S.~L{\"{o}}we}, title = {{CPAchecker} with Explicit-Value Analysis Based on {CEGAR} and Interpolation (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {610-612}, year = {2013}, series = {LNCS~7795}, publisher = {Springer}, doi = {10.1007/978-3-642-36742-7_44}, }
3. P. Wendler. CPAchecker with Sequential Combination of Explicit-State Analysis and Predicate Analysis (Competition Contribution). In Proc. TACAS, LNCS 7795, pages 613-615, 2013. Springer. doi:10.1007/978-3-642-36742-7_45 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{CPACHECKERSEQCOM-SVCOMP13, author = {P.~Wendler}, title = {{CPAchecker} with Sequential Combination of Explicit-State Analysis and Predicate Analysis (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {613-615}, year = {2013}, series = {LNCS~7795}, publisher = {Springer}, doi = {10.1007/978-3-642-36742-7_45}, }
4. K. Dudka, P. Müller, P. Peringer, and T. Vojnar. Predator: A Tool for Verification of Low-level List Manipulation (Competition Contribution). In Proc. TACAS, LNCS 7795, pages 627-629, 2013. Springer. doi:10.1007/978-3-642-36742-7_49 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{PREDATOR-SVCOMP13, author = {K.~Dudka and P.~Müller and P.~Peringer and T.~Vojnar}, title = {{Predator}: {A} Tool for Verification of Low-level List Manipulation (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {627-629}, year = {2013}, series = {LNCS~7795}, publisher = {Springer}, doi = {10.1007/978-3-642-36742-7_49}, }
5. J. Slaby, J. Strejček, and M. Trtík. Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution (Competition Contribution). In Proc. TACAS, LNCS 7795, pages 630-632, 2013. Springer. doi:10.1007/978-3-642-36742-7_50 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{SYMBIOTIC-SVCOMP13, author = {J.~Slaby and J.~Strejček and M.~Trtík}, title = {{Symbiotic}: {Synergy} of Instrumentation, Slicing, and Symbolic Execution (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {630-632}, year = {2013}, series = {LNCS~7795}, publisher = {Springer}, doi = {10.1007/978-3-642-36742-7_50}, }
6. B. Fischer, O. Inverso, and G. Parlato. CSeq: A Sequentialization Tool for C (Competition Contribution). In Proc. TACAS, LNCS 7795, pages 616-618, 2013. Springer. doi:10.1007/978-3-642-36742-7_46 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{CSEQ-SVCOMP13, author = {B.~Fischer and O.~Inverso and G.~Parlato}, title = {{CSeq}: {A} Sequentialization Tool for {C} (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {616-618}, year = {2013}, series = {LNCS~7795}, publisher = {Springer}, doi = {10.1007/978-3-642-36742-7_46}, }
7. A. Gurfinkel, A. Albarghouthi, S. Chaki, Y. Li, and M. Chechik. Ufo: Verification with Interpolants and Abstract Interpretation (Competition Contribution). In Proc. TACAS, LNCS 7795, pages 637-640, 2013. Springer. doi:10.1007/978-3-642-36742-7_52 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{UFO-SVCOMP13, author = {A.~Gurfinkel and A.~Albarghouthi and S.~Chaki and Y.~Li and M.~Chechik}, title = {{Ufo}: {Verification} with Interpolants and Abstract Interpretation (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {637-640}, year = {2013}, series = {LNCS~7795}, publisher = {Springer}, doi = {10.1007/978-3-642-36742-7_52}, }
8. S. Falke, F. Merz, and C. Sinz. Llbmc: Improved Bounded Model Checking of C Programs Using LLVM (Competition Contribution). In Proc. TACAS, LNCS 7795, pages 623-626, 2013. Springer. doi:10.1007/978-3-642-36742-7_48 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{LLBMC-SVCOMP13, author = {S.~Falke and F.~Merz and C.~Sinz}, title = {{Llbmc}: {Improved} Bounded Model Checking of {C} Programs Using {LLVM} (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {623-626}, year = {2013}, series = {LNCS~7795}, publisher = {Springer}, doi = {10.1007/978-3-642-36742-7_48}, }
9. C. Popeea and A. Rybalchenko. Threader: A Verifier for Multi-threaded Programs (Competition Contribution). In Proc. TACAS, LNCS 7795, pages 633-636, 2013. Springer. doi:10.1007/978-3-642-36742-7_51 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{THREADER-SVCOMP13, author = {C.~Popeea and A.~Rybalchenko}, title = {{Threader}: {A} Verifier for Multi-threaded Programs (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {633-636}, year = {2013}, series = {LNCS~7795}, publisher = {Springer}, doi = {10.1007/978-3-642-36742-7_51}, }
10. J. Morse, L. C. Cordeiro, D. Nicole, and B. Fischer. Handling Unbounded Loops with Esbmc 1.20 (Competition Contribution). In Proc. TACAS, LNCS 7795, pages 619-622, 2013. Springer. doi:10.1007/978-3-642-36742-7_47 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{ESBMC-SVCOMP13, author = {J.~Morse and L.~C.~Cordeiro and D.~Nicole and B.~Fischer}, title = {Handling Unbounded Loops with {Esbmc} 1.20 (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {619-622}, year = {2013}, series = {LNCS~7795}, publisher = {Springer}, doi = {10.1007/978-3-642-36742-7_47}, }
11. M. Heizmann, J. Christ, D. Dietsch, E. Ermis, J. Hoenicke, M. Lindenmann, A. Nutz, C. Schilling, and A. Podelski. Ultimate Automizer with SMTInterpol (Competition Contribution). In Proc. TACAS, LNCS 7795, pages 641-643, 2013. Springer. doi:10.1007/978-3-642-36742-7_53 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{ULTIMATE-SVCOMP13, author = {M.~Heizmann and J.~Christ and D.~Dietsch and E.~Ermis and J.~Hoenicke and M.~Lindenmann and A.~Nutz and C.~Schilling and A.~Podelski}, title = {{Ultimate Automizer} with {SMTInterpol} (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {641-643}, year = {2013}, series = {LNCS~7795}, publisher = {Springer}, doi = {10.1007/978-3-642-36742-7_53}, }

SV-COMP 2012

1. D. Beyer. Competition on Software Verification (SV-COMP). In Proc. TACAS, LNCS 7214, pages 504-524, 2012. Springer. doi:10.1007/978-3-642-28756-5_38 Publisher's Version PDF Supplement
   BibTeX Entry

   @inproceedings{SVCOMP12, author = {D.~Beyer}, title = {Competition on Software Verification ({SV-COMP})}, booktitle = {Proc.\ TACAS}, pages = {504-524}, year = {2012}, series = {LNCS~7214}, publisher = {Springer}, doi = {10.1007/978-3-642-28756-5_38}, url = {https://www.sosy-lab.org/research/pub/2012-TACAS.Competition_on_Software_Verification.pdf}, }
2. K. Dudka, P. Müller, P. Peringer, and T. Vojnar. Predator: A Verification Tool for Programs with Dynamic Linked Data Structures (Competition Contribution). In Proc. TACAS, LNCS 7214, pages 545-548, 2012. Springer. doi:10.1007/978-3-642-28756-5_45 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{PREDATOR-SVCOMP12, author = {K.~Dudka and P.~M{\"{u}}ller and P.~Peringer and T.~Vojnar}, title = {{Predator}: {A} Verification Tool for Programs with Dynamic Linked Data Structures (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {545-548}, year = {2012}, series = {LNCS~7214}, publisher = {Springer}, doi = {10.1007/978-3-642-28756-5_45}, }
3. P. Shved, M. U. Mandrykin, and V. S. Mutilin. Predicate Analysis with Blast 2.7 (Competition Contribution). In Proc. TACAS, LNCS 7214, pages 525-527, 2012. Springer. doi:10.1007/978-3-642-28756-5_39 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{BLAST-SVCOMP12, author = {P.~Shved and M.~U.~Mandrykin and V.~S.~Mutilin}, title = {Predicate Analysis with {Blast} 2.7 (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {525-527}, year = {2012}, series = {LNCS~7214}, publisher = {Springer}, doi = {10.1007/978-3-642-28756-5_39}, }
4. D. Wonisch. Block Abstraction Memoization for CPAchecker (Competition Contribution). In Proc. TACAS, LNCS 7214, pages 531-533, 2012. Springer. doi:10.1007/978-3-642-28756-5_41 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{CPACHECKERMEMO-SVCOMP12, author = {D.~Wonisch}, title = {Block Abstraction Memoization for {CPAchecker} (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {531-533}, year = {2012}, series = {LNCS~7214}, publisher = {Springer}, doi = {10.1007/978-3-642-28756-5_41}, }
5. L. C. Cordeiro, J. Morse, D. Nicole, and B. Fischer. Context-Bounded Model Checking with Esbmc 1.17 (Competition Contribution). In Proc. TACAS, LNCS 7214, pages 534-537, 2012. Springer. doi:10.1007/978-3-642-28756-5_42 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{ESBMC-SVCOMP12, author = {L.~C.~Cordeiro and J.~Morse and D.~Nicole and B.~Fischer}, title = {Context-Bounded Model Checking with {Esbmc} 1.17 (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {534-537}, year = {2012}, series = {LNCS~7214}, publisher = {Springer}, doi = {10.1007/978-3-642-28756-5_42}, isbnnote = {978-3-642-28755-8}, }
6. C. Sinz, F. Merz, and S. Falke. Llbmc: A Bounded Model Checker for Llvm’s Intermediate Representation (Competition Contribution). In Proc. TACAS, LNCS 7214, pages 542-544, 2012. Springer. doi:10.1007/978-3-642-28756-5_44 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{LLBMC-SVCOMP12, author = {C.~Sinz and F.~Merz and S.~Falke}, title = {{Llbmc}: {A} Bounded Model Checker for {Llvm}’s Intermediate Representation (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {542-544}, year = {2012}, series = {LNCS~7214}, publisher = {Springer}, doi = {10.1007/978-3-642-28756-5_44}, }
7. G. Weissenbacher, D. Kröning, and S. Malik. Wolverine: Battling Bugs with Interpolants (Competition Contribution). In Proc. TACAS, LNCS 7214, pages 556-558, 2012. Springer. doi:10.1007/978-3-642-28756-5_48 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{WOLVERINE-SVCOMP12, author = {G.~Weissenbacher and D.~Kröning and S.~Malik}, title = {{Wolverine}: {B}attling Bugs with Interpolants (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {556-558}, year = {2012}, series = {LNCS~7214}, publisher = {Springer}, doi = {10.1007/978-3-642-28756-5_48}, }
8. S. Löwe and P. Wendler. CPAchecker with Adjustable Predicate Analysis (Competition Contribution). In Proc. TACAS, LNCS 7214, pages 528-530, 2012. Springer. doi:10.1007/978-3-642-28756-5_40 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{CPACHECKERABE-SVCOMP12, author = {S.~Löwe and P.~Wendler}, title = {{CPAchecker} with Adjustable Predicate Analysis (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {528-530}, year = {2012}, series = {LNCS~7214}, publisher = {Springer}, doi = {10.1007/978-3-642-28756-5_40}, }
9. G. Basler, A. F. Donaldson, A. Kaiser, D. Kröning, M. Tautschnig, and T. Wahl. SATabs: A Bit-Precise Verifier for C Programs (Competition Contribution). In Proc. TACAS, LNCS 7214, pages 552-555, 2012. Springer. doi:10.1007/978-3-642-28756-5_47 Publisher's Version PDF
   BibTeX Entry

   @inproceedings{SATABS-SVCOMP12, author = {G.~Basler and A.~F.~Donaldson and A.~Kaiser and D.~Kröning and M.~Tautschnig and T.~Wahl}, title = {{SATabs}: {A} Bit-Precise Verifier for {C} Programs (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {552-555}, year = {2012}, series = {LNCS~7214}, publisher = {Springer}, doi = {10.1007/978-3-642-28756-5_47}, }
10. A. Holzer, D. Kröning, C. Schallhart, M. Tautschnig, and H. Veith. Proving Reachability using FShell (Competition Contribution). In Proc. TACAS, LNCS 7214, pages 538-541, 2012. Springer. doi:10.1007/978-3-642-28756-5_43 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{FSHELL-SVCOMP12, author = {A.~Holzer and D.~Kröning and C.~Schallhart and M.~Tautschnig and H.~Veith}, title = {Proving Reachability using {FShell} (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {538-541}, year = {2012}, series = {LNCS~7214}, publisher = {Springer}, doi = {10.1007/978-3-642-28756-5_43}, }
11. S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea, and A. Rybalchenko. Hsf(c): A Software Verifier based on Horn Clauses (Competition Contribution). In Proc. TACAS, LNCS 7214, pages 549-551, 2012. Springer. doi:10.1007/978-3-642-28756-5_46 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{HSFC-SVCOMP12, author = {S.~Grebenshchikov and A.~Gupta and N.~P.~Lopes and C.~Popeea and A.~Rybalchenko}, title = {{{Hsf}({c})}: {A} Software Verifier based on {H}orn Clauses (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {549-551}, year = {2012}, series = {LNCS~7214}, publisher = {Springer}, doi = {10.1007/978-3-642-28756-5_46}, }

Imprint and Privacy Policy