LogoopenSUSE Build Service > Projects
Sign Up | Log In

Alt-Ergo automatic theorem prover

Alt-Ergo is an automatic theorem prover dedicated to program verification. Alt-Ergo is based on CC(X) a congruence closure algorithm parameterized by an equational theory X. Currently, CC(X) can be instantiated by the empty equational theory and by the linear arithmetics. Alt-Ergo contains also a home made SAT-solver and an instantiation mechanism. Its architecture is summarized by the the following picture.

Source Files (show merged sources derived from linked package)

Filename Size Changed Actions
alt-ergo-0.95.2.tar.gz 228 KB almost 5 years ago Download File
alt-ergo.changes 1001 Bytes almost 5 years ago Download File
alt-ergo.spec 1.99 KB almost 5 years ago Download File

Comments for home:lorenz:formal (0)

Login required, please login or signup in order to comment