Satisfiability in the theory of lists

In this post I will present a program for checking the satisfiability of formulae in the list theory, that I developed as a project for a course in program verification.
For example the formula

atom(x) ^ x=cons(y,z)

is clearly unsatisfiable - here "^" means "AND".

It uses the Nelson-Oppen congruence closure algorithm, as described in this book and in this article.
The only requirement is a Java Runtime Environment.

Under UNIX the program can be started with ./listsat. You'll see that the program complains for missing options. If you pass the name of a (well formed) file containing a formula it prints something like:

Loading formula from file: ../random/r3.txt
Loaded after 0.265 secs

Formula contains 95 positive literals, 48 negative literals, 57 atoms (200 total).
Constructing initial DAG...
DAG constructed - time: 0.093
DAG has 921 nodes.
Starting Congruence Closure algorithm...

 ========== ========== ========== ========== ========== ========== [60/200]
 ========== ========== ========== =====*

CC algorithm ended - time: 0.685

Formula is UNSATISFIABLE
Last processed literal: g(h(x,y,f(x,t(x))),f(z,g(y,y)))!=y.



If you want to start the graphical interface pass the option -g.

The ListSAT main window

Here you can generate a random formula

The dialog for running the benchmarks.

The archive with sources and binaries.

The JAR-only archive.

An introductory article (in Italian).

Sicurezza delle Smart Card

Una Smart Card! (da Wikipedia)

An overview (in Italian) of Smart Cards’ Security. It covers power analysis as well as other physical attacks that can break the security of secrets stored in the card.  Of course nothing in this material is original, since it was a course assignment - see the bibliography at pages 15-16.

Oggi pubblico un articolo sulla sicurezza delle smart card, quelle tesserine che abbiamo tutti, in tasca o nel telefono cellulare .
Nell’articolo non troverete niente di originale, visto che è un progetto d’esame,
serve più che altro a introdurre le varie modalità di  attacco ai segreti memorizzati su questi dispositivi, a cui evidentemente i progettisti delle prime smart card non avevano pensato.

Articolo 

Presentazione 

Buona lettura!