NSAD 2020: Proceedings of the 9th ACM SIGPLAN International Workshop on Numerical and Symbolic Abstract Domains

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.

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.

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.

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.