Reasoning about incompletely defined programs
From MaRDI portal
program verificationautomated reasoningunderspecificationtheorem proving by inductionloose specificationincompletely defined programsVeriFun
Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Functional programming and lambda calculus (68N18) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites work
- scientific article; zbMATH DE number 3073037 (Why is no real title available?)
- Adapting Calculational Logic to the Undefined
- Classical logic with partial functions
- Computer science today. Recent trends and developments
- Context dependent procedures and computed types in \texttt{VeriFun}
- Dafny: an automatic program verifier for functional correctness
- Dependent types and multi-monadic effects in \(\mathrm{F}^*\)
- Induction proofs with partial functions
- Isabelle/HOL. A proof assistant for higher-order logic
- Logic for Programming, Artificial Intelligence, and Reasoning
- Many-Valued Logic, Partiality, and Abstraction in Formal Specification Languages
- On proving the termination of algorithms by machine
- Partial and nested recursive function definitions in higher-order logic
- Partial functions and logics: A warning
- Partial functions in ACL2
- Partial functions in a total setting
- Reasoning about partial functions in the formal development of programs
- Refinement types for Haskell
- Why3 -- where programs meet provers
This page was built for publication: Reasoning about incompletely defined programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6912393)
