Compositional Analysis for Equational Horn Programs

Abstract. We introduce a compositional characterization of the operational semantics of equational Horn programs. Then we show that this semantics and the standard operational semantics based on (barowing coincide. We define an abstract narrower mimicking this semantics, and show how it can be used as a basis for efficient ANDcompositional program analysis. As an application of our framework, we show a compositional analysis to detect the unsatisfiability of an equation set with respect to a given equational theory. We also show that our method allows us to perform computations and analysis incrementally in a Constraint Equational setting and that the test of satisfiability in this setting can be done in parallel.

• Type: Conference
• Year: 1994
• Where: ALP
• Authors: María Alpuente, Moreno Falaschi, Germán Vidal
• Keywords: ALP 1994, Automated Reasoning, Equational, Equational Horn Programs, Operational Semantics