1 resultado para Classical methods
em Instituto Politécnico do Porto, Portugal
Filtro por publicador
- KUPS-Datenbank - Universität zu Köln - Kölner UniversitätsPublikationsServer (1)
- Acceda, el repositorio institucional de la Universidad de Las Palmas de Gran Canaria. España (2)
- AMS Tesi di Dottorato - Alm@DL - Università di Bologna (4)
- AMS Tesi di Laurea - Alm@DL - Università di Bologna (1)
- Aquatic Commons (2)
- ArchiMeD - Elektronische Publikationen der Universität Mainz - Alemanha (2)
- Aston University Research Archive (5)
- Biblioteca de Teses e Dissertações da USP (2)
- Biblioteca Digital da Produção Intelectual da Universidade de São Paulo (4)
- Biblioteca Digital da Produção Intelectual da Universidade de São Paulo (BDPI/USP) (3)
- Biblioteca Digital de Teses e Dissertações Eletrônicas da UERJ (2)
- BORIS: Bern Open Repository and Information System - Berna - Suiça (6)
- Boston University Digital Common (1)
- Bulgarian Digital Mathematics Library at IMI-BAS (6)
- CaltechTHESIS (5)
- Cambridge University Engineering Department Publications Database (20)
- CentAUR: Central Archive University of Reading - UK (10)
- Chinese Academy of Sciences Institutional Repositories Grid Portal (10)
- Cochin University of Science & Technology (CUSAT), India (2)
- Coffee Science - Universidade Federal de Lavras (1)
- CORA - Cork Open Research Archive - University College Cork - Ireland (1)
- Corvinus Research Archive - The institutional repository for the Corvinus University of Budapest (1)
- Dalarna University College Electronic Archive (1)
- Deakin Research Online - Australia (2)
- Digital Commons - Michigan Tech (1)
- Digital Commons at Florida International University (3)
- DigitalCommons@University of Nebraska - Lincoln (1)
- DRUM (Digital Repository at the University of Maryland) (1)
- Duke University (1)
- eResearch Archive - Queensland Department of Agriculture; Fisheries and Forestry (38)
- Glasgow Theses Service (1)
- Helda - Digital Repository of University of Helsinki (104)
- Indian Institute of Science - Bangalore - Índia (182)
- Instituto Politécnico de Bragança (3)
- Instituto Politécnico do Porto, Portugal (1)
- Martin Luther Universitat Halle Wittenberg, Germany (1)
- Massachusetts Institute of Technology (1)
- National Center for Biotechnology Information - NCBI (3)
- Publishing Network for Geoscientific & Environmental Data (1)
- QUB Research Portal - Research Directory and Institutional Repository for Queen's University Belfast (9)
- Queensland University of Technology - ePrints Archive (454)
- Repositório Alice (Acesso Livre à Informação Científica da Embrapa / Repository Open Access to Scientific Information from Embrapa) (1)
- Repositório Institucional da Universidade de Aveiro - Portugal (1)
- Repositório Institucional UNESP - Universidade Estadual Paulista "Julio de Mesquita Filho" (24)
- Research Open Access Repository of the University of East London. (1)
- RUN (Repositório da Universidade Nova de Lisboa) - FCT (Faculdade de Cienecias e Technologia), Universidade Nova de Lisboa (UNL), Portugal (1)
- Scielo España (1)
- Universidad de Alicante (6)
- Universidad del Rosario, Colombia (2)
- Universidad Politécnica de Madrid (9)
- Universidade Complutense de Madrid (1)
- Universidade de Lisboa - Repositório Aberto (1)
- Universidade Federal do Pará (2)
- Universidade Federal do Rio Grande do Norte (UFRN) (5)
- Universitätsbibliothek Kassel, Universität Kassel, Germany (3)
- Université de Montréal (1)
- Université de Montréal, Canada (4)
- University of Michigan (3)
- University of Queensland eSpace - Australia (3)
- University of Washington (2)
- Worcester Research and Publications - Worcester Research and Publications - UK (2)
Resumo:
This paper presents a mechanically verified implementation of an algorithm for deciding the equivalence of Kleene algebra terms within the Coq proof assistant. The algorithm decides equivalence of two given regular expressions through an iterated process of testing the equivalence of their partial derivatives and does not require the construction of the corresponding automata. Recent theoretical and experimental research provides evidence that this method is, on average, more efficient than the classical methods based on automata. We present some performance tests, comparisons with similar approaches, and also introduce a generalization of the algorithm to decide the equivalence of terms of Kleene algebra with tests. The motivation for the work presented in this paper is that of using the libraries developed as trusted frameworks for carrying out certified program verification.