Publications of SV-COMP

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 Link to this entry 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 Link to this entry 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 Link to this entry 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 Link to this entry 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 Link to this entry 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 Link to this entry 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 Link to this entry 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 Link to this entry 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 Link to this entry 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 Link to this entry 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{2LS-COMP20, 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{COASTAL-COMP20, 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{DARTAGNAN-COMP20, 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{GACAL-COMP20, 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{JAVARANGER-COMP20, 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{JDART-COMP20, 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{MAP2CHECK-COMP20, 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{PREDATORHP-COMP20, 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{SYMBIOTIC-COMP20, 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{UTAIPAN-COMP20, 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{VERIABS-COMP20, 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 Link to this entry 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. Kareem Khazem and Michael Tautschnig. CBmc Path: A Symbolic Execution Retrofit of the C Bounded Model Checker (Competition Contribution). In Proc. TACAS (3), LNCS 11429, 2019. Springer. Link to this entry
    BibTeX Entry
    @inproceedings{CBMCPATH-SVCOMP19, author = {Kareem Khazem and Michael Tautschnig}, title = {{CBmc Path}: A Symbolic Execution Retrofit of the {C} Bounded Model Checker (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, year = {2019}, series = {LNCS~11429}, publisher = {Springer}, }
  3. Eti Chaudhary and Saurabh 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{PINAKA-SVCOMP19, author = {Eti Chaudhary and Saurabh 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 Link to this entry 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 Link to this entry 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, 2019. Springer. Link to this entry
    BibTeX Entry
    @inproceedings{JPF-SVCOMP19, author = {C.~Artho and W.~Visser}, title = {{Java Pathfinder} at {SV-COMP} 2019 (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, year = {2019}, series = {LNCS~11429}, publisher = {Springer}, }
  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 Link to this entry 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 Link to this entry 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 Link to this entry 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. Temesghen Kahsai, Philipp Rümmer, and Martin 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{JAYHORN-SVCOMP19, author = {Temesghen Kahsai and Philipp Rümmer and Martin 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. Pritom Rajkhowa and Fangzhen Lin. Viap 1.1: Automated System for Verifying Integer Assignment Programs with Loops (Competition Contribution). In Proc. TACAS (3), LNCS 11429, pages 137-144, 2019. Springer. doi:10.1109/SYNASC.2017.00032 Link to this entry Publisher's Version
    BibTeX Entry
    @inproceedings{VIAP-SVCOMP19, author = {Pritom Rajkhowa and Fangzhen Lin}, title = {{Viap} 1.1: Automated System for Verifying Integer Assignment Programs with Loops (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {137-144}, year = {2019}, series = {LNCS~11429}, publisher = {Springer}, doi = {10.1109/SYNASC.2017.00032}, }
  12. Henrich Lauko, Vladimír Štill, Petr Ročkai, and Jiří 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{DIVINESMT-SVCOMP19, author = {Henrich Lauko and Vladimír Štill and Petr Ročkai and Jiří 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 Link to this entry 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 Link to this entry 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. Liangze Yin, Wei Dong, Wanwei Liu, Yunchou Li, and Ji 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{YOGARCBMC-SVCOMP18, author = {Liangze Yin and Wei Dong and Wanwei Liu and Yunchou Li and Ji 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. Priyanka Darke, Sumanth Prabhu, Bharti Chimdyalwar, Avriti Chauhan, Shrawan Kumar, Animesh Basak Chowdhury, R. Venkatesh, Advaita Datar, and Raveendra Kumar Medicherla. 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{VERIABS-SVCOMP18, author = {Priyanka Darke and Sumanth Prabhu and Bharti Chimdyalwar and Avriti Chauhan and Shrawan Kumar and Animesh Basak Chowdhury and R. Venkatesh and Advaita Datar and Raveendra Kumar Medicherla}, 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 Link to this entry 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{CPABAM-COMP17, 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{SKINK-COMP17, 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{SYMBIOTIC-COMP17, 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. Bharti Chimdyalwar, Priyanka Darke, Avriti Chauhan, Punit Shah, Shrawan 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{VERIABS-COMP17, author = {Bharti Chimdyalwar and Priyanka Darke and Avriti Chauhan and Punit Shah and Shrawan 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{UTAIPAN-COMP17, 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{UAUTOMIZER-COMP17, 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. Jera Hensel, Frank Emrich, Florian Frohn, Thomas Ströder, and Jürgen 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{APROVE-COMP17, author = {Jera Hensel and Frank Emrich and Florian Frohn and Thomas Str{\"{o}}der and J{\"{u}}rgen 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. Lukáš Holík, Martin Hruška, Ondřej Lengál, Adam Rogalewicz, Jirí Simácek, and Tomáš 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{FORESTER-COMP17, author = {Luk{\'{a}}{\v{s}} Hol{\'{\i}}k and Martin Hruška and Ondřej Leng{\'{a}}l and Adam Rogalewicz and Jir{\'{\i}} Sim{\'{a}}cek and Tom{\'{a}}{\v{s}} 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. Ton Chanh Le, Quang-Trung Ta, and Wei-Ngan 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{HIPTNT-COMP17, author = {Ton Chanh Le and Quang{-}Trung Ta and Wei{-}Ngan 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. Jan Mrázek, Martin Jonáš, Vladimír Still, Henrich Lauko, and Jiri 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{SYMDIVINE-COMP17, author = {Jan Mr{\'{a}}zek and Martin Jon{\'{a}}{\v{s}} and Vladim{\'{\i}}r Still and Henrich Lauko and Jiri 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. Truc L. Nguyen, Omar Inverso, Bernd Fischer, Salvatore La Torre, and Gennaro 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{LAZYCSEQ-COMP17, author = {Truc L. Nguyen and Omar Inverso and Bernd Fischer and Salvatore {La Torre} and Gennaro 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{DEPTHK-COMP17, 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 Link to this entry 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. Lukáš Holík, Martin Hruška, Ondřej Lengál, Adam Rogalewicz, Jirí Simácek, and Tomáš Vojnar. Run Forester, Run Backwards! (Competition Contribution). In Proc. TACAS, LNCS 9636, pages 923-926, 2016. Springer. Link to this entry
    BibTeX Entry
    @inproceedings{FORESTER-COMP16, author = {Luk{\'{a}}{\v{s}} Hol{\'{\i}}k and Martin Hruška and Ondřej Leng{\'{a}}l and Adam Rogalewicz and Jir{\'{\i}} Sim{\'{a}}cek and Tom{\'{a}}{\v{s}} Vojnar}, title = {Run Forester, Run Backwards! (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {923-926}, year = {2016}, series = {LNCS~9636}, publisher = {Springer}, }
  3. Michal Kotoun, Petr Peringer, Veronika Šoková, and Tomáš 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{PREDATOR-COMP16, author = {Michal Kotoun and Petr Peringer and Veronika {\v{S}}okov{\'{a}} and Tom{\'{a}}{\v{s}} 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. Link to this entry
    BibTeX Entry
    @inproceedings{SYMBIOTIC-COMP16, 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}, }
  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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{MAP2CHECK-COMP16, 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. Henning Günther, Alfons Laarman, and Georg Weissenbacher. Vienna Verification Tool: IC3 for Parallel Software (Competition Contribution). In Proc. TACAS, LNCS 9636, pages 954-957, 2016. Springer. Link to this entry
    BibTeX Entry
    @inproceedings{VVT-COMP16, author = {Henning G{\"{u}}nther and Alfons Laarman and Georg Weissenbacher}, title = {{Vienna Verification Tool}: {IC3} for Parallel Software (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {954-957}, year = {2016}, series = {LNCS~9636}, publisher = {Springer}, }
  7. Peter Schrammel and Daniel 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{2LS-COMP16, author = {Peter Schrammel and Daniel 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. Ermenegildo Tomasco, Truc L. Nguyen, Omar Inverso, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato. MU-CSeq 0.4: Individual Memory Location Unwindings (Competition Contribution). In Proc. TACAS, LNCS 9636, pages 436-438, 2016. Springer. Link to this entry
    BibTeX Entry
    @inproceedings{MUCSEQ-COMP16, author = {Ermenegildo Tomasco and Truc L. Nguyen and Omar Inverso and Bernd Fischer and Salvatore {La Torre} and Gennaro 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}, }
  9. Karlheinz 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{CPABAM-COMP16, author = {Karlheinz 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. Egor George 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{LPI-COMP16, author = {Egor George 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. Stefan 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{CPAREFSEL-COMP16, author = {Stefan 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. Link to this entry
    BibTeX Entry
    @inproceedings{DIVINE-COMP16, 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}, }
  13. Manchun Zheng, John G. Edenhofner, Ziqing Luo, Mitchell J. Gerrard, Matthew B. Dwyer, and Stephen 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. Link to this entry
    BibTeX Entry
    @inproceedings{CIVL-COMP16, author = {Manchun Zheng and John G. Edenhofner and Ziqing Luo and Mitchell J. Gerrard and Matthew B. Dwyer and Stephen 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}, }
  14. Olli Saarikivi and Keijo Heljanko. LCTD: Tests-Guided Proofs for C Programs on LLVM (Competition Contribution). In Proc. TACAS, LNCS 9636, pages 927-929, 2016. Springer. Link to this entry
    BibTeX Entry
    @inproceedings{LCTD-COMP16, author = {Olli Saarikivi and Keijo 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}, }
  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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{UAUTOMIZER-COMP16, 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 Link to this entry Publisher's Version PDF Supplement
    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}, url = {https://www.sosy-lab.org/research/pub/2014-TACAS.Status_Report_on_Software_Verification.pdf}, }
  2. Lukáš Holík, Martin Hruška, Ondřej Lengál, Adam Rogalewicz, Jirí Simácek, and Tomáš Vojnar. Forester: Shape Analysis Using Tree Automata. In Proc. TACAS, LNCS 9035, pages 432-435, 2015. Springer. Link to this entry
    BibTeX Entry
    @inproceedings{FORESTER-COMP15, author = {Luk{\'{a}}{\v{s}} Hol{\'{\i}}k and Martin Hruška and Ondřej Leng{\'{a}}l and Adam Rogalewicz and Jir{\'{\i}} Sim{\'{a}}cek and Tom{\'{a}}{\v{s}} Vojnar}, title = {{Forester}: {S}hape Analysis Using Tree Automata}, booktitle = {Proc.\ TACAS}, pages = {432-435}, year = {2015}, series = {LNCS~9035}, publisher = {Springer}, }
  3. Thomas Ströder, Cornelius Aschermann, Florian Frohn, Jera Hensel, and Jürgen Giesl. AProVE: Termination and Memory Safety of C Programs (Competition Contribution). In Proc. TACAS, LNCS 9035, pages 417-419, 2015. Springer. Link to this entry
    BibTeX Entry
    @inproceedings{APROVE-COMP15, author = {Thomas Str{\"{o}}der and Cornelius Aschermann and Florian Frohn and Jera Hensel and J{\"{u}}rgen 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}, }
  4. Franck Cassez, Takashi Matsuoka, Edward Pierzchalski, and Nathan Smyth. Perentie: Modular Trace Refinement and Selective Value Tracking (Competition Contribution). In Proc. TACAS, LNCS 9035, pages 439-442, 2015. Springer. Link to this entry
    BibTeX Entry
    @inproceedings{PERENTIE-COMP15, author = {Franck Cassez and Takashi Matsuoka and Edward Pierzchalski and Nathan 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}, }
  5. Caterina Urban. FuncTion: An Abstract Domain Functor for Termination (Competition Contribution). In Proc. TACAS, LNCS 9035, pages 464-466, 2015. Springer. Link to this entry
    BibTeX Entry
    @inproceedings{FUNCTION-COMP15, author = {Caterina 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}, }
  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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{CPAREC-COMP15, 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{SMACKCORRAL-COMP15, 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. Alexander Nutz, Daniel Dietsch, Mostafa Mahmoud Mohamed, and Andreas 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{KOJAK-COMP15, author = {Alexander Nutz and Daniel Dietsch and Mostafa Mahmoud Mohamed and Andreas 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{PREDATOR-COMP15, 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. Pablo Gonzalez-de-Aledo and Pablo Sanchez. FramewORk for Embedded System verificaTion (Competition Contribution). In Proc. TACAS, LNCS 9035, 2015. Springer. Link to this entry
    BibTeX Entry
    @inproceedings{FOREST-COMP15, author = {Pablo Gonzalez-de-Aledo and Pablo Sanchez}, title = {FramewORk for Embedded System verificaTion (Competition Contribution)}, booktitle = {Proc.\ TACAS}, year = {2015}, series = {LNCS~9035}, publisher = {Springer}, }
  11. Wei Wang and Clark Barrett. Cascade (Competition Contribution). In Proc. TACAS, LNCS 9035, pages 420-422, 2015. Springer. Link to this entry
    BibTeX Entry
    @inproceedings{CASCADE-COMP15, author = {Wei Wang and Clark Barrett}, title = {Cascade (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {420-422}, year = {2015}, series = {LNCS~9035}, publisher = {Springer}, }
  12. Ermenegildo Tomasco, Omar Inverso, Bernd Fischer, Salvatore La Torre, and Gennaro 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. Link to this entry
    BibTeX Entry
    @inproceedings{MUCSEQ-COMP15, author = {Ermenegildo Tomasco and Omar Inverso and Bernd Fischer and Salvatore {La~Torre} and Gennaro 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}, }
  13. Truc L. Nguyen, Bernd Fischer, Salvatore La Torre, and Gennaro 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{ULAZYCSEQ-COMP15, author = {Truc L. Nguyen and Bernd Fischer and Salvatore {La~Torre} and Gennaro 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{CPACHECKER-COMP15, 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. Arie Gurfinkel, Temesghen Kahsai, and Jorge 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{SEAHORN-COMP15, author = {Arie Gurfinkel and Temesghen Kahsai and Jorge 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{AUTOMIZER-COMP15, 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 Link to this entry 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{CPACHECKER-COMP14, 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{CBMC-COMP14, 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{CPALIEN-COMP14, 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{CSEQLAZY-COMP14, 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. Link to this entry
    BibTeX Entry
    @inproceedings{CSEQMU-COMP14, 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}, }
  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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{ESBMC-COMP14, 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. Link to this entry
    BibTeX Entry
    @inproceedings{FBIT-COMP14, 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}, }
  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. Link to this entry
    BibTeX Entry
    @inproceedings{PREDATOR-COMP14, 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}, }
  10. J. Slaby and J. Strejček. Symbiotic 2: More Precise Slicing (Competition Contribution). In Proc. TACAS, LNCS 8413, pages 415-417, 2014. Springer. Link to this entry
    BibTeX Entry
    @inproceedings{SYMBIOTIC-COMP14, 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}, }
  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. Link to this entry
    BibTeX Entry
    @inproceedings{AUTOMIZER-COMP14, 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}, }
  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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{KOJAK-COMP14, author = {E.~Ermis and A.~Nutz and D.~Dietsch and J.~Hoenicke and A.~Podelski}, title = {Ultimate {K}ojak (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 Link to this entry 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{CPACHECKEREXPLICIT-COMP13, 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{CPACHECKERSEQCOM-COMP13, 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. Link to this entry
    BibTeX Entry
    @inproceedings{PREDATOR-COMP13, 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}, }
  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. Link to this entry
    BibTeX Entry
    @inproceedings{SYMBIOTIC-COMP13, 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}, }
  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. Link to this entry
    BibTeX Entry
    @inproceedings{CSEQ-COMP13, 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}, }
  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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{UFO-COMP13, 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. Link to this entry
    BibTeX Entry
    @inproceedings{LLBMC-COMP13, 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}, }
  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. Link to this entry
    BibTeX Entry
    @inproceedings{THREADER-COMP13, 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}, }
  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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{ESBMC-COMP13, 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. Link to this entry
    BibTeX Entry
    @inproceedings{ULTIMATE-COMP13, 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 {A}utomizer with {SMTInterpol} (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {641-643}, year = {2013}, series = {LNCS~7795}, publisher = {Springer}, }

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 Link to this entry 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. Link to this entry
    BibTeX Entry
    @inproceedings{PREDATOR-COMP12, 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}, }
  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. Link to this entry
    BibTeX Entry
    @inproceedings{BLAST-COMP12, 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}, }
  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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{CPACHECKERMEMO-COMP12, 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{ESBMC-COMP12, 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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{LLBMC-COMP12, 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. Link to this entry
    BibTeX Entry
    @inproceedings{WOLVERINE-COMP12, 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}, }
  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 Link to this entry Publisher's Version PDF
    BibTeX Entry
    @inproceedings{CPACHECKERABE-COMP12, author = {S.~L{\"{o}}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. Link to this entry
    BibTeX Entry
    @inproceedings{SATABS-COMP12, 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}, }
  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. Link to this entry
    BibTeX Entry
    @inproceedings{FSHELL-COMP12, 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}, }
  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. Link to this entry
    BibTeX Entry
    @inproceedings{QARMC-COMP12, 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}, }