scientific article; zbMATH DE number 7453193

MaRDI QIDQ5020652FDO

Authors Emanuele De Angelis, Fabio Fioravanti, Maurizio Proietti

Publication date 6 January 2022

Full work available at URL https://arxiv.org/abs/2008.02934

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites work

• scientific article; zbMATH DE number 1696790 (Why is no real title available?)
• A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs
• A Transformation System for Developing Recursive Programs
• A decompositional approach for computing least fixed-points of datalog programs with \(\mathcal Z\)-counters
• An axiomatic basis for computer programming
• Analysis of Linear Hybrid Systems in CLP
• Automating induction for solving Horn clauses
• Decision procedures for algebraic data types with abstractions
• Deforestation: Transforming programs to eliminate trees
• Derivation of Logic Programs
• Horn clause solvers for program verification
• Induction for SMT solvers
• Proof of a recursive program: Quicksort
• Quicksort revisited. Verifying alternative versions of quicksort
• Reasoning about algebraic data types with abstractions
• Removing algebraic data types from constrained Horn clauses using difference predicates
• Solving Horn clauses on inductive data types without induction
• Synchronizing constrained Horn clauses
• The automation of proof by mathematical induction
• Transformations of CLP modules
• Unfolding--definition--folding, in this order, for avoiding unnecessary variables in logic programs
• Verification of sequential and concurrent programs

Cited in

(3)

• Simplifying the Verification of Quantified Array Assertions via Code Transformation
• A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq
• Proving Quicksort Correct in Event-B

Describes a project that uses

Uses Software

• z3
• ARMC
• Scala
• CVC4
• Quicksort
• VeriMAP

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 Q5020652)