Project

General

Profile

Actions
Copy link

Feature #1969

open

Concurrent forward exploration at each node

Added by Pavel Shved about 13 years ago.

Status:
New
Priority:
Normal
Assignee:
-
Category:
-
Target version:
-
Start date:
11/06/2011
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

Cartesian Abstraction used in BLAST involves checks if each of the candidate predicates is implied by postcondition of an operation. These checks are independent for each predicate. Therefore, they should be made concurrent.

Of course, it's just a parody of fully-distributed state exploration algorithm, but at least it should be easier to fit this into BLAST, which gets very useful on programs with a lot of predicates per location.

The main issue here is that OCaml and SMP concurrency are not close friends. :-(

No data to display

Actions
Copy link

Also available in: Atom PDF