Trace-based verification of imperative programs with I/O
From MaRDI portal
Publication:617977
DOI10.1016/j.jsc.2010.08.004zbMath1215.68070OpenAlexW2106096722MaRDI QIDQ617977
Greg Morrisett, Ryan Wisnesky, Gregory Malecha
Publication date: 14 January 2011
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jsc.2010.08.004
General topics in the theory of software (68N01) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Automated temporal verification for algebraic effects ⋮ An extensible approach to session polymorphism
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Intuitionistic completeness of first-order logic
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Certifying low-level programs with hardware interrupts and preemptive threads
- A semantics for concurrent separation logic
- A calculus for cryptographic protocols: The spi calculus
- Isabelle/HOL. A proof assistant for higher-order logic
- Effective interactive proofs for higher-order imperative programs
- Dafny: An Automatic Program Verifier for Functional Correctness
- A Hoare Logic for the State Monad
- Multiparty asynchronous session types
- Parsing expression grammars
- Imperative Functional Programming with Isabelle/HOL
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Bisimulation can't be traced
- The view from the left
- Ynot
- Toward a verified relational database management system
- Verifying distributed systems
- Programming Languages and Systems
- Using First-Order Theorem Provers in the Jahob Data Structure Verification System
- A Realizability Model for Impredicative Hoare Type Theory
- Polymorphism and separation in hoare type theory
