Project

General

Profile

Actions

Feature #6747

closed

Support UAtomizer as one of Klever verification back-ends

Added by Evgeny Novikov almost 9 years ago. Updated almost 8 years ago.

Status:
Rejected
Priority:
Immediate
Assignee:
-
Category:
-
Target version:
-
Start date:
02/03/2016
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

At the moment just CPAchecker is involved quite well.


Related issues 2 (1 open1 closed)

Is duplicate of Klever - Feature #7799: Integrate Ultimate Automizer as an alternative verification toolClosedIlja Zakharov12/13/2016

Actions
Blocks Klever - Feature #6552: Implement Cluster SchedulerNewIlja Zakharov01/28/2016

Actions
Actions #1

Updated by Ilja Zakharov almost 9 years ago

  • Priority changed from Normal to High
Actions #2

Updated by Vadim Mutilin almost 9 years ago

According to SV-COMP results http://sv-comp.sosy-lab.org/2016/results/results-verified/DeviceDriversLinux64.table.html
except CPAchecker (3177 points) and BLAST (2704) good candidates are
  • UAtomizer (2686)
  • smack+corral (2206)
  • LPI[CPAchecker] (2107)
  • ESBMC+depthk (2009)
  • CBMC (1972)
  • SeaHorn (1694)
Actions #3

Updated by Alexey Khoroshilov almost 9 years ago

Is it make sense to take a look at some subset of the tasks or to use some other scheme of scoring?
Is it easy enough?

Actions #4

Updated by Evgeny Novikov almost 9 years ago

Alexey Khoroshilov wrote:

Is it make sense to take a look at some subset of the tasks or to use some other scheme of scoring?
Is it easy enough?

This feature request is to just try several static verifiers other than CPAchecker. I assume that there will be several issues due to our current strict relation with CPAchecker. Finally it should be possible to run any verifier participated in SV-COMP but likely just those which participated in the device driver category is fair enough.

Everything else should be done outside this feature request.

Actions #5

Updated by Evgeny Novikov almost 8 years ago

  • Subject changed from Try a couple of other static verifiers to Support UAtomizer as one of Klever verification back-ends
  • Category deleted (Scheduling)
  • Status changed from New to Open
  • Assignee set to Ilja Zakharov
  • Priority changed from High to Immediate
Actions #6

Updated by Evgeny Novikov almost 8 years ago

  • Status changed from Open to Rejected
  • Assignee deleted (Ilja Zakharov)

Duplicates #7799 that looks more appropriate.

Actions

Also available in: Atom PDF