What we do in Lugano

Lab research deals with improving the program development process through formal methods of specification and verification. Our interests lie in software and hardware verification, temporal logics, model checking, SAT/SMT methods, and concurrent and distributed computing.

One of our special interests is information security: in this area we develop new techniques that are exhaustive and formally guarantee the correctness of security properties of the actual implementation given in languages such as ANSI-C. Our techniques target detection of faults that arise from two sources: a) the programmer may unintentionally introduce a bug that is exploitable (e.g., buffers with insufficient bounds checks), and b) an adversary may hide exploitable code in the software.