Output details
11 - Computer Science and Informatics
University of Sheffield
Algebraic Notions of Termination
<10> This international collaboration initiates a new algebraic approach to modular termination conditions for programs and software systems. It uses extensions of Kleene algebras, which are fundamental mathematical structures for program analysis and verification. It generalises termination analysis techniques that are used, e.g., by Microsoft for device driver verification (Terminator). The results have been elaborated in three successor journal papers (2 JLAP, 1 ENTCS) and several successor conference publications, including work on non-termination analysis and implementations in theorem proving environments. Its different versions (journal, preprint and conference) have 29 GoogleScholar citations.