SAT
SAT is the question whether a given Boolean formula can be evaluated to true by assigning variables to true or false. Many important real-world problems (e.g. verification of hard- or software) can be formulated as SAT problem. In the last ten years a quite active SAT community arose and tries to find efficient algorithm to solve this problem (so called SAT solvers). By the way: SAT is known to be a hard problem (NP complete problem).
Software Verification
With the help of software verification one tries to assure that software (or parts of it) fully satisfy all the expected requirements. There are two fundamental approaches to verification: (1) test-driven verification, where programs are fed with different test cases. The problem is obvious: you can never know if the program is really doing what it should or you just forget the corresponding test case. (2) static verification, where we prove the correctness of a program with the help of mathematical methods. This method is clearly more reliable but also harder to perform.
Computer Algebra & Symbolic Computation
Computer Algebra and Symbolic Computation are the direct opposites to numerical mathematics. CA or SC systems manipulate mathematical equations and expressions in symbolic form, as opposed to manipulating the approximations of specific numerical quantities represented by those symbols. CA and SC can be used to solve a variety of problems e.g. in biology or verification.
Project MathLang
The meaning of a (mathematical) text can not be easily grasped by a machine. Therefore we have to provide additional information together with the original text. MathLang is a framework for computerizing such mathematical text by marking special structures in the text. MathLang tries to keep the computerization as close as possible to the mathematician’s text while at the same time providing a formal structure supporting mathematical software systems (e.g. computer algebra systems, theorem provers, etc.).