An expressive trace logic for recursive programs
From MaRDI portal
Cites work
- -Calculus with Explicit Points and Approximations
- A lattice-theoretical fixpoint theorem and its applications
- A propositional modal logic of time intervals
- A structural approach to operational semantics
- Deductive software verification: from pen-and-paper proofs to industrial tools
- Finiteness is mu-ineffable
- First-Order and Temporal Logics for Nested Words
- Hoare logic for Java in Isabelle/HOL
- scientific article; zbMATH DE number 1304336 (Why is no real title available?)
- scientific article; zbMATH DE number 3351184 (Why is no real title available?)
- 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
- Kleene algebra with tests and Coq tools for while programs
- Locally abstract, globally concrete semantics of concurrent programming languages
- Matching logic
- Matching logic explained
- On Hoare logic and Kleene algebra with tests
- Propositional dynamic logic of context-free programs and fixpoint logic with chop
- Semantics with applications: an appetizer.
- Temporal abstract interpretation
- Temporal stream logic: synthesis beyond the Bools
- Trace-Based Coinductive Operational Semantics for While
- Trace-based deductive verification
This page was built for publication: An expressive trace logic for recursive programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7296816)
