Verification conditions for source-level imperative programs
DOI10.1016/J.COSREV.2011.02.002zbMATH Open1298.68171OpenAlexW2142667604MaRDI QIDQ465685FDOQ465685
Authors: Jorge Sousa Pinto, Maria João Frade 
Publication date: 24 October 2014
Published in: Computer Science Review (Search for Journal in Brave)
Full work available at URL: http://hdl.handle.net/1822/12547
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
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)
Cites Work
- Theory and Applications of Satisfiability Testing
- Simplify: a theorem prover for program checking
- Isabelle/HOL. A proof assistant for higher-order logic
- Satisfiability modulo theories: an appetizer
- Title not available (Why is that?)
- Title not available (Why is that?)
- An axiomatic basis for computer programming
- Affine relationships among variables of a program
- Ten Years of Hoare's Logic: A Survey—Part I
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Grammar Analysis and Parsing by Abstract Interpretation
- Automated deduction for verification
- A Tutorial on Satisfiability Modulo Theories
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Software model checking
- Computer aided verification. 19th international conference, CAV 2007, Berlin, Germany, July 3--7, 2007. Proceedings.
- \textsf{CC(X)}: semantic combination of congruence closure with solvable theories
- Logical analysis of programs
- Hoare logic for Java in Isabelle/HOL
- Title not available (Why is that?)
- Efficient weakest preconditions
- The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
- Specification and verification challenges for sequential object-oriented programs
- Avoiding exponential explosion: generating compact verification conditions
- Title not available (Why is that?)
- The derivation of systolic computations
- Weakest pre-condition reasoning for Java programs with JML annotations
- Hoare logic and auxiliary variables
- Title not available (Why is that?)
- Handbook of philosophical logic. Volume II: Extensions of classical logic
- Automatic program verification. I: A logical basis and its implementation
- Secure mechanical verification of mutually recursive procedures
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Secure information flow by self-composition
- Mechanical proofs about computer programs
- Theorem-proving support in programming language semantics
- Abstract Interpretation of Symbolic Execution with Explicit State Updates
- Inference Rules for Program Annotation
- Title not available (Why is that?)
- Theories of Programming Languages
- Specifying Software
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
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
- Explaining Verification Conditions
- Generation of correctness conditions for imperative programs
- Programmable verifiers in imperative programming
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)
