scientific article; zbMATH DE number 7444023
From MaRDI portal
Publication:5016384
Searching and sorting (68P10) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)
Recommendations
- Horn clause solvers for program verification
- scientific article; zbMATH DE number 4014042
- Deductive synthesis of sorting programs
- A simple functional presentation and an inductive correctness proof of the Horn algorithm
- Proving correctness of imperative programs by linearizing constrained Horn clauses
- A correctness proof of sorting by means of formal procedures
Cites work
- scientific article; zbMATH DE number 3039293 (Why is no real title available?)
- Automating induction for solving Horn clauses
- Horn clause solvers for program verification
- Induction for SMT solvers
- Predicate pairing for program verification
- Proving correctness of imperative programs by linearizing constrained Horn clauses
- Solving Horn clauses on inductive data types without induction
- Synchronizing constrained Horn clauses
- The automation of proof by mathematical induction
- Transformations of CLP modules
- \(b=\int g\)
Cited in
(4)- An assertional proof of the stability and correctness of Natural Mergesort
- A Generic Approach to the Verification of the Permutation Property of Sequential and Parallel Swap-Based Sorting Algorithms
- Solving Horn clauses on inductive data types without induction
- Removing algebraic data types from constrained Horn clauses using difference predicates
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5016384)
