Department of Information Technology
Department of Information Technology
Uppsala UniversityInformation TechnologyResearchUPMARC
Listen

NEW

UPMARC Posters
4posters-200x146.jpg

UPMARC, the Uppsala Programming for Multicore Architectures Research Center

UPMARC Tools

  • UPPAAL - A model checker for real-time and embedded systems, developed jointly between Uppsala University and Aalborg University (Denmark).
  • Dialyzer - A static analysis tool that identifies software discrepancies such as definite type errors, data race conditions, interface violations in callback modules, code which has become dead or unreachable due to some programming error, unnecessary tests, etc. in single Erlang modules or entire (sets of) applications. For a number of years now, the Dialyzer tool is part of the Erlang/OTP distribution.
  • Concuerror - A systematic testing tool (aka. stateless model checker) for concurrent Erlang programs.
  • Nidhugg - A stateless model checker for programs in C/pthreads under the SC, TSO or PSO memory models.
  • Memorax - A model checker and automatic memory fence synthesis tool for parallel programs running under the TSO, PSO or VIPS memory models.
  • PARALUTION - A library for iterative solvers.
    This library enables you to perform various sparse iterative solvers and preconditioners on multi/many-core CPU and GPU devices. Based on C++, it provides a generic and flexible design which allows seamless integration with other scientific software packages. PARALUTION is listed as a CUDA-Accelerated Library
  • SuperGlue - A C++ library for task-parallelism, with data-dependent tasks.
  • FMM2D - An adaptive general fast multipole method in 2 dimensions, with a nice Matlab-interface.
    Has a fully ported GPU-version, which supports NVIDIA's CUDA and is highly configurable.
  • URDME - A modular framework for simulation of stochastic reaction and diffusion (R&D) processes on two- or three-dimensional unstructured meshes
    The main routine is operated within MATLAB in combination with COMSOL Multiphysics, while the core solvers are compiled at runtime and accessed as assembliess for efficiency.
  • Princess - A theorem prover designed for program verification.
    Princess is tailored to the combination of first-order logic and integer arithmetic, and provides, e.g., sophisticated treatment of quantifiers, generalised forms of quantifier elimination, and the ability to compute Craig interpolants. In 2012, Princess won in the category TFA (arithmetic problems) of the theorem prover competition CASC.
  • Psi-Calculi Workbench - A generic and parametric tool for process calculi specifications, allowing symbolic execution and bisimulation checking for processes that may contain both unicast and wireless broadcast communication. The tool also provides a supporting library for implementing new psi-calculus instances.
  • Eldarica - A model checker for solving systems of Horn constraints, developed in collaboration with researchers at EPFL Lausanne.
    The use of Horn constraints as intermediate representation of programs has recently been proposed as a promising direction to extend the reach of automated verification methods to concurrent programs, and to programs with procedures and recursion, among others.
  • Cache Pirate - A tool that measures application sensitivity to shared cache allocation. The Cache Pirate "steals" shared cache from a co-running application to measure how much the application's performance suffers as a function of its shared cache allocation. The Cache Pirate has been implemented internally by Ericsson for evaluation of their base station software and won the best paper award at the 40th International Conference on Parallel Processing.

Updated  2016-10-25 15:34:17 by Bengt Jonsson.