The University of Southampton
Email:
et1m11@soton.ac.uk

Ermenegildo Tomasco

Postgraduate research student

I earned a five years University’s degree, grade 110/110 Summa cum Laude,  in Computer Science in February 2002 at University of Salerno (Italy) with a thesis on theorical aspects concerning security and cryptography on Certified email (Certified email: an inline protocol with timestamping). From 2002 to 2005 I worked as web designer for an Italian IT company. Since 2005 to present I have been working for Italian Revenues Agency as an IT expert. At the beginning of 2012 I was awarded with a Master Degree in Interoperability for Public Administration and Networked Enterprises at University of Rome La Sapienza (Grade: 110/110 summa cum laude).

I'm currently a PhD student in Computer Science at the University of Southampton supervised by Gennaro Parlato. My research interests are in Program analysis and Verification, Model-Checking, and Automata Theory.


Current Research Projects

Sequentialization of concurrent programs (CSeq)


Software/Tools

CSeq - Sequentialization tool for concurrent C programs with Pthread library

Papers     (DBLP, Google Scholar)

Bounded Model Checking of Multi-Threaded C Programs via Lazy Sequentialization  
O. InversoE. Tomasco, B. FischerS. La Torre, and G. Parlato.
26th Int'l Conference on Computer Aided Verification (CAV).
Vienna, Austria, 2014.

 PDF, see also CSeq webpage for tools and experiments


Lazy-CSeq: A Lazy Sequentialization Tool for C (Competition Contribution)
O. InversoE. TomascoS. La Torre, Bernd Fischer, and G. Parlato.
3rd Intl. Competition on Software Verification (SV-COMP), held at TACAS,
Grenoble, France, 2014.
[Cseq-Lazy won the gold medal in the concurrency category]

PDF, PPT, CSeq webpage



MU-CSeq: Sequentialization of C Programs by Shared Memory Unwindings (Competition Contribution)
E. Tomasco, O. InversoS. La Torre, Bernd Fischer, and G. Parlato.
3rd Intl. Competition on Software Verification (SV-COMP), held at TACAS,
Grenoble, France, 2014.
[Cseq-MU won the silver medal in the concurrency category]

PDF, PPT, CSeq webpage

Verifying Concurrent Programs by Memory Unwinding
E. Tomasco, O. InversoS. La Torre, Bernd Fischer, and G. Parlato.
21st Int'l Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS),
London, UK,  2015.

MU-CSeq 0.3: Sequentialization by Read-implicit and Coarse-grained Memory Unwindings (Competition Contribution)
E. Tomasco, O. InversoS. La Torre, Bernd Fischer, and G. Parlato.
4th Intl. Competition on Software Verification (SV-COMP), held at TACAS,
London, UK, 2015.
[MU-CSeq won the gold medal in the concurrency category]