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
- Induction for SMT Solvers
- Proof of a recursive program: Quicksort
- An axiomatic basis for computer programming
- Deforestation: Transforming programs to eliminate trees
- The automation of proof by mathematical induction
- A Transformation System for Developing Recursive Programs
- Verification of sequential and concurrent programs
- Derivation of Logic Programs
- Transformations of CLP modules
- Unfolding--definition--folding, in this order, for avoiding unnecessary variables in logic programs
- Analysis of Linear Hybrid Systems in CLP
- A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs
- Automating induction for solving Horn clauses
- Horn Clause Solvers for Program Verification
- A decompositional approach for computing least fixed-points of datalog programs with \(\mathcal Z\)-counters
- Reasoning about algebraic data types with abstractions
- Decision procedures for algebraic data types with abstractions
- Quicksort revisited. Verifying alternative versions of quicksort
- Removing algebraic data types from constrained Horn clauses using difference predicates
- Solving Horn Clauses on Inductive Data Types Without Induction
- Synchronizing Constrained Horn Clauses
- Title not available (Why is that?)
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)