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

DOI10.1007/978-3-662-49498-1_3zbMATH Open1335.68044OpenAlexW2420279234MaRDI QIDQ2802468FDOQ2802468

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

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

Mathematics Subject Classification ID

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

Cites Work

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

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

Uses Software

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

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)