PV1 ⊧ VeriAbs: Verification by Abstractionperforms several predefined analyses on C programs to make them compatible with a bounded model checker

Links

• SV-Comp'17: 115.113.148.49/VeriAbs.htm (dysfunctional)
• SV-Comp'18: https://gitlab.com/sosy-lab/sv-comp/archives/-/blob/master/2018/veriabs.zip
• SV-Comp'18: http://www.cmi.ac.in/~madhukar/veriabs/VeriAbs.zip
• SV-Comp'19: https://gitlab.com/sosy-lab/sv-comp/archives-2020/tree/master/2020/veriabs.zip (wrong URL in the paper)
• GitHub: https://github.com/divyeshunadkat/VAJRA (VAJRA and TILER are integrated and are claimed as the source of success of VeriAbs at SV-Comp'20)
• Last commit date: 20 Feb 2020 (default branch)
• Last commit date: 20 Feb 2020 (last activity)

Related papers

• VeriAbs: Verification by Abstraction (Competition Contribution) (TACAS'17 tool)
• VeriAbs: Verification by Abstraction and Test Generation (TACAS'18 tool)
• VeriAbs : Verification by Abstraction and Test Generation (Competition Contribution) (TACAS'20 tool)
• Verifying Array Manipulating Programs with Full-Program Induction (TACAS'20 full paper)

Last publication date

Related tools

• PRISM*
• CBMC*
• CPAchecker*
• VAJRA*
• TILER*

ProVerB specific

• Markdown description: view/edit
• Reason for this entry: TACAS 2020
• Contained in the ProVerB22 dataset (paper + artefact)