Main.HomePage History

Hide minor edits - Show changes to output - Cancel

September 24, 2013, at 02:17 PM by 192.168.156.40 -
September 24, 2013, at 02:16 PM by 192.168.156.40 -
Changed lines 39-40 from:
Unfortunately, we no longer develop, maintain, and distribute [=SystemC2C=] because
to:
Due to a number of requests for [=SystemC2C=], we regret to say
that, unfortunately
, we no longer develop, maintain, and distribute [=SystemC2C=] because
September 24, 2013, at 02:15 PM by 192.168.156.40 -
Changed line 45 from:
encode SystemC models. We provide the benchmarks in our download section.
to:
encode [=SystemC=] models. We provide the benchmarks in our download section.
September 24, 2013, at 02:14 PM by 192.168.156.40 -
Changed lines 37-38 from:
!! Info on SystemC2C
to:
!! Info on [=SystemC2C=]
Changed line 41 from:
In particular SystemC2C relies on Pinapa front-end, that is no longer maintained
to:
In particular [=SystemC2C=] relies on [=Pinapa=] front-end, that is no longer maintained
September 24, 2013, at 02:13 PM by 192.168.156.40 -
Added lines 37-49:
!! Info on SystemC2C

Unfortunately, we no longer develop, maintain, and distribute [=SystemC2C=] because
it relies on old tools that are no longer maintained/available on our system.
In particular SystemC2C relies on Pinapa front-end, that is no longer maintained
by its developers, and an old version of [=GCC=], that is no longer installed on our system.

You can still use Kratos to verify sequential and threaded C benchmarks that
encode SystemC models. We provide the benchmarks in our download section.
Moreover, because Kratos is constantly under development, we have not released
a newer version of it. So, we suggest that you try the Kratos executable
used in our latest paper that is list in the publication section (the download
link is provided in the paper).
December 04, 2012, at 02:29 PM by Iman Narasamdya -
Changed lines 9-10 from:
* ''lazy predicate abstraction'' (Blast algorithm)
* ''lazy abstraction with interpolants'' ([=McMillan=] algorithm)
to:
* ''Lazy Predicate Abstraction'' (Blast algorithm) and
*
''Lazy Abstraction with Interpolants'' ([=McMillan=]/Impact algorithm)
December 04, 2012, at 02:11 PM by Iman Narasamdya -
Changed lines 10-12 from:
* ''lazy abstraction with interpolants'' ([= McMillan=] algorithm)

to:
* ''lazy abstraction with interpolants'' ([=McMillan=] algorithm)

Changed line 14 from:
* ''Explicit-Scheduler/Symbolic-Threads'' ([=ESST=]) and
to:
* ''Explicit-Scheduler/Symbolic-Threads'' ('''[=ESST=]''') and
Changed line 17 from:
ESST combines explicit-state model checking techniques for analyzing
to:
[=ESST=] combines explicit-state model checking techniques for analyzing
Changed line 19 from:
abstraction for analyzing the threads. That is, ESST keeps track of
to:
abstraction for analyzing the threads. That is, [=ESST=] keeps track of
Changed lines 23-24 from:
S3ST is built on ESST for handling designs with parametric interactions
between the threads and the scheduler. S3ST combines the explicit part
to:
[=S3ST=] is built on [=ESST=] for handling designs with parametric interactions
between the threads and the scheduler. [=S3ST=] combines the explicit part
Changed lines 27-31 from:
Both ESST and S3ST have been specialized to [= SystemC =] verification.
In the sense that ESST and S3ST implements [= SystemC =] scheduling policy and
(subset of) [= SystemC =] synchronization functions. ESST, in particular,
has also been specialized to [= FairThreads =] verification.
to:
Both [=ESST=] and [=S3ST=] have been specialized to [=SystemC=] verification.
In the sense that [=ESST=] and [=S3ST=] implements [=SystemC=] scheduling policy and
(subset of) [=SystemC=] synchronization functions. [=ESST=], in particular,
has also been specialized to [=FairThreads=] verification.
Changed line 33 from:
Promela or to NuSMV models, and from threaded programs to Promela models.
to:
[=Promela=] or to [=NuSMV=] models, and from threaded programs to [=Promela=] models.
December 04, 2012, at 02:08 PM by Iman Narasamdya -
Changed lines 10-12 from:
* ''lazy abstraction with interpolants'' ([= McMillan =] algorithm)

to:
* ''lazy abstraction with interpolants'' ([= McMillan=] algorithm)

Changed lines 14-15 from:
* ''Explicit-Scheduler/Symbolic-Threads'' ([= '''ESST''' =]) and
* ''Semi-Symbolic-Scheduler/Symbolic-Threads'' ([= '''S3ST''' =]) algorithms.
to:
* ''Explicit-Scheduler/Symbolic-Threads'' ([=ESST=]) and
* ''Semi-Symbolic-Scheduler/Symbolic-Threads'' ('''[=S3ST=]''') algorithms.
December 04, 2012, at 02:07 PM by Iman Narasamdya -
Changed lines 10-12 from:
* ''lazy abstraction with interpolants'' (McMillan algorithm)

to:
* ''lazy abstraction with interpolants'' ([= McMillan =] algorithm)

Changed lines 14-15 from:
* ''Explicit-Scheduler/Symbolic-Threads'' ([= ESST =]) and
* ''Semi-Symbolic-Scheduler/Symbolic-Threads'' ([= S3ST =]) algorithms.
to:
* ''Explicit-Scheduler/Symbolic-Threads'' ([= '''ESST''' =]) and
* ''Semi-Symbolic-Scheduler/Symbolic-Threads'' ([= '''S3ST''' =]) algorithms.
December 04, 2012, at 02:07 PM by Iman Narasamdya -
Changed lines 14-15 from:
* ''Explicit-Scheduler/Symbolic-Threads'' ('''ESST''') and
* ''Semi-Symbolic-Scheduler/Symbolic-Threads'' ('''S3ST''') algorithms.
to:
* ''Explicit-Scheduler/Symbolic-Threads'' ([= ESST =]) and
* ''Semi-Symbolic-Scheduler/Symbolic-Threads'' ([= S3ST =]) algorithms.
December 04, 2012, at 02:06 PM by Iman Narasamdya -
Changed lines 7-9 from:
For analysis of sequential programs, Kratos implements
'''lazy predicate abstraction''' (Blast algorithm) and
'''lazy abstraction with interpolants''' (McMillan algorithm).
to:

For analysis of sequential programs, Kratos implements
* ''lazy predicate abstraction'' (Blast algorithm)
* ''lazy abstraction with interpolants'' (McMillan algorithm)

Changed lines 14-15 from:
'''Explicit-Scheduler/Symbolic-Threads''' (ESST) and
'''Semi-Symbolic-Scheduler/Symbolic-Threads'''(S3ST) algorithms.
to:
* ''Explicit-Scheduler/Symbolic-Threads'' ('''ESST''') and
* ''
Semi-Symbolic-Scheduler/Symbolic-Threads'' ('''S3ST''') algorithms.
December 04, 2012, at 02:03 PM by Iman Narasamdya -
December 04, 2012, at 02:02 PM by Iman Narasamdya - Update decription of Kratos to follow its current status
Changed lines 4-13 from:
Kratos is a software model checker for [= SystemC =]. Currently, it only
verifies safety properties in the form
of program assertion.
Kratos provides two different analyses for verifying [= SystemC =] designs:
sequential
and concurrent analyses. The sequential analysis
is based on the lazy predicate abstraction and relies on the translation
from [= SystemC =] designs to sequential C programs.
The concurrent analysis is based on the ESST algorithm that combines
''Explicit'' state techniques to handle
the [= SystemC =] ''Scheduler''
with ''Symbolic'' techniques based on lazy predicate abstraction to handle
the
''Threads''
.
to:
Kratos is a software model checker for sequential and (cooperative)
threaded C programs. Kratos verifies safety properties in the
form
of program assertion.
For analysis of sequential programs, Kratos implements
'''lazy predicate abstraction''' (Blast algorithm)
and
'''lazy abstraction with interpolants''' (McMillan algorithm).
For analysis of threaded programs, Kratos implements
'''Explicit-Scheduler/Symbolic-Threads''' (ESST) and
'''Semi-Symbolic-Scheduler/Symbolic-Threads'''(S3ST) algorithms.

ESST combines explicit-state model checking techniques for analyzing
the scheduler and symbolic techniques based on lazy predicate
abstraction for analyzing the threads. That is, ESST keeps track of

the scheduler states explicitly and orchestrate the whole verification
by direct executions of the scheduler (i.e.,
the scheduler is part
of the model checking algorithm, and not part of design under verification)
.
S3ST is built on ESST for handling designs with parametric interactions
between the threads and the scheduler. S3ST combines the explicit part
of executions with symbolically-represented set of scheduler states.

Both ESST and S3ST have been specialized to [= SystemC =] verification.
In the sense that ESST and S3ST implements [= SystemC =] scheduling policy and
(subset of) [= SystemC =] synchronization functions. ESST, in particular,
has also been specialized to [= FairThreads =] verification.

Kratos can also perform translations from sequential programs to
Promela or to NuSMV models, and from threaded programs to Promela models.
Currently, Kratos only handles a subset of C language. Extending
Kratos to handle a large subset of C constructs are in progress.

Changed line 1 from:
(:Title Kratos :)
to:
(:Title Overview :)
Deleted lines 2-3:

!!Overview
Added lines 2-3:
(:Description Kratos's main page :)
Added line 1:
(:Title Kratos :)
Deleted lines 0-2:
(:Title Kratos -- A Software Model Checker for [= SystemC =]:)
(:Description Kratos' short web page:)

Deleted lines 12-29:

!!Downloads

Kratos consists of two executables that run under Linux machine:

# [[https://es.fbk.eu/tools/kratos/downloads/swchecker|swchecker]] implements the sequential analysis.
# [[https://es.fbk.eu/tools/kratos/downloads/cswchecker|cswchecker]] implements the concurrent analysis.

Documents related to Kratos are the following:

# [[https://es.fbk.eu/tools/kratos/downloads/manual.pdf|Manual]].
# [[https://es.fbk.eu/tools/kratos/downloads/tool.pdf|Architecture]] (a tool paper submitted for publication).

!!Benchmarks

# [[https://es.fbk.eu/tools/kratos/downloads/benchmarks.tgz|Benchmarks]] for swchecker.
# [[https://es.fbk.eu/tools/kratos/downloads/cbenchmarks.tgz|Benchmarks]] for cswchecker.

January 17, 2011, at 05:25 PM by Iman Narasamdya -
Deleted line 33:
[[~Iman Narasamdya]]
January 17, 2011, at 05:24 PM by Iman Narasamdya -
Changed lines 13-16 from:
Explicit state techniques to handle the [= SystemC =] Scheduler
with Symbolic techniques based on lazy predicate abstraction to handle the
Threads.
to:
''Explicit'' state techniques to handle the [= SystemC =] ''Scheduler''
with ''Symbolic'' techniques based on lazy predicate abstraction to handle the
''Threads''.
Added lines 33-34:

[[~Iman Narasamdya]]
January 17, 2011, at 05:01 PM by Iman Narasamdya - Kratos' short web page
Changed lines 1-12 from:
Welcome to PmWiki!

A local copy of PmWiki's
documentation has been installed along with the software,
and
is available via the [[PmWiki/documentation index]].  

To continue setting up PmWiki, see [[PmWiki/initial setup tasks]]
.

The [[PmWiki/basic editing]] page describes how to create pages
in PmWiki.
  You can practice editing in the [[wiki sandbox]].

More information about PmWiki is available from http://www.pmwiki.org
.
to:
(:Title Kratos -- A Software Model Checker for [= SystemC =]:)
(:Description Kratos' short web page:)

!!Overview

Kratos
is a software model checker for [= SystemC =]. Currently, it only
verifies safety properties in the form of program assertion
.
Kratos provides two different analyses for verifying [= SystemC =] designs:
sequential and concurrent analyses. The sequential analysis
is based on the lazy predicate abstraction and relies on the translation
from [= SystemC =] designs to sequential C programs.
The concurrent analysis is based on the ESST algorithm that combines
Explicit state techniques to handle the [= SystemC =] Scheduler
with Symbolic techniques based on lazy predicate abstraction to handle the
Threads.

!!Downloads

Kratos consists of two executables that run under Linux machine:

# [[https://es.fbk.eu/tools/kratos/downloads/swchecker|swchecker]] implements the sequential analysis.
# [[https://es.fbk.eu/tools/kratos/downloads/cswchecker|cswchecker]] implements the concurrent analysis.

Documents related to Kratos are the following:

# [[https://es.fbk.eu/tools/kratos/downloads/manual.pdf|Manual]].
# [[https://es.fbk.eu/tools/kratos/downloads/tool.pdf|Architecture]] (a tool paper submitted for publication).

!!Benchmarks

# [[https://es.fbk.eu/tools/kratos/downloads/benchmarks.tgz|Benchmarks]] for swchecker.
# [[https://es.fbk.eu/tools/kratos/downloads/cbenchmarks.tgz|Benchmarks]] for cswchecker
.


Page last modified on September 24, 2013, at 02:17 PM