Interval-based resource usage verification by translation into Horn clauses and an application to energy consumption

DOI10.1017/S1471068418000042zbMath1478.68170arXiv1803.04451OpenAlexW2962765334WikidataQ114653853 ScholiaQ114653853MaRDI QIDQ4644354

Manuel V. Hermenegildo, Maximiliano Klemen, Umer Liqat, Luthfi Darmawan, Francisco Bueno, Pedro Lopez-Garcia

Publication date: 31 May 2018

Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)

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

zbMATH Keywords

static analysisdebuggingenergy consumptionprogram verificationHorn clause-based analysis and verificationresource usage analysis and verification

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (6)

A General Framework for Static Cost Analysis of Parallel Logic Programs ⋮ VeriFly: On-the-fly Assertion Checking via Incrementality ⋮ Fifty Years of Prolog and Beyond ⋮ Parallel Logic Programming: A Sequel ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ Incremental and Modular Context-sensitive Analysis

Uses Software

• z3
• LLVM
• GSL
• HSF
• Ciao
• CiaoPP
• RAHFT

Cites Work

• Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor)
• A Framework for Verification and Debugging of Resource Usage Properties: Resource Usage Verification
• An overview of Ciao and its design philosophy
• Resource Usage Analysis of Logic Programs via Abstract Interpretation Using Sized Types
• Static Contract Checking with Abstract Interpretation
• Interval-Based Resource Usage Verification: Formalization and Prototype
• Compile-time derivation of variable dependency using abstract interpretation
• Abstract diagnosis
• A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs
• Comparing Cost Functions in Resource Analysis
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Interval-based resource usage verification by translation into Horn clauses and an application to energy consumption