Powered by
9th ACM SIGPLAN International Workshop on Numerical and Symbolic Abstract Domains (NSAD 2020),
November 17, 2020,
Virtual, USA
9th ACM SIGPLAN International Workshop on Numerical and Symbolic Abstract Domains (NSAD 2020)
Frontmatter
Welcome from the Chairs
Welcome to the Ninth International Workshop on Numerical and Symbolic Abstract Domains (NSAD 2020).
The workshop took place virtually (online) on November 17, 2020 as a satellite event to the
ACM SIGPLAN conference on Systems, Programming, Languages, and Applications: Software for Humanity
(SPLASH 2020).
Invited Talk
Abstract Domains in SMT Solving for Real Algebra (Invited Talk)
Erika Abraham
(RWTH Aachen University, Germany)
SMT solving is a technology which aims at solving logical formulas over different theories. For real algebraic formulas, some SMT solvers make use of a method based on the cylindrical algebraic decomposition. We discuss relevant abstract domains in this context and illustrate how a modified abstract domain view can improve the solving techniques.
@InProceedings{NSAD20p1,
author = {Erika Abraham},
title = {Abstract Domains in SMT Solving for Real Algebra (Invited Talk)},
booktitle = {Proc.\ NSAD},
publisher = {ACM},
pages = {1--1},
doi = {10.1145/3427762.3430180},
year = {2020},
}
Publisher's Version
Papers
Abstract Domains for Constraint Programming with Differential Equations
Ghiles Ziat,
Olivier Mullier,
Julien Alexandre dit Sandretto,
Christophe Garion,
Alexandre Chapoutot, and
Xavier Thirioux
(ISAE-supaero, France; University of Toulouse, France; ENSTA Paris, France)
Cyber-physical systems (CPSs), as cruise control systems, involve
life-critical or mission critical functions that must be
validated. Formal verification techniques can bring high assurance
level but have to be extended to embrace all the components of
CPSs. Physical part models of CPSs are usually defined from ordinary
differential equations (ODEs) and reachability methods can be used
to compute safe over-approximation of the solution set of
ODEs. However, additional constraints, as obstacle avoidance have
also to be considered to validate CPSs. To meet this need, we
propose in this paper a framework, based on abstract domains, for
solving constraint satisfaction problems where the objects
manipulated are described by ODEs. We use a form of disjunctive
completion for which we provide a split operator and an efficient
constraint filtering mechanism that takes advantage of the
continuity aspect of ODEs. We illustrate the benefits of our method
on a real-world application of trajectory validation of a swarm of
drones, for which the main property we aim to prove is the absence
of collisions between drone trajectories. Our work has been
concretized in the form of a cooperation between the DynIbex
library, used for the abstraction of ODEs, and the AbSolute
constraint solver, used for the constraint resolution. Experiments
show promising results.
@InProceedings{NSAD20p2,
author = {Ghiles Ziat and Olivier Mullier and Julien Alexandre dit Sandretto and Christophe Garion and Alexandre Chapoutot and Xavier Thirioux},
title = {Abstract Domains for Constraint Programming with Differential Equations},
booktitle = {Proc.\ NSAD},
publisher = {ACM},
pages = {2--11},
doi = {10.1145/3427762.3429453},
year = {2020},
}
Publisher's Version
Numeric Domains Meet Algebraic Data Types
Santiago Bautista,
Thomas Jensen, and
Benoît Montagu
(ENS Rennes, France; Inria, France)
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.
@InProceedings{NSAD20p12,
author = {Santiago Bautista and Thomas Jensen and Benoît Montagu},
title = {Numeric Domains Meet Algebraic Data Types},
booktitle = {Proc.\ NSAD},
publisher = {ACM},
pages = {12--16},
doi = {10.1145/3427762.3430178},
year = {2020},
}
Publisher's Version
Proving Array Properties using Data Abstraction
Julien Braine and
Laure Gonnord
(University of Lyon, France; CNRS, France; Inria, France; LIP, France)
This paper presents a framework to abstract data structures within Horn clauses
that allows abstractions to be easily expressed, compared, composed
and implemented. These abstractions introduce new quantifiers that we eliminate with quantifier elimination techniques.
We study the case of arrays and our experimental evaluation show promising results on classical array programs.
@InProceedings{NSAD20p17,
author = {Julien Braine and Laure Gonnord},
title = {Proving Array Properties using Data Abstraction},
booktitle = {Proc.\ NSAD},
publisher = {ACM},
pages = {17--21},
doi = {10.1145/3427762.3430179},
year = {2020},
}
Publisher's Version
Info
proc time: 2.06