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

DOI10.1007/978-3-662-49498-1_3zbMath1335.68044OpenAlexW2420279234MaRDI QIDQ2802468

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

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

Related Items (2)

Instrumenting a weakest precondition calculus for counterexample generation ⋮ A verified VCGen based on dynamic logic: an exercise in meta-verification with Why3

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Efficient weakest preconditions
• Proving total correctness of recursive procedures
• The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
• Hoare logic and auxiliary variables
• Forward with Hoare
• Ten Years of Hoare's Logic: A Survey—Part I
• Soundness and Completeness of an Axiom System for Program Verification
• Avoiding exponential explosion
• Tools and Algorithms for the Construction and Analysis of Systems
• Why3 — Where Programs Meet Provers
• An axiomatic basis for computer programming

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