This module implements functions for working with automata, in particular, determinizing them by Rabin-Scott and the Breakpoint construction, as well as converting omega-automata to other acceptance conditions.

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.

This module implements global functions and constants for the teaching tools.

This module

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 file 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 symbolic model checking of mu-calculus and temporal logics. The model checking algorithms are mainly implemented by means of BDDs. There is also a function for symbolic computation of predecessor and successor states using quantifier elimination.

This module implements functions for parsing propositional logic and temporal logic formulas by simplifying the functions provided in Averest.

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.