Verification conditions for source-level imperative programs
From MaRDI portal
Hoare logicprogram verificationweakest preconditionsupdatesprogram annotationsverification conditions
Research exposition (monographs, survey articles) pertaining to computer science (68-02) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)
Recommendations
- Generation of correctness conditions for imperative programs
- Verification conditions are code
- Effective generation of verification conditions for non-deterministic unstructured programs
- Verification Condition Generation Via Theorem Proving
- Building verification condition generators by compositional extension
Cites work
- scientific article; zbMATH DE number 1612488 (Why is no real title available?)
- scientific article; zbMATH DE number 1693527 (Why is no real title available?)
- scientific article; zbMATH DE number 1706329 (Why is no real title available?)
- scientific article; zbMATH DE number 439891 (Why is no real title available?)
- scientific article; zbMATH DE number 3748393 (Why is no real title available?)
- scientific article; zbMATH DE number 44976 (Why is no real title available?)
- scientific article; zbMATH DE number 3574936 (Why is no real title available?)
- scientific article; zbMATH DE number 1142325 (Why is no real title available?)
- scientific article; zbMATH DE number 1500648 (Why is no real title available?)
- scientific article; zbMATH DE number 3995020 (Why is no real title available?)
- scientific article; zbMATH DE number 1832224 (Why is no real title available?)
- scientific article; zbMATH DE number 1841809 (Why is no real title available?)
- scientific article; zbMATH DE number 3302923 (Why is no real title available?)
- scientific article; zbMATH DE number 3351184 (Why is no real title available?)
- scientific article; zbMATH DE number 3410595 (Why is no real title available?)
- A Tutorial on Satisfiability Modulo Theories
- Abstract Interpretation of Symbolic Execution with Explicit State Updates
- Affine relationships among variables of a program
- An axiomatic basis for computer programming
- Automated deduction for verification
- Automatic program verification. I: A logical basis and its implementation
- Avoiding exponential explosion: generating compact verification conditions
- Computer aided verification. 19th international conference, CAV 2007, Berlin, Germany, July 3--7, 2007. Proceedings.
- Efficient weakest preconditions
- Grammar Analysis and Parsing by Abstract Interpretation
- Handbook of philosophical logic. Volume II: Extensions of classical logic
- Hoare logic and auxiliary variables
- Hoare logic for Java in Isabelle/HOL
- Inference Rules for Program Annotation
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Isabelle/HOL. A proof assistant for higher-order logic
- Logical analysis of programs
- Mechanical proofs about computer programs
- Satisfiability modulo theories: an appetizer
- Secure information flow by self-composition
- Secure mechanical verification of mutually recursive procedures
- Simplify: a theorem prover for program checking
- Software model checking
- Specification and verification challenges for sequential object-oriented programs
- Specifying Software
- Ten Years of Hoare's Logic: A Survey—Part I
- The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
- The derivation of systolic computations
- Theorem-proving support in programming language semantics
- Theories of Programming Languages
- Theory and Applications of Satisfiability Testing
- Weakest pre-condition reasoning for Java programs with JML annotations
- \textsf{CC(X)}: semantic combination of congruence closure with solvable theories
Cited in
(13)- Efficient weakest preconditions
- Characteristic formulae for the verification of imperative programs
- Verification conditions are code
- Verification Condition Generation Via Theorem Proving
- Assertion-based slicing and slice graphs
- Error-tracing axiomatic semantics for C-kernel
- Effective generation of verification conditions for non-deterministic unstructured programs
- Avoiding exponential explosion: generating compact verification conditions
- A generic intermediate representation for verification condition generation
- Deciding Kleene algebra terms equivalence in Coq
- Generation of correctness conditions for imperative programs
- Explaining Verification Conditions
- Programmable verifiers in imperative programming
Describes a project that uses
Uses Software
This page was built for publication: Verification conditions for source-level imperative programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q465685)
