scientific article; zbMATH DE number 7444023
zbMATH Open1483.68189arXiv1907.03999MaRDI QIDQ5016384FDOQ5016384
Authors: Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti 
Publication date: 13 December 2021
Full work available at URL: https://arxiv.org/abs/1907.03999
Title of this publication is not available (Why is that?)
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
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)
Cites Work
- Induction for SMT solvers
- \(b=\int g\)
- The automation of proof by mathematical induction
- Proving correctness of imperative programs by linearizing constrained Horn clauses
- Transformations of CLP modules
- Automating induction for solving Horn clauses
- Horn clause solvers for program verification
- Predicate pairing for program verification
- Solving Horn clauses on inductive data types without induction
- Synchronizing constrained Horn clauses
- Title not available (Why is that?)
Cited In (4)
- 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
- An assertional proof of the stability and correctness of Natural Mergesort
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)
