[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS] New article type PROOF PEARLS in Journal of Automated Reasoning

Journal of Automated Reasoning is very happy to announce the new article type of

*Proof Pearls*.

The goal of *Proof Pearls* is to disseminate insights gleaned from the growing body of machine-checked formalizations and proofs, obtained using both interactive and automated methods. Application areas include the full range from pure mathematics and logic to software and hardware verification. Proof pearls should be short communications that focus on a few central ideas rather than extended research reports. Contributions may include:

o a short, elegant proof of a self-standing result

o a novel way of defining a fundamental concept

o a notable approach to proving a key lemma in a larger development

o a snippet of verified code, carefully engineered to balance efficiency
with ease of verification

o a clever or impressive application of automated tools in a particular domain

*Proof Pearls* adapt Jon Bentley's notion of a "programming pearl" to the verification paradigm. Proof pearls should thus encapsulate fundamental insights that are adaptable and reusable, while being elegant and satisfying in their own right. Typical examples could be a verification of Huffman's algorithm, a perspicuous proof of the fundamental theorem of algebra, or a novel axiomatization of a particular algebraic system that was discovered using automated methods.

Submissions will undergo the usual refereeing process, and will be evaluated according to expository and theoretical merit. Systems and formalizations should be made available online.

We look forward to your submissions
Tobias Nipkow