Using computer algebra techniques for the specification, verification and synthesis of recursive programs

DOI10.1016/j.matcom.2008.11.017zbMath1183.68757OpenAlexW2003319485MaRDI QIDQ1025311

Tudor Jebelean, Nikolaj Popov

Publication date: 18 June 2009

Published in: Mathematics and Computers in Simulation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.matcom.2008.11.017

zbMATH Keywords

computer algebraprogram synthesisspecification and verification

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Specification and verification (program logics, model checking, etc.) (68Q60)

Uses Software

• Coq
• Mathematica
• Theorema
• PVS

Cites Work

• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• \textit{Theorema}: Towards computer-aided mathematical theory exploration
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Using computer algebra techniques for the specification, verification and synthesis of recursive programs