100
D. Ahmed et al.
SAT-based CEGIS implementation, which automates the construction of Lyapunov functions and associated validity domains, which is is sound, and also
applicable to parameterised models.
The remainder of the paper is organised as follows. In Section 2 we present the
SMT Z3 solver and the inductive synthesis (IS) framework. The implementation
of CEGIS, for both linear and non-linear models, is explained in Section 3.
Experiments and case studies are in Section 4. Finally, conclusions are drawn in
Section 5.
2 Formal Verification – Concepts and Techniques
In this work we use Z3, an SMT solver, and the CEGIS architecture, to build
and to verify Lyapunov functions.
2.1 Satisfiability Modulo Theory
A Satisfiability Modulo Theory problem is a decision problem formulated within
a theory, e.g. first-order logic with equality [28]. The aim is to check whether a
first-order logical formula within such theory, referred to as an SMT instance, is
satisfied. For example, a formula can be the inequality 3x 0 + x 1 > 0 evaluated
within the theory of linear inequalities. An SMT solver is a software that checks
the satisfiability of an SMT instance, i.e. whether there exists an instantiation
of the formula that evaluates to True. SMT solvers can be useful for function
synthesis, namely to mechanically construct a function, given requirements on
its output.
2.2 The Z3 SMT Solver
Z3 [11,29] is a powerful SMT solver that integrates SAT solvers, theory solvers for
equalities and interpreted functions, satellite solvers for arithmetic, real, array,
and other theories, and an abstract machine to handle quantifiers. Receiving
an input formula, Z3 represents it as an abstract syntax tree and processes it
with its SAT solver core, until it returns SAT if the formula is satisfiable, UNSAT
otherwise.
Example 1 (Operation of Z3). Consider the formula a = b ∧ f (a) = f (b) in the
theory of equality. To verify its satisfiability, Z3 constructs a syntax tree, with
nodes for each variable (a, b) and formulae (a = b, f (a), f (b), f (a) = f (b)). Once
the tree is built, Z3 merges a with b and f (a) with f (b) to represent the equality
operation and, in order to verify the correctness of the assertion, applies the
congruence rule
n−1
i=0 x i = y i ⇒ f (x 0 , . . . x n−1 ) = f (y 0 , . . . y n−1 ) to conclude
that a = b ⇒ f (a) = f (b). Finally, nodes a = b and f (a) = f (b) are merged and
Z3 returns SAT.
D. Ahmed et al.
SAT-based CEGIS implementation, which automates the construction of Lyapunov functions and associated validity domains, which is is sound, and also
applicable to parameterised models.
The remainder of the paper is organised as follows. In Section 2 we present the
SMT Z3 solver and the inductive synthesis (IS) framework. The implementation
of CEGIS, for both linear and non-linear models, is explained in Section 3.
Experiments and case studies are in Section 4. Finally, conclusions are drawn in
Section 5.
2 Formal Verification – Concepts and Techniques
In this work we use Z3, an SMT solver, and the CEGIS architecture, to build
and to verify Lyapunov functions.
2.1 Satisfiability Modulo Theory
A Satisfiability Modulo Theory problem is a decision problem formulated within
a theory, e.g. first-order logic with equality [28]. The aim is to check whether a
first-order logical formula within such theory, referred to as an SMT instance, is
satisfied. For example, a formula can be the inequality 3x 0 + x 1 > 0 evaluated
within the theory of linear inequalities. An SMT solver is a software that checks
the satisfiability of an SMT instance, i.e. whether there exists an instantiation
of the formula that evaluates to True. SMT solvers can be useful for function
synthesis, namely to mechanically construct a function, given requirements on
its output.
2.2 The Z3 SMT Solver
Z3 [11,29] is a powerful SMT solver that integrates SAT solvers, theory solvers for
equalities and interpreted functions, satellite solvers for arithmetic, real, array,
and other theories, and an abstract machine to handle quantifiers. Receiving
an input formula, Z3 represents it as an abstract syntax tree and processes it
with its SAT solver core, until it returns SAT if the formula is satisfiable, UNSAT
otherwise.
Example 1 (Operation of Z3). Consider the formula a = b ∧ f (a) = f (b) in the
theory of equality. To verify its satisfiability, Z3 constructs a syntax tree, with
nodes for each variable (a, b) and formulae (a = b, f (a), f (b), f (a) = f (b)). Once
the tree is built, Z3 merges a with b and f (a) with f (b) to represent the equality
operation and, in order to verify the correctness of the assertion, applies the
congruence rule
n−1
i=0 x i = y i ⇒ f (x 0 , . . . x n−1 ) = f (y 0 , . . . y n−1 ) to conclude
that a = b ⇒ f (a) = f (b). Finally, nodes a = b and f (a) = f (b) are merged and
Z3 returns SAT.