scientific article; zbMATH DE number 7453193
From MaRDI portal
Publication:5020652
Fabio Fioravanti, Emanuele De Angelis, Maurizio Proietti
Publication date: 6 January 2022
Full work available at URL: https://arxiv.org/abs/2008.02934
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Transformations of CLP modules
- Unfolding--definition--folding, in this order, for avoiding unnecessary variables in logic programs
- Verification of sequential and concurrent programs
- Deforestation: Transforming programs to eliminate trees
- A decompositional approach for computing least fixed-points of datalog programs with \(\mathcal Z\)-counters
- Reasoning about algebraic data types with abstractions
- Quicksort revisited. Verifying alternative versions of quicksort
- Removing algebraic data types from constrained Horn clauses using difference predicates
- Automating induction for solving Horn clauses
- Horn Clause Solvers for Program Verification
- Analysis of Linear Hybrid Systems in CLP
- Derivation of Logic Programs
- A Transformation System for Developing Recursive Programs
- Solving Horn Clauses on Inductive Data Types Without Induction
- Synchronizing Constrained Horn Clauses
- Induction for SMT Solvers
- Decision procedures for algebraic data types with abstractions
- A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs
- An axiomatic basis for computer programming
- Proof of a recursive program: Quicksort
This page was built for publication:
