Home Research USI Group Tools Teaching Service Funding

Software

    All of these tools were realized with significant contributions by various colleagues and in particular by Ph.D. students

    Model Checkers

    UpProver

    SMT-based incremental bounded model-checking

    FunFrog

    SAT-based bounded model checker using interpolation-based function summaries

    eVolCheck

    SAT-based bounded model checker with upgrade checking capabilities

    SMTS

    Parallel Software Model Checker

    HiFrog

    SMT-based Bounded Model Checker for C with Function Summaries

    Booster

    Verifier for programs with arrays

    Verige

    SAFARI

    Model checker for programs with arrays

    LoopFrog

    Loop summarization based static analyzer for C programs

    Computational Solvers

    Golem

    Constrained Horn Clause Solver

    OpenSMT

    Compact and open-source SMT-solver written in C++

    PeRIPLO

    SAT-solver capable of proof manipulation and interpolant generation

    PVAIR

    Interpolator that supports Partial Variable Assignment Interpolants (PVAIs)