DPOP

A DPOP implementation for solving DCOP problems.

It uses a simple textual input format, initially developed for describing Multi Robot Patrolling instances, but quite general to be used for any distributed constraint optimization problem.

The program can be started using the script dpop or executing the JAR file directly.
 

The archive with sources and binaries.

The JAR-only archive.

An introductory article (in Italian).

A set of linear test instances.

A set of grid test instances.

TeePee, a theorem prover

TeePee is a simple theorem prover for CNF FOL formulae.
It doesn't aim to be a fully featured prover (like Prover9, E and others) but rather an "educational toy", to show a simple implementation of concepts practically used in automated reasoning (being written in one week for a course assignment).

Many things can be improved - for example, ProcessorTest needs a lot of refactoring.

The program can be started using the script teepee or executing the JAR file directly.

Note: on page 4 of the article the problems PLA001-1.p, PLA002-1.p and PLA003-1.p are reported to be satisfiable, which is wrong! I think that's because I considered only clauses marked as "negated conjecture" to belong to the set of support - indeed not using the set-of-support strategy (not using the -sos flag) correctly reports "unsatisfiable".

 

The archive with sources and binaries.

The JAR-only archive.

An introductory article (in Italian).

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!