Gennaro Parlato





Current Position
I'm a postdoc research associate in the Department of Computer Science at UIUC (USA).  My CV is available here.

Research Interests
   - Software analysis and verification
   - Model checking: algorithms and tools
   - Logic, automata theory, and graph theory

Contact Information







Tools
   GetAFix (A Boolean program checker)

Papers
● Sequentializing Parameterized Programs.
with S. La Torre, and P. Madhusudan.
Under Submission. 2009.
● The Language Theory of Bounded Context-Switching.
with S. La Torre, and P. Madhusudan.
9th Latin American Theoretical Informatics Symposium (LATIN).
Oaxaca, México, 2010.
PDF
● Reducing Context-bounded Concurrent Reachability to Sequential Reachability.
with S. La Torre, and P. Madhusudan.
21st International Conference on Computer Aided Verification (CAV).
Grenoble, France, 2009.
PDF, PPT
See also the cbp2bp page.
● 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
● Improvements for Truthful Mechanisms with Verifiable One-Parameter Selfish Agents.
with A. Ferrante,  F. Sorrentino, and C. Ventre.
Theoretical Computer Science (TCS) 2009.
PDF
● 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
● Verification of Scope-Dependent Hierarchical State Machines.
with S. La Torre, M. Napoli, and M. Parente.
Information and Computation 2008.
PDF
● Context-Bounded Analysis of Concurrent Queue Systems.
with S. La Torre, and P. Madhusudan.
14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
Budapest, Hungary, 2008.
PDF, PPT
● 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
● On the Complexity of LTL Model-Checking of Recursive State Machines.
with S. La Torre.
34th International Colloquium on Automata, Languages and Programming (ICALP)
Wroclaw, Poland, 2007.
PDF
● Verification of Succinct Hierarchical State Machines.
with S. La Torre, M. Napoli, and M. Parente.
1st International Conference on Language and Automata Theory and Applications (LATA)
Tarragona, Spain, 2007.
PDF
● 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
● 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
● Minimum Weighted Feedback Vertex Set on Diamonds.
with F. Carrabs, R. Cerulli, and M. Gentili.
Electronic Notes in Discrete Mathematics (ENDM), 2004.
● Hierarchical and Recursive State Machines with Context-Dependent Properties.
with S. La Torre, M. Napoli, and M. Parente.
30th International Colloquium on Automata, Languages and Programming (ICALP)
Eindhoven, The Netherlands, 2003.
PDF