Skip to Main content Skip to Navigation
Conference papers

Numeric Domains Meet Algebraic Data Types

Santiago Bautista 1 Thomas Jensen 1 Benoît Montagu 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : We report on the design and formalization of a novel abstract domain, called numeric path relations (NPRs), that combines numeric relational domains with algebraic data types. This domain expresses relations between algebraic values that can contain scalar data. The construction of the domain is parameterized by the choice of a relational domain on scalar values. The construction employs projection paths on algebraic values, and in particular projections on variant cases, whose sound treatment is subtle due to mutual exclusiveness.
Document type :
Conference papers
Complete list of metadata
Contributor : Benoît Montagu Connect in order to contact the contributor
Submitted on : Friday, November 27, 2020 - 3:58:26 PM
Last modification on : Wednesday, November 3, 2021 - 8:13:49 AM
Long-term archiving on: : Sunday, February 28, 2021 - 8:09:11 PM


Files produced by the author(s)



Santiago Bautista, Thomas Jensen, Benoît Montagu. Numeric Domains Meet Algebraic Data Types. NSAD 2020 - 9th International Workshop on Numerical and Symbolic Abstract Domains, Nov 2020, Virtual, United States. pp.12-16, ⟨10.1145/3427762.3430178⟩. ⟨hal-03028476⟩



Les métriques sont temporairement indisponibles