Integrated approach to analysis and verification of imperative programs

MaRDI QIDQ2979818zbMATH OpenFDO

Authors Igor S. Anureev

Publication date 26 April 2017

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

zbMATH Keywords

C-kernelC-lightdomain-specific languageprogram analysisprogram modelprogram verificationverification system

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Algebraic Methodology and Software Technology
• A language-based approach to functionally correct imperative programming
• Programmable verifiers in imperative programming
• Static Analysis
• On automated program construction and verification

Cited in

(9)

• Integration of verification methods for program systems
• Efficient verification of imperative programs using auto2
• Program verification with interacting analysis plugins
• A language-based approach to functionally correct imperative programming
• Introduction to the Atoment language
• Programmable verifiers in imperative programming
• scientific article; zbMATH DE number 7364137 (Why is no real title available?)
• Characteristic formulae for the verification of imperative programs
• Algebraic Methodology and Software Technology

Describes a project that uses

Uses Software

• Isabelle
• ACSL
• Why3
• Spec#
• OpenJML
• Atoment
• Boogie
• PVS
• JML
• Frama-C
• C-Light

This page was built for publication: Integrated approach to analysis and verification of imperative programs

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