Whats the advantage of having FLOSS tools for open proofs?
Technological advancements in formal methods (FM) tools are sometimes held back by lack of published code. For example, “The Evolution from LIMMAT to NANOSAT”,Technical Report #444 by Armin Biere (Dept. Computer Science, ETH Z¨urich, CH-8092 Z¨urich, Switzerland, Computer System Institute, April 2004) reports that their efforts to “cross check the impressive results the authors of CHAFF” had problems. “From the publications alone, without access to the source code, various details were still unclear… what we did not realize, and which hardly could be deduced from the literature, was [an optimization] employed in GRASP and CHAFF… Only [when CHAFF’s source code became available did] our unfortunate design decision became clear… The lesson learned is, that important details are often omitted in publications and can only be extracted from source code. It can be argued, that making source code of SAT solvers available is as important to the advancement of the field as publications”. F
