Verification conditions for source-level imperative programs
DOI10.1016/j.cosrev.2011.02.002zbMath1298.68171OpenAlexW2142667604MaRDI QIDQ465685
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
Hoare logicprogram verificationweakest preconditionsupdatesprogram annotationsverification conditions
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Efficient weakest preconditions
- The derivation of systolic computations
- Handbook of philosophical logic. Volume II: Extensions of classical logic
- Affine relationships among variables of a program
- Isabelle/HOL. A proof assistant for higher-order logic
- Automatic program verification. I: A logical basis and its implementation
- Weakest pre-condition reasoning for Java programs with JML annotations
- The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
- Secure mechanical verification of mutually recursive procedures
- Hoare logic and auxiliary variables
- Computer aided verification. 19th international conference, CAV 2007, Berlin, Germany, July 3--7, 2007. Proceedings.
- Specification and verification challenges for sequential object-oriented programs
- CC(X): Semantic Combination of Congruence Closure with Solvable Theories
- Secure information flow by self-composition
- Mechanical proofs about computer programs
- Simplify: a theorem prover for program checking
- Grammar Analysis and Parsing by Abstract Interpretation
- Abstract Interpretation of Symbolic Execution with Explicit State Updates
- Satisfiability Modulo Theories: An Appetizer
- Inference Rules for Program Annotation
- Ten Years of Hoare's Logic: A Survey—Part I
- Logical analysis of programs
- Theories of Programming Languages
- Specifying Software
- Hoare logic for Java in Isabelle/HOL
- Avoiding exponential explosion
- Automated deduction for verification
- Software model checking
- Theory and Applications of Satisfiability Testing
- A Tutorial on Satisfiability Modulo Theories
- An axiomatic basis for computer programming
This page was built for publication: Verification conditions for source-level imperative programs
