This module contains an instruction set simulator for the Abacus processor It also considers the main memory and a configurable data cache.

This module implements functions for working with automata, in particular, determinizing them by the subset and the breakpoint constructions, as well as converting omega-automata to other acceptance conditions. Automata are represented in either a fully explicit enumeration of their states and transitions, a fully symbolic representation, or a semi-symbolic one.

This module implements functions for generating some special boolean functions like arithmetic circuits for addition, subtraction, multiplication, threshold functions, the hidden weighted bit functions, the queen's problem, and the pigeonhole problems.

This file implements functions for generating computer arithmetic ciruits. The overall idea is that the circuit is generated as a side effect when calling a generator function with input bitvectors. The generator function is thereby given the input and output bitvectors as string[]. This way, also circuits for arithmetic expressions can be generated.

This file implements functions for radix integer arithmetic

This module implements data types and functions to reason about dataflow process networks. Among others, there are functions to classify a node concerning sequentiality, (weak) endochrony, Kahn criteria and to run a network of nodes on a given input state.

This module implements algorithms for analyzing dataflow process networks. In particular, for static DPNs it can decide whether there is a static periodic schedule and whether the DPN is bounded, and for dynamic DPNs, it can compute the product firing table for the entire DPN and can decide about the (weak) endochrony and Kahn criteria of its nodes.

The functions in this module implement algorithms for encoding a given alphabet of letters based on the Shannon-Fano, Huffman, and arithmetic encodings as well as functions for linear encodings and CRC error checksums.

This module implements some functions for context-free grammars and parser generators.

This module implements a teaching tool for dealing with graphs.

This file implements algorithms about interconnection and sorting networks used in computer systems. In particular, there are functions to determine the configurations of Beneš and Banyan networks with 2-way switches. Since routing is a special case of sorting (where only permutations are considered), we also consider sorting networks as interconnection networks. In particular, Batcher's Bitonic and OddEven divide/sort/merge based networks are considered, with the isomorphic version of Parberry's pairwise sorting network, and also Dowd's periodic balanced network that allows the reuse of the periodic block. For all of these configurations, there are functions to write the resulting network in form of SVG images. There is also a function to verify whether a given comparator network is a sorting network, and also a function to determine a

This module implements functions to generate SMV files for synthesizing correct sorting/splitter networks for a given number of inputs and a desired depth. Further options are found by the global variables below.

This module implements functions for checking (bi)simulation relations of labeled transition systems (Kripke structures). It also computes quotients and products of Kripke structures.

 This module contains functions around the Mastermind board game like some
 well-known strategies like the MinMax, Entropy, ExpectedSize and MaxParts
 strategies.
 Mastermind is a simple two-player code-breaking board game invented in 1970
 by Mordecai Meirowitz, an Israeli postmaster and telecommunications expert.
 It may have been inspired by moo, a program developed by J.M. Grochow at MIT
 in the late 1960s.
 In the game, one player is the codemaker and the other is the codebreaker.
 The codemaker secretly selects a code consisting of an ordered sequence of
 four colors (c_1,c_2,c_3,c_4), each chosen from a set of six possible colors,
 with repetitions allowed. The codebreaker then tries to guess the code by
 repeatedly proposing a sequence of colors (g_1,g_2,g_3,g_4). After each
 guess, the codemaker tells the codebreaker two numbers (b,w): the number of
 correct colors in the correct positions (p) and the number of colors that
 are part of the code but not in the correct positions (w). For example, if
 the code is (1,2,3,3) and the codebreaker's guess is (3,2,4,3), then the
 codemaker's response would be (2,1), since the codebreaker has guessed the
 2 and the second 3 correctly and in the correct positions, while having
 guessed the first 3 correctly but in the wrong position.
  The codebreaker continues guessing until she guesses the code correctly or
 until she reaches a maximum allowable number of guesses without having
 correctly identified the secret code.
 Note that w can be computed as w=(sum_(i=1)^numColors min(c_i,g_i))-b,
 where c_i is the number of times the color i is in the code and g_i is the
 number of times it is in the guess.

This module implements functions for compiling MiniC to cmd programs, performing dataflow analysis, displaying CFGs, and generating code for Abacus.

This module implements functions for global and local model checking of mu-calculus and CTL formulas of explicitly defined Kripke structures. It also provides functions for some Kripke structure examples like the NIM game.

This module implements functions for verification of safety properties using induction; in particular functions for incremental induction as used in property directed reachability (PDR). In contrast to reals PDR implementation that are based on SAT solvers (and clause sets), this version is based on BDDs.

This module implements functions for checking whether a given binary relation satisfies some properties of partial orders, directed sets, and lattices. It is restricted, however, to finite relations and sets.

This module implements functions for dealing with propositional logic like computing truth tables, evaluating formulas by truth assignments, computing canonical CNF and DNF and the sequent calculus.

This module first implements functions and data types for generating an extended finite state machine for a given Quartz program (without module calls). Furthermore, functions to generate verification conditions are provided which are based on induction on the EFSM states and strongly connected components.

This module implements

This module implements functions for solving parity games with Zielonka's algorithm.

This module implements functions for scheduling the code of a basic block to a SCAD machine with a given number of universal processing units. Note that the problem is NP-complete!

This module implements teaching tools for scheduling algorithms.

This module implements a form that can be configured to collect student opinions.

This module implements teaching tools for linear temporal logic

This module implements algorithms checking properties of ternary functions.

This module implements functions to classify a threaded execution according to various weak memory consistency models.