Select a WP



A SAT-Based Polynomial Space Algorithm for Answer Set Programming, that deals with any (non disjunctive) logic program, works on SAT formulas without additional variables, and is guaranteed to work in polynomial space.

Download link.

klase wp: 4.3


C-Plan is a SAT-Based Conformant Planner. It takes as input a Conformant Planning problem description in the action language "C" and an integer n, and returns the shortest conformant plan of length less than or equal n, or NO is there is no such conformant plan.

Homepage: C-Plan

klase wp: 4

MBP: a Model Based Planner

The Model Based Planner (MBP) is a system designed to perform plan synthesis, plan validation and plan/domain simulation in non-deterministic domains. It provides: a general framework for modeling nondeterministic domains with various degrees of observability, and a language to support it; a general plan model, and a language supporting it with powerful primitives; plan validation capabilities, expressing plan validation as a model checking problem; a set of efficient algorithms that perform plan synthesis for a variety of classes of planning problems; a means for simulation of domains, in isolation or driven by plans. MBP assumes a simple but general model of non-determinism, which encompasses uncertainty on the initial situation, on the action effects, and on the state in which the actions will be executed.

Homepage: MBP

Download link.

klase wp: 4,4.2


MathSAT is a DPLL-based decision procedure for the SMT problem for various theories, including those of Equality and Uninterpreted Function (EUF), Separation Logic (SEP), Linear Arithmetic over the Reals (LA(R)) and Linear Arithmetic over the Integers (LA(Z)).

Homepage: MathSAT

Download link.

klase wp: 3,3.5

NuSMV: a new symbolic model checker

NuSMV is a reimplementation and extension of SMV, the first model checker based on BDDs. NuSMV has been designed to be an open architecture for model checking, which can be reliably used for the verification of industrial designs, as a core for custom verification tools, as a testbed for formal verification techniques, and applied to other research areas.

Homepage: NuSMV

Download link.

klase wp: 3,3.4,3.5

OPTSAT (OPTimal SATisfiability)

OPTSAT is a DLL based SAT solver tuned for optimization problems like MAX-SAT or MIN-ONE

Homepage: OPTSAT

klase wp: 4.3

QuBE (Quantifier Boolean Encoder)

QuBE is an efficient solver for deciding the satisfiability of QBFs.

Homepage: QuBE

klase wp: 3.5,4.5

QuEnC (Quantifier Encoder for model Checking)

QuEnC is a tool for bounded model checking that translate a qltl problem into a quantified boolean formula

Homepage: QuEnC

klase wp: 3.5

SIMO (Satisfiability Internal Modules)

SIM is a library of efficient procedures for propositional satisfiability (SAT) problems.

Homepage: SIMO

klase wp: 3.5,4.5

T-Tool: The Formal Tropos Tool

T-Tool provides a framework for the effective use of formal methods in the early requirements phase. The framework allows for the formal and mechanized analysis of early requirements specifications expressed in a formal modeling language.

Homepage: T-Tool

Download link.

klase wp: 3,3.4


TSAT++ is an open platform for Satisfiability Modulo Theories (SMT); the current version of TSAT++ is tailored for an instance of SMT, called Separation Logic

Homepage: TSAT++

klase wp: 4.3

WS-TV: Web Service Timed Verification

WS-TV is part of the ASTRO toolset. It is a prototype tool that supports the verification of time-related properties of Web Service compositions.

Homepage: WS-TV

klase wp: 3,7

WS-VERIFY: A Web Service Composition Verification Tool

WS-VERIFY (Web Service Composition Verification Tool) is part of the ASTRO toolset. It is a tool aimed at providing techniques that allow for detecting problems at design time. The designer implements its processes in a suitable language, e.g., BPEL4WS. Given this set of processes, and a set of business requirements, the WS-VERIFY tool allows to check whether the requirements are violated. If this is the case, an error flow, i.e., a flow of interaction that causes the problem is reported to the developer that can modify the BPEL4WS process and re-iterate the verification step.

Homepage: WS-Verify

klase wp: 3,7


WS-monitor is part of the ASTRO toolset. It extends the standard process monitoring capabilities of an industrial-strength Web Service execution engine, ActiveBPEL. WS-monitor allows to trace the run-time behavior of WS-processes described in the BPEL language, to detect violations with respect to a set of behavioral properties, and to report these deviations in a convenient format.

Homepage: WS-monitor

Download link.

klase wp: 4,7


WS-syntools is part of the ASTRO toolset. It exploits "Planning via Model Checking" techniques to support the automated generation of Web service compositions. WS-syntools extends the standard "Planning via Model Checking" algorithms in order to manage asynchronous interactions among Web Services. Moreover it implements advanced techniques, based on knowledge-level planning, to manage data types with unbounded ranges, such as thoese typically used in Web Service interactions.

Homepage: WS-syntools

Download link.

klase wp: 4,7


WS-translator is part of the ASTRO toolset. It allows for translating specifications of WS-processes expressed in the BPEL lanaguage into finite-state models. WS-translator supports different target languages, including State-Transition Systems, the SMV language, and Java code. WS-translator can be used as a front-end to WS-monitor and to WS-synthols.

Homepage: WS-translator

Download link.

klase wp: 7