Boolean Satisfiability (SAT) solvers are now routinely used in the verification of large industrial problems. However, their application in safety-critical domains such as the railways, avionics, and automotive industries requires some form of assurance for the results, as the solvers can (and sometimes do) have bugs. Unfortunately, the complexity of modern, highly optimized SAT solvers renders impractical the development of direct formal proofs of their correctness. This paper presents an alternative approach where an untrusted, industrial-strength, SAT solver is plugged into a trusted, formally certified, SAT proof checker to provide industrial-strength certified SAT solving. The key novelties and characteristics of our approach are (i) that the checker is automatically extracted from the formal development, (ii), that the combined system can be used as a standalone executable program independent of any supporting theorem prover, and (iii) that the checker certifies any SAT solver respecting the agreed format for satisfiability and unsatisfiability claims. The core of the system is a certified checker for unsatisfiability claims that is formally designed and verified in Coq. We present its formal design and outline the correctness proofs. The actual standalone checker is automatically extracted from the the Coq development. An evaluation of the certified checker on a representative set of industrial benchmarks from the SAT Race Competition shows that, albeit it is slower than uncertified SAT checkers, it is significantly faster than certified checkers implemented on top of an interactive theorem prover.

De novo Sequencing of peptides is a challenging task in proteome research. Whilethere exist reliable DNAsequencing methods, the highthroughput denovo sequencing of proteins by mass spectrometry is still an open problem. Current approaches suffer from a lack in precision to detect mass peaks in the spectrograms. In this paper we present a novel method for de novo peptide sequencing based on a hidden Markov model. Experiments effectively demonstrate that this new method significantly outperformsstandard approaches in matching quality.

Clustering aims at extracting hidden structure in dataset. While the problem offinding compact clusters has been widely studied in the literature, extractingarbitrarily formed elongated structures is considered a much harder problem. In this paper we present a novel clustering algorithm whichtackles the problem by a two step procedure: first the data are transformed in such a way that elongated structures become compact ones. In a second step, these new objects are clustered by optimizing a compactness-based criterion. The advantages of the method over related approaches are threefold: (i) robustness properties of compactness-based criteria naturally transfer to the problem of extracting elongated structures, leadingto a model which is highly robust against outlier objects; (ii) the transformed distances induce a Mercer kernel which allows us to formulate a polynomial approximation scheme to the generally N P-hard clustering problem; (iii) the new method does not contain free kernel parameters in contrast to methods like spectral clustering or mean-shift clustering.

Machine learning has reached a point where many probabilistic methods can be understood as variations, extensions and combinations of a much smaller set of abstract themes, e.g., as different instances of the EM algorithm. This enables the systematic derivation of algorithms customized for different models.

Machine learning has reached a point where many probabilistic methods can be understood as variations, extensions and combinations of a much smaller set of abstract themes, e.g., as different instances of the EM algorithm. This enables the systematic derivation of algorithms customized for different models.

Machine learning has reached a point where many probabilistic methods canbe understood as variations, extensions and combinations of a much smaller set of abstract themes, e.g., as different instances of the EM algorithm. This enables the systematic derivation of algorithms customized fordifferent models. Here, we describe the AUTOBAYES system which takes a high-level statistical model specification, uses powerful symbolic techniques based on schema-based program synthesis and computer algebra to derive an efficient specialized algorithm for learning that model, and generates executable code implementing that algorithm. This capability is far beyond that of code collections such as Matlab toolboxes oreven tools for model-independent optimization such as BUGS for Gibbs sampling: complex new algorithms can be generated without newprogramming, algorithms can be highly specialized and tightly crafted for the exact structure of the model and data, and efficient and commented code can be generated for different languages or systems.

The Association for the Advancement of Artificial Intelligence, in cooperation with Stanford University's Department of Computer Science, presented the 2002 Spring Symposium Series, held Monday through Wednesday, 25 to 27 March 2002, at Stanford University. The nine symposia were entitled (1) Acquiring (and Using) Linguistic (and World) Knowledge for Information Access; (2) Artificial Intelligence and Interactive Entertainment; (3) Collaborative Learning Agents; (4) Information Refinement and Revision for Decision Making: Modeling for Diagnostics, Prognostics, and Prediction; (5) Intelligent Distributed and Embedded Systems; (6) Logic-Based Program Synthesis: State of the Art and Future Trends; (7) Mining Answers from Texts and Knowledge Bases; (8) Safe Learning Agents; and (9) Sketch Understanding.

The Association for the Advancement of Artificial Intelligence, in cooperation with Stanford University's Department of Computer Science, presented the 2002 Spring Symposium Series, held Monday through Wednesday, 25 to 27 March 2002, at Stanford University. The nine symposia were entitled (1) Acquiring (and Using) Linguistic (and World) Knowledge for Information Access; (2) Artificial Intelligence and Interactive Entertainment; (3) Collaborative Learning Agents; (4) Information Refinement and Revision for Decision Making: Modeling for Diagnostics, Prognostics, and Prediction; (5) Intelligent Distributed and Embedded Systems; (6) Logic-Based Program Synthesis: State of the Art and Future Trends; (7) Mining Answers from Texts and Knowledge Bases; (8) Safe Learning Agents; and (9) Sketch Understanding.