Projects

CVC4

CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination.

OpenBricks

OpenBricks is an enterprise-grade embedded Linux framework that provides easy creation of custom distributions for industrial embedded devices. It features a complete embedded development kit for rapid deployment on x86, ARM, PowerPC and MIPS systems with support for industry leaders. Pick your ... [More] device, select your software bricks and cook your product ! OpenBricks reduces development efforts by abstracting the low-level interface to your device. It supports all Khronos industry standards (OpenGL|ES, OpenVG, OpenMAX …) and major applicative frameworks (Qt, GTK, EFL, SDL) for you to only focus on your end-user application. OpenBricks is an OpenSource framework. It’s the masterpiece framework behind your next design product. OpenBricks currently sustains the GeeXboX project. [Less]

Cunei Machine Translation Platform

Cunei is a data-driven machine translation system that builds dynamic, statistical models based on instances of known translations found in a corpus.

moses-for-mere-mortals

This site offers a set of Bash scripts and Windows executables add-ins that, together, create a basic translation chain prototype able of processing very large corpora. It uses Moses, a widely known statistical machine translation system. The idea is to help build a translation chain for the real ... [More] world, but it should also enable a quick evaluation of Moses for actual translation work and guide users in their first steps of using Moses. The scripts cover the installation, the creation of representative test files, the training, the translation, the scoring and the transfer of trainings between persons or between several Moses installations. A Help/Short Tutorial (http://moses-for-mere-mortals.googlecode.com/files/Help.odt) and a demonstration corpus (too small for doing justice to the qualitative results that can be achieved with Moses, but able of giving a realistic view of the relative duration of the steps involved) are available. Two Windows add-ins allow the creation of Moses input files from *.TMX translation memories (Extract_TMX_Corpus.exe), as well as the creation of *.TMX files from Moses output files (Moses2TMX.exe). A synergy between machine translation and translation memories is therefore created. The scripts were tested in Ubuntu 9.04 (64-bit version). Documents used for corpora training should be perfectly aligned and saved in UTF-8 character encoding. Documents to be translated should also be in UTF-8 format. One would expect the users of these scripts, perhaps after having tried the provided demonstration corpus, to immediately use and get results with the real corpora they are interested in. Though already tested and used in actual work, this should be considered a work in progress. So as to protect the users not yet completely acquainted with Moses, these scripts try to avoid mistakes that would cost them dearly in terms of time and/or results, but do not completely insulate them (especially from the consequences of malformed corpora files). [Less]

csisat

CSIsat is an interpolating decision procedure for the quantifier-free theory of rational linear arithmetic and equality with uninterpreted function symbols. Our implementation combines the efficiency of linear programming for solving the arithmetic part with the efficiency of a SAT solver to reason ... [More] about the boolean structure. CSIsat Project Home PagePlease visit the CSIsat Project Home Page DocumentationTool paper at CAV 2008: CSIsat: A Tool for LA+EUF Interpolation Proc. CAV'08, LNCS 5123, pages 304-308, Springer-Verlag, 2008. API and source code documentation Tutorial coming soon. Quick reference DownloadsThe download list provides archived source code and binaries for released versions Check out the latest version To build from source code, read the installation instructions Problem ReportsMail to: Dirk Beyer (first.last@sfu.ca) or Damien Zufferey (first.last@epfl.ch) AcknowledgementsWe thank many other people for their contributions. [Less]

simple-sat-solver

simple SAT and SMT solver written in Java

simplesmt

A SMT processor in SimpleScalar. CS696 course project.

extract-tmx-corpus

Extract-Tmx-Corpus is a Windows program (Vista and XP supported) that enables translators not necessarily with a deep knowledge of linguistic tools to create highly customised corpora that can be used with the Moses machine translation system and with other systems. In order to create corpora ... [More] that are most useful to train machine translation systems, one should strive to include segments that are relevant for the task in hand. One of the ways of finding such segments could involve the usage of previous translation memory files (TMX files). This way the corpora could be customised for the person or for the type of task in question. The present program uses such files as input. The program can create strictly aligned corpora for a single pair of languages, several pairs of languages or all the pairs of languages contained in the TMX files. The program creates 2 separate files (UTF-8 format; Unix line endings) for each language pair that it processes: one for the starting language and another for the destination language. The lines of a given TMX translation unit are placed in strictly the same line in both files. The program suppresses empty TMX translation units, as well as those where the text for the first language is the same as that of the second language (like translation units consisting solely of numbers, or those in which the first language segment has not been translated into the second language). If you are interested in another format of corpus, it should be relatively easy to adapt this format to the format you are interested in. The program also informs about errors that might occur during processing and creates a file that lists the name(s) of the TMX files that caused them, as well as a separate one listing the files successfully treated and the number of segments extracted for the language pair. [Less]