Ackermann reduction

F is x = z /\ f(x) = f(y) can be represented without `f’ in case of uninterpreted `f’ ! by the following way:
let v1 = f(x), let v2 = f(y), so
F’ is (x = y -> v1 = v2) -> ( x = z /\ v1 = v2 ). F and F’ are valid-equivalent.

If we have more accesses to `f’, additional transitivity constraints must be added. The drawback is growth of F’ size.

I’m wondering but this obvious way has a special name! Ackerman reduction! (may be after the following article: “Ackerman W. (1954) Solvable Cases of the Decision Problem” – I can’t find it on Internet )

Similar constraints should be useful for describing effect of memory sequence (`f’ is memory, argument of `f’ is memory address, `read’ operation is using `f’ access, `write’ is changing a value of `f’ for the specific address).

// by articles of R.Bryant and M.Vinov on the microprocessor verification using SAT, f.e. “TLSim and EVC: A Term-Level Symbolic Simulator and an Efficient Decision Procedure for the Logic of Equality with Uninterpreted Functions and Memories”

Another bug in Yices ?

Yices gets `Illegal instruction’ on the following “program”:

(define-type A)
(define-type B (bitvector 31))
(define-type C (bitvector 24))
(define f::(-> A (subrange 0 3)))
(define g::(-> A A bool))
(define h :: (-> B C) (lambda (x :: B) (bv-extract 30 7 x)))
(assert (forall (x::A y::A)(=> (= x y) (g x y))))
(assert (forall (x::A y::A)(=> (g x y) (= (f x) (f y) ))))
(define ts0 :: A )
(define v_ts0 :: B )
(assert (= (f ts0) 2))
(define ts1 :: A )
(define v_ts1 :: B )
(assert (= (f ts1) 2))
(assert (=> (and (= (f ts1) 1) (= 1 (f ts0) ))(/= (h v_ts1) (h v_ts0))))
(assert (not (g ts0 ts1)))
(assert (=> (< (f ts0) 2)(= (= ts0 ts1) (= v_ts0 v_ts1) )))
(check)

Is it bug or feature?

The Effect of Nogood Recording in DPLL-CBJ SAT Algorithms

Authors: Inês Lynce, João Marques-Silva (Technical University of Lisbon, IST/INESC/CEL, Lisbon, Portugal)
Link: pdf

Articles contains wonderful terminology survey about CSP and SAT. I want to present this terminology and abbreviations. The main idea of DPLL is backtracking search. DPLL-based algorithms (core of SAT-solvers) have optimized scheme of this search. The main idea of MAC is

BCP – Boolean Constraint Propagation. Point of joining DPLL and MAC. Propagation of boolean constraints is similar to the backtracking search!

NCB – Non-Chronological Backtracking. Backtracking is also returns to the parent node of selection. But it is may be more efficient to return not to the direct parent but to the parent of parent or parent of parent of parent, etc.

CBJ – Conflict-directed BackJumping. It is a method of NCB. It gets a way to define a point to return. This point is conflict-node. If this point is set to unusual value, all formula is inconsistent. So other value must be used for this point. This is achieved by backjumping to this point.

Learning (Nogoods). It is a method of adding new constraints to prevent occured conflict (i.e. assignment of variables on which formula is inconsistent).

GBJ – Graph-Based Jumping. Point of backjumping is defined based on constraint graph.

BDD – Binary Decision Diagrams. ROBDD – Reduced Ordered BDD. They are very effective representation of the boolean formula. So every boolean formula transformation algorithm can be implemented using BDD transformations! BDD is also structure representation, it is not algorithm itself.

Main conferences on solvers, test generation, formal verification, etc. of software/hardware

VERIFY – International Verification Workshop (5th – VERIFY’08) http://www.uni-koblenz.de/~beckert/verify08/

SAT – International Conference on Theory and Applications of Satisfiability Testing (12th – SAT 2009) http://www.cs.swan.ac.uk/~csoliver/SAT2009/

CFV – International Workshop on Constraints in Formal Verification (5th – CFV’08) http://www.miroslav-velev.com/cfv08.html

TAP – International Conference on Tests and Proofs (2nd – TAP’08) http://www.uni-koblenz.de/~tap2008/

TACAS – International Conference on TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS (15th – TACAS’09) http://www.embedded.rwth-aachen.de/tacas2009/

APV – Symposium on Automatic Program Verification http://se.ethz.ch/apv/

SSV – International Workshop on Systems Software Verification (4th – SSV’09) http://www.embedded.rwth-aachen.de/ssv09

HVC – Haifa Verification Conference http://www.haifa.ibm.com/conferences/hvc2009/

Another bug in Yices 1.0.21 I found (now in Linux version)

The following program writes to only “system1.txt” but not to different “systemNNN.txt” at the different calls on Linux:

               YicesLite yl = new YicesLite();
               yl.yicesl_enable_log_file("system" + (++nnn) + ".txt" );
               yl.yicesl_set_output_file("system-output" + nnn + ".txt");
               int context = yl.yicesl_mk_context();
               ...
               yl.yicesl_del_context(context);

yicesl_set_output_file works well.

MathSAT and Verifying Heap-Manipulating Programs

Authors: Zvonimir Rakamaríc, Roberto Bruttomesso , Alan J. Hu , and Alessandro Cimatti (MathSAT developer)

MathSAT webpage: http://mathsat.itc.it

Core article: “Verifying Heap-Manipulating Programs in an SMT Framework” (pdf).

Heap-manipulating programs can do incorrent operations due to hard manipulation with dynamic objects in memory. So problem of verification such programs is important. Authors have developed theory of heap-manipulations and incorporated in to MathSAT SMT-solver. They use delayed theory combination (DTC) feature of MathSAT. This feature is a novel way to integrate a lot of theories in one solver. Core article contains brief summary of DTC and Nelson-Oppen combination (another theories combination procedure for SMT-solvers).

My article on EWDTS’09

Commit article ‘SMT-based Test Program Generation for Cache-memory Testing’ on http://www.ewdtest.com/conf/ (Moscow, September 18-21, 2009)

Yices Java API Lite for Windows

I have compiled Yices Java API Lite from http://atlantis.seidenberg.pace.edu/wiki/lep/Yices%20Java%20API%20Lite on Windows.

The results are:

http://tesla-project.googlecode.com/files/libYicesLite.dll

http://tesla-project.googlecode.com/files/YicesLite.jar

More information in my Russian blog: http://kornevgen.blogspot.com/2009/05/yices-java-windows.html

Found bug in Yices 1.0.21 :)

Segmentation fault on Linux version


(define-type t)
(define p::(-> t (subrange 0 3)))
(define vvv::(-> t t bool))
(assert (forall (x::t y::t) (=> (vvv x y) (p x y))))
(define ts1::t)
(assert (>= (p ts1 2)) )


Solvers

World of solvers:

MAC-solvers + IC (finite domains and intervals)  : ECLiPSe

SAT-solvers (DPLL) :

SMT-solvers (DPLL + special theories) : Yices, Z3, CVC3

BDD representation of predicates and special algorithms for BDD operations (BDD algebra) : used mostly for `model checking’ (verification problem – not testing – but can be formulated with test generation aims) but some researchers consider DPLL implementation on BDD.

What else ?