ETAPS 2016: 2-8 April 2016, Eindhoven, The Netherlands

TACAS 2016 Competition on Software Verification - Presentation

Thursday, April 7th
16h30 - 18h00 Room: TBD
(chair: Dirk Beyer)
  • Dirk Beyer. SV-COMP-Report: Reliable and Reproducible Competition Results with BenchExec and Witnesses
  • Peter Schrammel and Daniel Kroening. 2LS for Program Analysis
  • Vadim Mutilin, Mikhail Mandrykin and Pavel Shved. Predicate Analysis with BLAST 2.7.3
  • Daniel Kroening and Michael Tautschnig. CBMC -- C Bounded Model Checker
  • Dexi Wang, Chao Zhang, Guang Chen, Fei He, Ming Gu and Jiaguang Sun. Ceagle: An LLVM-based C Program Verifier
  • Manchun Zheng, John G. Edenhofner, Ziqing Luo, Mitchell J. Gerrard, Michael S. Rogers, Matthew B. Dwyer and Stephen F. Siegel. CIVL: Applying a General Concurrency Verification Framework to C/Pthreads Programs
  • Karlheinz Friedberger. Block-Abstraction Memoization with Value Analysis and Predicate Analysis in CPAchecker
  • Matthias Dangl. Bit-Precise k-Induction with Continuously-Refined Invariant Generation in CPAchecker
  • Williame Rocha, Herbert Rocha, Lucas Cordeiro and Bernd Fischer. Verification and Refutation using Witness Checker in ESBMC+DepthK v2.1
  • Vladimír Štill, Petr Rockai and Jiri Barnat. DIVINE: Explicit-State LTL Model Checker
  • Mikhail Ramalho, Jeremy Morse, Lucas Cordeiro and Denis Nicole. Improved loop unwinding in ESBMC 2.1
  • Lukas Holik, Martin Hruska, Ondrej Lengal, Adam Rogalewicz, Jiri Simacek and Tomas Vojnar. Run Forester, Run Backwards!
  • Olli Saarikivi and Keijo Heljanko. LCTD: Tests-Guided Proofs for C Programs on LLVM
  • Egor George Karpenkov. Software Verification with Local Policy Iteration
  • Herbert O. Rocha, Raimundo Barreto and Lucas Cordeiro. Hunting Memory Bugs in C Programs with Map2Check
  • Michal Kotoun, Petr Peringer, Veronika Šokova and Tomas Vojnar. Predator Hunting Party Revisited
  • Montgomery Carter, Pantazis Deligiannis, Alastair F. Donaldson, Michael Emmi, Shaobo He, Akash Lal, Shaz Qadeer, Zvonimir Rakamaric and Jonathan Whitaker. SMACK+Corral: A Modular Verifier
  • Marek Chalupa, Martin Jonas, Jiri Slaby, Jan Strejcek and Martina Vitovska. Symbiotic 3 - New Slicer and Error-Witness Generation
  • Matthias Heizmann, Daniel Dietsch, Marius Greitschus, Jan Leike, Betim Musa, Claus Schätzle and Andreas Podelski. Ultimate Automizer with Two-track Proofs
  • Henning Günther, Alfons Laarman and Georg Weissenbacher. Vienna Verification Tool: Parallel Software with IC3