1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
+++
title = "The need for abstract predicates"
date = "2022-07-19"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3c3g5"]
forwardlinks = ["3c3g7", "3c3g6a"]
zettelid = "3c3g6"
+++
In the previous version of the abstract language with predicated
expressions, the predicates were concrete, which is wrong because they
will then always be executed with respect to the original context. The
way this can be fixed is by also keeping track of abstract predicates,
however, then one ends up with predicates that might themselves be
predicated. Currently, the idea is to recombine these into a predicate
whenever this is needed, by anding all the elements in the list
together. This generates massive predicates because at each exit and
each predicate assignment, the predicates are multiplied together. Most
of the time, these predicates are very easy to solve, however, after
using the tseytin transformation, many additional variables are added
which makes it much harder to solve.
In general though, it seems like this analysis is at least correct,
meaning it can find bugs hopefully.
|
