Deductive formal verification of search programs in arrays of arbitrary size for abstract register machines

zbMATH Open1374.68276MaRDI QIDQ2979871FDOQ2979871

Authors: Dmitri A. Chkliaev, V. A. Nepomnyashchij 

Publication date: 26 April 2017

Full work available at URL: http://bulletin.iis.nsk.su/files/article/chklaev_nepomniaschy.pdf

Recommendations

• Formal verification of programs for abstract register machines
• Formal Methods at the Crossroads. From Panacea to Foundational Support
• scientific article; zbMATH DE number 2102724
• A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification
• Algorithmic analysis of array-accessing programs

zbMATH Keywords

interactive theorem provingformal specificationrandom-access machineabstract register machinesearch programverification system PVS

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Uses Software

• PVS

This page was built for publication: Deductive formal verification of search programs in arrays of arbitrary size for abstract register machines

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2979871)