Analysis and Transformation of Constrained Horn Clauses for Program Verification
From MaRDI portal
Publication:6063893
DOI10.1017/s1471068421000211arXiv2108.00739OpenAlexW3214504269MaRDI QIDQ6063893
Manuel V. Hermenegildo, Fabio Fioravanti, Emanuele De Angelis, Maurizio Proietti, Alberto Pettorossi, John P. Gallagher
Publication date: 12 December 2023
Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2108.00739
program transformationprogram analysisconstraint logic programmingprogram verificationconstrained Horn clauses
Related Items (3)
Cites Work
- Decision procedures for flat array properties
- SAT modulo linear arithmetic for solving polynomial constraints
- Deciding floating-point logic with abstract conflict driven clause learning
- SMT-based model checking for recursive programs
- An efficient SMT solver for string constraints
- Transformations of CLP modules
- Unfolding--definition--folding, in this order, for avoiding unnecessary variables in logic programs
- Abstract interpretation: a kind of magic
- Horn clause verification with convex polyhedral abstraction and tree automata-based refinement
- Grammar-related transformations of logic programs
- Cost analysis of object-oriented bytecode programs
- Polyvariant mixed computation for analyzer programs
- Deforestation: Transforming programs to eliminate trees
- Inference rules for proving the equivalence of recursive procedures
- An overview of the K semantic framework
- Unfold/fold transformation of stratified programs
- A bottom-up polymorphic type inference in logic programming
- Mixtus: An automatic partial evaluator for full Prolog
- Bottom-up abstract interpretation of logic programs
- A decompositional approach for computing least fixed-points of datalog programs with \(\mathcal Z\)-counters
- Isabelle/HOL. A proof assistant for higher-order logic
- Relational verification through Horn clause transformation
- Predicate pairing with abstraction for relational verification
- The Alexander Method - a technique for the processing of recursive axioms in deductive databases
- Removing algebraic data types from constrained Horn clauses using difference predicates
- Automating induction for solving Horn clauses
- On certain axiomatizations of arithmetic of natural and integer numbers
- Closed-form upper bounds in static cost analysis
- Linear resolution with selection function
- Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor)
- A lattice-theoretical fixpoint theorem and its applications
- Mechanized semantics for the clight subset of the C language
- A Transformational Approach to Parametric Accumulated-Cost Static Profiling
- Controlling Polyvariance for Specialization-based Verification
- Generalized Property Directed Reachability
- Proving Theorems by Program Transformation
- An overview of Ciao and its design philosophy
- TRACER: A Symbolic Execution Tool for Verification
- Solving Non-linear Arithmetic
- Resource Usage Analysis of Logic Programs via Abstract Interpretation Using Sized Types
- Horn Clause Solvers for Program Verification
- Newtonian program analysis
- On the implementation of the probabilistic logic programming language ProbLog
- BEYOND TAMAKI-SATO STYLE UNFOLD/FOLD TRANSFORMATIONS FOR NORMAL LOGIC PROGRAMS
- SAT-Based Model Checking without Unrolling
- Convex Hull Abstractions in Specialization of CLP Programs
- Analyzing logic programs using “prop”-ositional logic programs and a magic wand
- Interval-Based Resource Usage Verification: Formalization and Prototype
- Satisfiability Modulo Theories
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Refinement of Trace Abstraction
- Simple relational correctness proofs for static analyses and program transformations
- Counterexample-guided abstraction refinement for symbolic model checking
- Efficient generation of test data structures using constraint logic programming and program transformation
- Test Case Generation of Actor Systems
- Test case generation for object-oriented imperative languages in CLP
- Coinductive Logic Programming and Its Applications
- Abstract Interpretation with Specialized Definitions
- Analysis of Linear Hybrid Systems in CLP
- Simplification by Cooperating Decision Procedures
- Partial evaluation in logic programming
- Abstract interpretation and application to logic programs
- Compile-time derivation of variable dependency using abstract interpretation
- Abstract interpretation based on Alexander Templates
- A Transformation System for Developing Recursive Programs
- Horn clause computability
- The semantics of constraint logic programs1Note that reviewing of this paper was handled by the Editor-in-Chief.1
- Theory and practice of constraint handling rules
- Abstract interpretation of logic programs using magic transformations
- Logic programming and negation: A survey
- Transformation of logic programs: Foundations and techniques
- Exploiting goal independence in the analysis of logic programs
- Logic program specialisation through partial deduction: Control issues
- Solving Horn Clauses on Inductive Data Types Without Induction
- An iterative approach to precondition inference using constrained Horn clauses
- Horn clauses as an intermediate representation for program analysis and transformation
- A general framework for static profiling of parametric resource usage
- Predicate Pairing for program verification
- Interval-based resource usage verification by translation into Horn clauses and an application to energy consumption
- Tree dimension in verification of constrained Horn clauses
- Synchronizing Constrained Horn Clauses
- Proving Properties of Co-Logic Programs by Unfold/Fold Transformations
- Conjunctive partial deduction: foundations, control, algorithms, and experiments
- Abstract multiple specialization and its application to program parallelization
- Optimized algorithms for incremental analysis of logic programs
- Precise interprocedural dataflow analysis with applications to constant propagation
- Incremental Analysis of Logic Programs with Assertions and Open Predicates
- An Integrated Approach to Assertion-Based Random Testing in Prolog
- Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis
- Concolic Testing in CLP
- Induction for SMT Solvers
- Software model checking
- Probabilistic Horn Clause Verification
- Dynamic partial-order reduction for model checking software
- The loop absorption and the generalization strategies for the development of logic programs and partial deduction
- Generalization strategies for the verification of infinite state systems
- Removing Superfluous Versions in Polyvariant Specialization of Prolog Programs
- Programming Languages and Systems
- Why3 — Where Programs Meet Provers
- The MathSAT5 SMT Solver
- Relational cost analysis
- Semantics and Controllability of Time-Aware Business Processes*
- Failure tabled constraint logic programming by interpolation
- Decidable logics combining heap structures and data
- A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs
- An axiomatic basis for computer programming
- Program Development in Computational Logic
- Improving Reachability Analysis of Infinite State Systems by Specialization
- ICE-based refinement type discovery for higher-order functional programs
- Constraint-based deductive model checking
- Syntax-guided termination analysis
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Analysis and Transformation of Constrained Horn Clauses for Program Verification
