Incremental and Modular Context-sensitive Analysis

DOI10.1017/S1471068420000496zbMath1472.68035arXiv1804.01839OpenAlexW3122466558MaRDI QIDQ4957220

Manuel V. Hermenegildo, Isabel García-Contreras, Jose Francisco Morales

Publication date: 3 September 2021

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

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

zbMATH Keywords

program analysisincremental analysisabstract interpretationconstrained Horn clausesfixpoint algorithmsmodular analysislogic and constraint programming

Mathematics Subject Classification ID

Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (3)

VeriFly: On-the-fly Assertion Checking via Incrementality ⋮ Parallel Logic Programming: A Sequel ⋮ Result invalidation for incremental modular analyses

Uses Software

• z3
• TRACER
• HSF
• Ciao
• CiaoPP
• SeaHorn
• Datalog
• Infer
• VeriMAP
• RAHFT
• Flix
• IncA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Cost analysis of object-oriented bytecode programs
• Why does Astrée scale up?
• Automatic inference of determinacy and mutual exclusion for logic programs using mode and type analyses
• Conditions for incremental iteration: Examples and counterexamples
• A compositional semantics for logic programs
• A structural approach to operational semantics
• Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor)
• An overview of Ciao and its design philosophy
• TRACER: A Symbolic Execution Tool for Verification
• Incremental Tabling in Support of Knowledge Representation and Reasoning
• Horn Clause Solvers for Program Verification
• Static Contract Checking with Abstract Interpretation
• Analysis of Linear Hybrid Systems in CLP
• Compile-time derivation of variable dependency using abstract interpretation
• Property Directed Equivalence via Abstract Simulation
• Interval-based resource usage verification by translation into Horn clauses and an application to energy consumption
• Optimized algorithms for incremental analysis of logic programs
• Detecting Determinacy in Prolog Programs
• A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs
• A Machine-Oriented Logic Based on the Resolution Principle
• Program Development in Computational Logic
• Computer Aided Verification
• A practical framework for theabstract interpretation of logic programs
• Incremental verification using trace abstraction

This page was built for publication: Incremental and Modular Context-sensitive Analysis