Gennaro Parlato homepage

                Gennaro Parlato

Current Position
I am a Lecturer of Computer Science in the School of Electronics and Computer Science at the University of Southampton. I am a member of the Electronic & Software Systems research group.

Short Biography
I received my doctoral degree in Computer Science in April 2006 from the University of Salerno (Italy). Before joining the University of Southampton as a Lecturer, I was a CNRS postdoc research associate in the Modeling and Verification group at LIAFA laboratory (Paris, France, April 2010-April 2011), and a postdoc research associate in the Department of Computer Science at UIUC (Urbana, USA, May 2006-March 2010).

My CV is available here.

Research Interests
   - Software analysis and verification
   - Model checking: algorithms and tools
   - Verification of Concurrent Software
   - Security
   - Logics, automata theory, and graph theory

Current Research Projects
   - Model checking abstractions of concurrent programs using fixed-point (GetAFix)
   - Decidable automata with auxiliary storage
   - Sequentialization of concurrent programs (Cseq)
   - Verification of programs under weak memory models
   - Decidable logics for programs with data structures (STRAND)
   - Verification of ARBAC models (VAC)

Students
   - Omar Inverso (PhD, October 2011 - )
   - Ermenegildo Tomasco (PhD, May 2012- )

Teaching
   - COMP6004: Formal Design of Systems (2012-2013)
   - COMP2011: Theory of Computing        (2012-2013)
   - COMP6004: Formal Design of Systems (2011-2012)

Service
   - PC Member: CAV 2012, Berkeley, USA.
     24th Int'l Conference on Computer Aided Verification.
   - PC Member: MFCS 2012, Bratislava, Slovakia.
     37th Int'l Symposium on Mathematical Foundations of Computer Science.
   - PC Member: GandALF 2010, Minori, Italy.
     1st Int'l Symposium on Games, Automata, Logics and Formal Verification.

Software/Tools
   - GetAFix (A Boolean program checker)
   - STRAND
   - VAC (Verifier for Role Based Access Control Systems)
   - CSeq (Sequentialization tool for C programs+Pthread library)

Papers     (DBLP, Google Scholar)

1.	On Multi-stack Visibly Pushdown Languages with S. La Torre, and M. Napoli. Under submission, 2013. PDF
2.	The Path-Width of Integer Linear Programming with C. Enea, P. Habermehl, O. Inverso. Under submission, 2013. PDF, PPT (containing an open problem related to this paper: ''abab problem'').
3.	Looking at Computations from a Different Angle with O. Inverso, S. La Torre, E. Tomasco. Under submission, 2013. PDF
4.	CSeq: A Concurrency Pre-Processor for Sequential C Verification Tools with B. Fischer, and O. Inverso. Under submission. PDF, CSeq webpage
5.	Quantified Data Automata on Skinny Trees: an Abstract Domain for Lists with P. Garg, P. Madhusudan. 20th Static Analysis Symposium (SAS), Seattle, WA, USA, 2013. PDF, Experiments.
6.	Policy Analysis for Self-Administrated Role-Based Access Control with A. L. Ferrara, and P. Madhusudan. 19th Int'l Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Rome, Italy, 2013. PDF, PPT
7.	CSeq: A Sequentialization Tool for C (Competition Contribution) with B. Fischer, and O. Inverso. 2nd Intl. Competition on Software Verification (SV-COMP), held at TACAS, Rome, Italy, 2013. PDF, CSeq webpage
8.	Scope-bounded Multistack Pushdown Systems: Fixed-Point, Sequentialization, and Tree-Width. with S. La Torre. 32nd Foundations of Software Technology and Theoretical Computer Science conference (FSTTCS) IIIT Hyderabad, India, 2012. PDF, PPT Slides of a presentation I gave at the post-conference workshop on "Verification of Infinite-State Systems": The tree-width of Decidable Problems: PPT (in the last 5 slides you find an open problem on words: "abab problem")
9.	Security Analysis of Role-based Access Control through Program Verification. with A. L. Ferrara, and P. Madhusudan. 25th IEEE Computer Security Foundations Symposium (CSF). Harvard University, Cambridge MA, USA, 2012. PDF, PPT See also the VAC webpage for the tool and experiments
10.	Sequentializing Parameterized Programs. with S. La Torre, and P. Madhusudan. 4th International Workshop on Foundations of Interface Technologies (FIT). Tallinn, Estonia, 2012. PDF, PPT
11.	Analyzing Temporal Role Based Access Control Models with V. Atluri, A. L. Ferrara, P. Madhusudan, S. Sural, E. Uzun, and J. Vaidya. 17th ACM Symposium on Access Control Models and Technologies (SACMAT). Newark, USA, 2012.
12.	On Sequentializing Concurrent Programs. with A. Bouajjani, and M. Emmi. 18th Int'l Static Analysis Symposium (SAS). Venice, Italy, 2011. PDF, PPT
13.	Getting Rid of Store-Buffers in the Analysis of Weak Memory Models. with F. M. Atig, and A. Bouajjani. 23rd Int'l Conference on Computer Aided Verification (CAV). Cliff Lodge, Snowbird, Utah, USA, 2011. PDF, PPT, Experiments
14.	Decidable Logics Combining Heap Structures and Data. with P. Madhusudan, and X. Qiu. 38th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL) Austin, Texas, USA, 2011. PDF, PPT See also the STRAND webpage for the tool and experiments
15.	The Tree Width of Automata with Auxiliary Storage. with P. Madhusudan. 38th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL) Austin, Texas, USA, 2011. PDF (technical report has more proofs), PPT
16.	A Tabu Search Heuristic Based on k-Diamonds for the Weighted Feedback Vertex Set Problem. with F. Carrabs, R. Cerulli, and M. Gentili. Network Optimization: 5th International Conference, (INOC) Hamburg, Germany, 2011.
17.	Model-checking parameterized concurrent programs using linear interfaces. with S. La Torre, and P. Madhusudan. 22nd Int'l Conference on Computer Aided Verification (CAV). Edinburgh, UK, 2010. PDF
18.	The Language Theory of Bounded Context-Switching. with S. La Torre, and P. Madhusudan. 9th Latin American Theoretical Informatics Symposium (LATIN). Oaxaca, Mexico, 2010. PDF, PPT
19.	Reducing Context-bounded Concurrent Reachability to Sequential Reachability. with S. La Torre, and P. Madhusudan. 21st Int'l Conference on Computer Aided Verification (CAV). Grenoble, France, 2009. PDF, PPT See also the cbp2bp page.
20.	Analyzing Recursive Programs using Fixed-point Calculus. with S. La Torre, and P. Madhusudan. ACM SIGPLAN 2009 Conference on Programming Language Design and Implementation (PLDI). Dublin, Ireland, 2009. PDF, PPT See also the Getafix page for the tool and experiments
21.	Improvements for Truthful Mechanisms with Verifiable One-Parameter Selfish Agents. with A. Ferrante, F. Sorrentino, and C. Ventre. Theoretical Computer Science (TCS) 2009. PDF
22.	An Infinite Automaton Characterization of Double Exponential Time. with S. La Torre, and P. Madhusudan. 17th EACSL Annual Conference on Computer Science Logic (CSL). Bertinoro, Italy, 2008. PDF, PPT
23.	Verification of Scope-Dependent Hierarchical State Machines. with S. La Torre, M. Napoli, and M. Parente. Information and Computation 2008. PDF
24.	Context-Bounded Analysis of Concurrent Queue Systems. with S. La Torre, and P. Madhusudan. 14th Int'l Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) Budapest, Hungary, 2008. PDF, PPT
25.	A Robust Class of Context-Sensitive Languages. with S. La Torre, and P. Madhusudan. 22nd IEEE Symp. on Logic in Computer Science (LICS) Wroclaw, Poland, 2007. PDF
26.	On the Complexity of LTL Model-Checking of Recursive State Machines. with S. La Torre. 34th Int'l Colloquium on Automata, Languages and Programming (ICALP) Wroclaw, Poland, 2007. PDF
27.	Verification of Succinct Hierarchical State Machines. with S. La Torre, M. Napoli, and M. Parente. 1st Int'l Conference on Language and Automata Theory and Applications (LATA) Tarragona, Spain, 2007. PDF
28.	Improvements for Truthful Mechanisms with Verifiable One-Parameter Selfish Agents. with A. Ferrante, F. Sorrentino, and C. Ventre. 3rd Workshop on Approximation and Online Algorithms (WAOA) Palma de Mallorca, Mallorca, Balear Islands, Spain, 2005. PDF
29.	A Linear Time Algorithm for the Minimum Weighted Feedback Vertex Set on Diamonds. with F. Carrabs, R. Cerulli, and M. Gentili. Information Processing Letters (IPL), 2005. PDF
30.	Minimum Weighted Feedback Vertex Set on Diamonds. with F. Carrabs, R. Cerulli, and M. Gentili. Electronic Notes in Discrete Mathematics (ENDM), 2004.
31.	Hierarchical and Recursive State Machines with Context-Dependent Properties. with S. La Torre, M. Napoli, and M. Parente. 30th Int'l Colloquium on Automata, Languages and Programming (ICALP) Eindhoven, The Netherlands, 2003. PDF, PPT