Characteristic formulae for the verification of imperative programs

No abstract is available for this paper.

• Publication year

  2011

• Venue

  ACM SIGPLAN International Conference on Functional Programming

• Publication date

  2011-09-19

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/2034773.2034828
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Axiomatic Basis for Computer Programming

  2013cited by this paper
• Formal verification of machine-code programs

  2011cited by this paper
• Separation Logic Adapted for Proofs by Rewriting

  2010cited by this paper
• Program verification through characteristic formulae

  2010cited by this paper
• Structuring the verification of heap-manipulating programs

  2010influential reference
• Local Reasoning about While-Loops

  2010cited by this paper
• Practical Tactics for Separation Logic

  2009cited by this paper
• Experience report: seL4: formally verifying a high-performance microkernel

  2009cited by this paper
• Who: a verifier for effectful higher-order programs

  2009cited by this paper
• Effective interactive proofs for higher-order imperative programs

  2009influential reference
• seL4: formal verification of an OS kernel

  2009cited by this paper
• An integrated proof language for imperative programs

  2009cited by this paper
• Author manuscript, published in "International Workshop on Type theory, proof theory, and rewriting (TPR'07) (2007)" The Implicit Calculus of Constructions as a Programming Language with Dependent Types

  2009cited by this paper
• Verified LISP Implementations on ARM, x86 and PowerPC

  2009cited by this paper
• Hoare type theory, polymorphism and separation1

  2008influential reference
• A Hoare Logic for Call-by-Value Functional Programs

  2008cited by this paper
• Verification of Object-Oriented Software. The KeY Approach - Foreword by K. Rustan M. Leino

  2007cited by this paper
• Frame rules from answer types for code pointers

  2006cited by this paper
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant

  2006cited by this paper
• Descriptive and Relative Completeness of Logics for Higher-Order Functions

  2006cited by this paper
• Certified assembly programming with embedded code pointers

  2006cited by this paper
• Towards Formal Verication of Memory Properties using Separation Logic

  2005cited by this paper
• Proving pointer programs in higher-order logic

  2005cited by this paper
• Smallfoot: Modular Automatic Assertion Checking with Separation Logic

  2005cited by this paper
• Dependent type theory of stateful higher-order functions

  2005cited by this paper
• Toward Verification of Memory Management property using Separation logic

  2005cited by this paper
• A logical analysis of aliasing in imperative higher-order functions

  2005cited by this paper
• Programmation fonctionnelle certifiée : L'extraction de programmes dans l'assistant Coq. (Certified functional programming : Program extraction within Coq proof assistant)

  2004cited by this paper
• Verification of non-functional programs using interpretations in type theory

  2003cited by this paper
• Verification of Object-Oriented Programs with Invariants

  2003cited by this paper
• Java Program Verification at Nijmegen: Developments and Perspective

  2003cited by this paper
• Dynamic Logic by David Harel, Dexter Kozen and Jerzy Tiuryn. The MIT Press, Cambridge, Massachusetts. Hardback: ISBN 0–262–08289–6, $50, xv + 459 pages

  2002cited by this paper
• Separation logic: a logic for shared mutable data structures

  2002influential reference
• New Results - Implémentations de Caml

  2002cited by this paper
• Dynamic logic

  2001influential reference
• Local Reasoning about Programs that Alter Data Structures

  2001cited by this paper
• Purely functional data structures

  1998cited by this paper
• Assigning Meanings to Programs

  1993cited by this paper
• The essence of compiling with continuations

  1993cited by this paper
• A Modal Characterization of Observational Congruence on Finite Terms of CCS

  1984cited by this paper
• On Observing Nondeterminism and Concurrency

  1980cited by this paper

• Formal Semantics and Program Logics for a Fragment of OCaml

  2025cites this paper
• coma, an Intermediate Verification Language with Explicit Abstraction Barriers

  2025cites this paper
• Unfolding Iterators: Specification and Verification of Higher-Order Iterators, in OCaml

  2025cites this paper
• Verified VCG and Verified Compiler for Dafny

  2025cites this paper
• Nola: Later-Free Ghost State for Verifying Termination in Iris

  2025cites this paper
• PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs

  2025cites this paper
• Destabilizing Iris

  2025cites this paper
• Practical Deductive Verification of OCaml Programs

  2024cites this paper
• Verifying Programs with Logic and Extended Proof Rules: Deep Embedding vs. Shallow Embedding

  2024cites this paper
• Correctly Compiling Proofs About Programs Without Proving Compilers Correct

  2024cites this paper
• Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq

  2024cites this paper
• Le chameau et le serpent rentrent dans un bar : vérification quasi-automatique de code OCaml en logique de séparation

  2024cites this paper
• Static and Dynamic Verification of OCaml Programs: The Gospel Ecosystem (Extended Version)

  2024cites this paper
• Mechanised Hypersafety Proofs about Structured Data

  2024cites this paper
• Mostly Automated Proof Repair for Verified Libraries

  2023cites this paper
• Morpheus: Automated Safety Verification of Data-dependent Parser Combinator Programs

  2023cites this paper
• A Product of Shape and Sequence Abstractions

  2023cites this paper
• An AST for Representing Programs with Invariants and Proofs

  2023cites this paper
• Interaction Tree Specifications: A Framework for Specifying Recursive, Effectful Computations That Supports Auto-Active Verification (Artifact)

  2023cites this paper
• Interaction Tree Specifications: A Framework for 15 Specifying Recursive, Effectful Computations that 16 Supports Auto-active Verification

  2023cites this paper
• Omnisemantics: Smooth Handling of Nondeterminism

  2023cites this paper
• Specifying and Verifying Higher-order Rust Iterators

  2023influential citation
• Verified symbolic execution with Kripke specification monads (and no meta-programming)

  2022cites this paper
• Specification and verification of a transient stack

  2022influential citation
• Coq’s vibrant ecosystem for verification engineering (invited talk)

  2022cites this paper
• Conditional Contextual Refinement (CCR)

  2022cites this paper
• Functional Correctness of C Implementations of Dijkstra's, Kruskal's, and Prim's Algorithms

  2021cites this paper
• The CakeML Project's Quest for Ever Stronger Correctness Theorems (Invited Paper)

  2021cites this paper
• Cogent: uniqueness types and certifying compilation

  2021cites this paper
• Steel: proof-oriented programming in a dependently typed concurrent separation logic

  2021cites this paper
• Transfinite Iris: resolving an existential dilemma of step-indexed separation logic

  2021cites this paper
• Cameleer: a Deductive Verification Tool for OCaml

  2021influential citation
• Cost-Aware Type Theory

  2020cites this paper
• Formalisation de Sémantiques Squelettiques

  2020cites this paper
• Separation logic for sequential programs (functional pearl)

  2020cites this paper
• Formalization of logical calculi in Isabelle/HOL

  2020cites this paper
• FreeSpec: specifying, verifying, and executing impure computations in Coq

  2020cites this paper
• Layered Indexed Effects: Foundations and Applications of Effectful Dependently Typed Programming

  2020cites this paper
• Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts

  2019cites this paper
• PML2: Integrated Program Verification in ML

  2019cites this paper
• Reduction from branching-time property verification of higher-order programs to HFL validity checking

  2019cites this paper
• Optimizing a Verified SAT Solver

  2019cites this paper
• Formal Proof and Analysis of an Incremental Cycle Detection Algorithm

  2019cites this paper
• Semi-automated Reasoning About Non-determinism in C Expressions

  2019cites this paper
• Desfuncionalizar para Provar

  2019cites this paper
• Embedding Untrusted Imperative ML Oracles into Coq Verified Code

  2019cites this paper
• GOSPEL - Providing OCaml with a Formal Specification Language

  2019influential citation
• Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra

  2019cites this paper
• Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle

  2019cites this paper
• Trustworthy Graph Algorithms

  2019cites this paper
• Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL

  2019cites this paper
• Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs

  2019cites this paper
• Certifying graph-manipulating C programs via localizations within data structures

  2019cites this paper
• Verifying concurrent, crash-safe systems with Perennial

  2019cites this paper
• Abstract Heap Relations for a Compositional Shape Analysis. (Abstractions Relationnelles de la Mémoire pour une Analyse Compositionnelle de Structures de Données)

  2019cites this paper
• VerifyThis 2018: A Program Verification Competition

  2019cites this paper
• Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle

  2018cites this paper
• A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification

  2018influential citation
• MoSeL: a general, extensible modal framework for interactive proofs in separation logic

  2018influential citation
• Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle

  2018cites this paper
• Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part IV

  2018cites this paper
• Scalability of Deductive Verification Depends on Method Call Treatment

  2018cites this paper
• 22nd International Conference on Types for Proofs and Programs, TYPES 2016, Novi Sad, Serbia, May 23-26, 2016

  2018cites this paper
• Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels. (Methods and tools for specification and proof of difficult properties of sequential programs)

  2018cites this paper
• Program Verification in the Presence of I/O - Semantics, Verified Library Routines, and Verified Applications

  2018cites this paper
• The PML 2 Language : Proving Programs in ML

  2018cites this paper
• From Sets to Bits in Coq

  2018cites this paper
• 23rd International Conference on Types for Proofs and Programs, TYPES 2017, Budapest, Hungary, May 29 - June 1, 2017

  2018cites this paper
• Program Extraction for Mutable Arrays

  2018cites this paper
• Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels

  2018cites this paper
• RustBelt : Logical Foundations for the Future of Safe Systems Programming

  2018cites this paper
• Modular Termination Verification of Single-Threaded and Multithreaded Programs

  2018influential citation
• Bidirectional Certified Programming

  2017cites this paper
• Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits

  2017cites this paper
• A Toolchain for Verified OCaml Programs

  2017cites this paper
• Temporary Read-Only Permissions for Separation Logic

  2017cites this paper
• Recalling a Witness

  2017cites this paper
• Verifying a hash table and its iterators in higher-order separation logic

  2017cites this paper
• Recalling a witness: foundations and applications of monotonic state

  2017cites this paper
• Verified Characteristic Formulae for CakeML

  2017influential citation
• VOCAL – A Verified OCAml Library

  2017cites this paper
• Verifying Hash tables in Iris

  2017influential citation
• Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL

  2017cites this paper
• Défonctionnaliser pour prouver

  2016cites this paper
• Functional and Logic Programming

  2016cites this paper
• Refinement based verification of imperative data structures

  2016cites this paper
• Efficient Verification of Imperative Programs Using Auto2

  2016cites this paper
• Dijkstra monads for free

  2016cites this paper
• COGENT: Certified Compilation for a Functional Systems Language

  2016cites this paper
• Formalizing the Edmonds-Karp Algorithm

  2016cites this paper
• From Sets to Bits in Coq

  2016cites this paper
• A Modular Way to Reason About Iteration

  2016cites this paper
• Higher-order representation predicates in separation logic

  2016influential citation
• Refinement through restraint: bringing down the cost of verification

  2016cites this paper
• Proof automation for functional correctness in separation logic

  2016cites this paper
• Coq Support in HAHA

  2016cites this paper
• Thesis for obtaining the title of Doctor of Engineering of the Faculties of Natural Sciences and Technology of Saarland University vorgelegt von

  2015cites this paper
• Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation

  2015influential citation
• Formal Verification of Asymptotic Complexity Bounds for OCaml Programs MPRI M 2 Internship Report , March-August 2015

  2015cites this paper
• Refinement to Imperative HOL

  2015cites this paper