Software developed at the Software Science Group

The research at the software science group has led to a variety of open-source tools that span the different research areas of the group. The following list gives an overview, details can be found on the individual tool pages.

Functional Programming and Workflow Management

• The functional programming language Clean is, like Haskell, a pure and lazy functional language, additionally offering some special feautures like Uniqueness Typing, a hybride type system offering dynamics in addition to static typing, and support for type-driven generic functions. The compiler is very fast, and it generates excellent code.
  
  
• iTask is a toolkit for building web-based workflow management systems using a powerful workflow language embedded in Clean
  
  
• The mTask system is a framework for programming complete IoT systems from a single source.The framework is powered by a multi-backend tagless embedded DSL embedded in the pure functional programming language Clean.With the bytecode generation backend and the iTask integration, mTask tasks can be embedded in iTask programs and shared data sources can be synchronized.The client runtime system runs on embedded devices such as Arduino/ESPxxx/Nucleo boards or on regular devices running linux, windows or mac.Traditionally IoT architectures are tiered architectures where different languages, protocols and paradigms are used in different layers.The mTask system generates all tiers from a single source specification.
• SAPL To enable the execution of applications written in a functional language in a browser, we have an option to compile functional programs to JavaScript. Originally it has been developed to allow the execution of iTask tasks written in Clean on clients.
  Laszlo Domoszlai has made a stand-alone version enabling both Clean as well Haskell functions to be compiled to JavaScript such that they can be executed in the browser. It uses an interpreter technique invented by Jan-Martin Jansen.

Automata Learning

• TOMTE is a tool that fully automatically constructs abstractions for automata learning. Usually, a component implementing the learning algorithm (the learner) is directly connected to the SUT (the teacher). By observing how the SUT responds to queries sent by the learner, a model of the behavior of the SUT can be constructed.
  

Program Verification and Automated Theorem Proving

• Iris is a framework for program verification using higher-order concurrent separation logic, embedded in the Coq proof assistant. Iris involves active collaboration with (among others) Aarhus University, BedRock Systems, Boston College, CNRS/LRI, Groningen University, INRIA, ITU Copenhagen, KU Leuven, Microsoft Research, MIT, MPI-SWS, NYU, Saarland University, and Vrije Universiteit Brussel, and has been applied to languages like Rust, Go, OCaml, C, Scala, and more.
  
  
• std++ is an extended "Standard Library" for Coq, with extensive support for common data structures like lists, sets, maps, multisets. The development of std++ is led by Robbert Krebbers (Radboud University) and Ralf Jung (MPI-SWS), and has an active number of contributors.

Testing

• TorXakis, an experimental model-based testing tool, based on the ioco-testing theory for labelled transition systems.
  
  

Probabilistic System Verification

• Storm is a modern probabilistic model-checker developed primarily at the RWTH Aachen University and the Radboud University.