Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach

DOI10.1007/978-3-662-49498-1_3MaRDI QIDQ2802468zbMATH OpenOpenAlexFDO

Authors Cláudio Belo Lourenço, Jorge Sousa Pinto, Maria João Frade

Publication date 26 April 2016

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL http://repositorio.inesctec.pt/handle/123456789/4534

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Recommendations

• A unified approach of program verification
• Extraction and verification of programs by analysis of formal proofs
• scientific article; zbMATH DE number 1796136
• Computer Science Logic
• Automating relatively complete verification of higher-order functional programs

Cites work

• scientific article; zbMATH DE number 194642 (Why is no real title available?)
• scientific article; zbMATH DE number 3351184 (Why is no real title available?)
• An axiomatic basis for computer programming
• Avoiding exponential explosion: generating compact verification conditions
• Efficient weakest preconditions
• Forward with Hoare
• Hoare logic and auxiliary variables
• Proving total correctness of recursive procedures
• Soundness and Completeness of an Axiom System for Program Verification
• Ten Years of Hoare's Logic: A Survey—Part I
• The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
• Tools and Algorithms for the Construction and Analysis of Systems
• Why3 -- where programs meet provers

Cited in

(3)

• A verified VCGen based on dynamic logic: an exercise in meta-verification with Why3
• Instrumenting a weakest precondition calculus for counterexample generation
• Static single assignment form for massage-passing programs

Describes a project that uses

Uses Software

• WhyML
• Boogie
• Frama-C
• Spec#
• Why3
• ACSL
• KRAKATOA
• SPARK

This page was built for publication: Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach

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