SAEPTUM: verification of ELAN hardware specifications using the proof assistant PVS. Rewriting and Rewriting-Logic have been used in several applications, including specification, formal verification and construction of proof assistants. Previous works explored hardware specification and modeling using the rewriting-logic system ELA. Experiences proved this to be very effective, but certainly restricted as a tool for formal verification of the correctness of the given hardware specifications. Although simple, verification had to be done exhaustively and manually, which indicated the need of automating this process. We present SAEPTUM, a methodology and tool for the verification of rewrite specifications created in ELAN, via the translation to the proof assistant PVS and automatic generation of critical pair based correction criteria.
Keywords for this software
References in zbMATH (referenced in 2 articles )
Showing results 1 to 2 of 2.
- Galdino, André L.; Ayala-Rincón, Mauricio: A formalization of the Knuth-Bendix(-Huet) critical pair theorem (2010)
- L. Galdino, André; Ayala-Rincón, Mauricio: A PVS theory for term rewriting systems (2009)