scientific article; zbMATH DE number 6687732

MaRDI QIDQ2963878zbMATH OpenFDO

Authors Nikolay V. Shilov, Evgeny V. Bodin, S. O. Shilova

Publication date 21 February 2017

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

zbMATH Keywords

Hoare triplesystem computer programverifying compiler

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Verifying Array Programs by Transforming Verification Conditions
• Artificial Intelligence and Symbolic Computation
• Simplifying the Verification of Quantified Array Assertions via Code Transformation
• Transformational Verification of Parameterized Protocols Using Array Formulas
• A type-theoretic semantics of arrays
• Verifying array manipulating programs with full-program induction
• scientific article; zbMATH DE number 4049004
• Scaling bounded model checking by transforming programs with arrays
• Array Abstractions from Proofs

Describes a project that uses

Uses Software

• F@BOOL@

This page was built for publication:

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