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

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)

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

Cited In (1)

• Formal verification of programs for abstract register machines

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)