Copyright 1999-2000 VA Linux Systems, Inc. Tue, 06 Jan 2009 9:39:18 GMT Gforge Full Project Listing http://gforge.avacs.org Gforge Full Project Listing webmaster@gforge.avacs.org en-us MiraXT http://gforge.avacs.org/projects/miraxt/ The goal of this project is to further improve MiraXT, a thread-based parallel SAT algorithm to take advantage of current and future shared memory multiprocessor systems. Stochastic Bounded Model Checking http://gforge.avacs.org/projects/sbmc/ The goal of this project is to generate counterexamples for Markov chains using bounded model checking when invariant properties are violated. SiSAT http://gforge.avacs.org/projects/sisat/ The SiSAT tool is an extension of the iSAT solver to deal with existential and randomized quantification of finite-domain variables. S3 WP1 T4 FM Driven Prob. Model Checking http://gforge.avacs.org/projects/femke/ The tool FEMKE gets system model (DTMC<=X<=CTMDP) and fault model to build stack of MC, each a scenario in fault-env. While batch-processing with PRISM, regions of attraction are found which can be further refined for asym appr optimal spot. BMX - BMC of Blackbox Designs http://gforge.avacs.org/projects/bmx/ BMX is a Bounded Model Checker for blackbox designs relying on 01X-logic and QBF. RPMC - prob. MC mit exakter Arithmetik http://gforge.avacs.org/projects/rpmc/ RPMC is a model checker for probabilistic transition systems using exact rationals. Its general purpose is the investigation of the impact of rounding in probabilistic model checking. HySAT http://gforge.avacs.org/projects/hysat/ HySAT: A Bounded Model Checker for Hybrid Systems Signature-based Bisimulation Computation http://gforge.avacs.org/projects/sigref/ Sigref provides a generic algorithm for the symbolic computation of bisimulations on transition systems. iMIRA http://gforge.avacs.org/projects/imira/ This project contains two variants of the iMira solver: The first is able to decide Boolean combinations of linear equations and inequations. The second (also called iSat2) decides - for cases this is possible - also non-linear logics. Linear Integer/Real Arithmetic Solver http://gforge.avacs.org/projects/lira/ LIRA is an automata-based solver (including parsers for various input formats) for the linear integer/real arithmetic, i.e. FOL(R, Z, +, <). First Order Model Checker http://gforge.avacs.org/projects/fomc/ AVACS H3 First Order Model Checking Site News Admin http://gforge.avacs.org/projects/newsadmin/ This project manages AVACS News. Please report problems in the Site Admin project. Site Admin http://gforge.avacs.org/projects/siteadmin/ Gforge Management Project. Please report problems/requests here.