Ponencia
Proving and Computing: Applying Automated Reasoning to the Verification of Symbolic Computation Systems
Autor/es | Ruiz Reina, José Luis |
Departamento | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial |
Fecha de publicación | 2014 |
Fecha de depósito | 2019-05-15 |
Publicado en |
|
ISBN/ISSN | 978-3-319-13769-8 0302-9743 |
Resumen | The application of automated reasoning to the formal verification
of symbolic computation systems is motivated by the need of
ensuring the correctness of the results computed by the system, beyond
the classical approach ... The application of automated reasoning to the formal verification of symbolic computation systems is motivated by the need of ensuring the correctness of the results computed by the system, beyond the classical approach of testing. Formal verification of properties of the implemented algorithms require not only to formalize the properties of the algorithm, but also of the underlying (usually rich) mathematical theory. We show how we can use ACL2, a first-order interactive theorem prover, to reason about properties of algorithms that are typically implemented as part of symbolic computation systems. We emphasize two aspects. First, how we can override the apparent lack of expressiveness we have using a first-order approach (at least compared to higher-order logics). Second, how we can execute the algorithms (efficiently, if possible) in the same setting where we formally reason about their correctness. Three examples of formal verification of symbolic computation algorithms are presented to illustrate the main issues one has to face in this task: a Gr¨obner basis algorithm, a first-order unification algorithm based on directed acyclic graphs, and the Eilenberg-Zilber algorithm, one of the central components of a symbolic computation system in algebraic topology. |
Cita | Ruiz Reina, J.L. (2014). Proving and Computing: Applying Automated Reasoning to the Verification of Symbolic Computation Systems. En AISC 2014: 12th International Conference on Artificial Intelligence and Symbolic Computation (1-6), Sevilla, España: Springer. |
Ficheros | Tamaño | Formato | Ver | Descripción |
---|---|---|---|---|
Proving and Computing.pdf | 116.6Kb | [PDF] | Ver/ | |