scientific article; zbMATH DE number 7453193
From MaRDI portal
Publication:5020652
Authors: Emanuele De Angelis, Fabio Fioravanti, Maurizio Proietti 
Publication date: 6 January 2022
Full work available at URL: https://arxiv.org/abs/2008.02934
Title of this publication is not available (Why is that?)
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Title not available (Why is that?)
- 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)
Uses Software
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)
