iSAT-parallel (Picoso)

 

Subproject

H1/2

Categories

Core algorithms, Model checker / solver for hybrid systems

Overview

Same features as iSAT, but allows usage of more than one CPU core to speed up the solving process.

Publications

N. Kalinnik, E. Abraham, T. Schubert, R. Wimmer, and B. Becker. Exploiting different strategies for the parallelization of an SMT solver. In Manfred Dietrich, editor, GI/ITG/GMM Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen", pages 97-106, 2010.

N. Kalinnik, T. Schubert, E. Abraham, R. Wimmer, and B. Becker. Picoso - A parallel interval constraint solver. In Hamid R. Arabnia, editor, In International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA), pages 473-479, 2009. 

Benchmarks

iSAT Benchmarks, HySAT Benchmarks, ETCS Train System

Download

Picoso requires MPICH¹ libraries and environment to run correctly. Due to its specific requirements (paths, environment variables and daemons, ...) we do not provide a binary of Picoso.

¹ MPICH is an implementation of the "Message Passing Interface" standard.

Manual

---

Status

Prototype