The University of Southampton

Publications

Madhusudan, P. and Parlato, Gennaro (2011) The tree width of auxiliary storage. At POPL '11. Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL '11. Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, United States. 26 - 28 Jan 2011. pp. 283-294. (doi:10.1145/1925844.1926419).

Madhusudan, P., Parlato, Gennaro and Qiu, Xiaokang (2011) Decidable logics combining heap structures and data. At POPL '11. Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL '11. Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, United States. 26 - 28 Jan 2011. pp. 611-622.

Atig, Mohamed Faouzi, Bouajjani, Ahmed and Parlato, Gennaro (2011) Getting rid of store-buffers in TSO analysis. At 23rd International Conference on Computer Aided Verification (CAV 2011) 23rd International Conference on Computer Aided Verification (CAV 2011), United States. 14 - 20 Jul 2011. 16 pp, pp. 99-115.

Bouajjani, Ahmed, Emmi, Michael and Parlato, Gennaro (2011) On Sequentializing Concurrent Programs. At SAS SAS, Italy. 14 - 16 Sep 2011.

La Torre, Salvatore, Madhusudan, P. and Parlato, Gennaro (2012) Sequentializing parameterized programs. At 4th International Workshop on Foundations of Interface Technologies 4th International Workshop on Foundations of Interface Technologies. 21 pp.

Torre, Salvatore La, Madhusudan, P. and Parlato, Gennaro (2010) Model-Checking Parameterized Concurrent Programs Using Linear Interfaces. At CAV CAV, United Kingdom. 15 - 19 Jul 2010. pp. 629-644.

La Torre, Salvatore, Madhusudan, P. and Parlato, Gennaro (2010) The Language Theory of Bounded Context-Switching. At LATIN LATIN, Mexico. 19 - 23 Apr 2010. pp. 96-107.

Torre, Salvatore La, Madhusudan, P. and Parlato, Gennaro (2009) Reducing Context-Bounded Concurrent Reachability to Sequential Reachability. At CAV CAV, France. 26 Jun - 02 Jul 2009. pp. 477-492.

Torre, Salvatore La, Madhusudan, Parthasarathy and Parlato, Gennaro (2009) Analyzing recursive programs using a fixed-point calculus. At PLDI '09. Proceedings of the 2009 ACM SIGPLAN conference on Programming Language Design and Implementation PLDI '09. Proceedings of the 2009 ACM SIGPLAN conference on Programming Language Design and Implementation, Ireland. 15 - 21 Jun 2009. pp. 211-222. (doi:10.1145/1543135.1542500).

Ferrante, Alessandro, Parlato, Gennaro, Sorrentino, Francesco Sorrentino and Ventre, Carmine (2009) Fast payment schemes for truthful mechanisms with verification. Theor. Comput. Sci., 410 (8-10), 886-899.

Torre, Salvatore La, Madhusudan, P. and Parlato, Gennaro (2008) An Infinite Automaton Characterization of Double Exponential Time. At CSL CSL, Italy. 16 - 19 Sep 2008. pp. 33-48.

Carrabs, Francesco, Cerulli, Raffaele, Gentili, Monica and Parlato, Gennaro (2011) A tabu search heuristic based on k-diamonds for the weighted feedback vertex set problem. Network Optimization: 5th International Conference, (INOC), Germany. 13 - 16 Jun 2001. (In Press)

Torre, Salvatore La, Madhusudan, P. and Parlato, Gennaro (2008) Context-Bounded Analysis of Concurrent Queue Systems. At TACAS TACAS, Hungary. 29 Mar - 06 Apr 2008. pp. 299-314.

Torre, Salvatore La, Napoli, Margherita, Parente, Mimmo and Parlato, Gennaro (2008) Verification of scope-dependent hierarchical state machines. Inf. Comput., 206 (9-10), 1161-1177.

Torre, Salvatore La and Parlato, Gennaro (2007) On the Complexity of LtlModel-Checking of Recursive State Machines. At ICALP ICALP, Poland. 09 - 13 Jul 2007. pp. 937-948.

Torre, Salvatore La, Madhusudan, Parthasarathy and Parlato, Gennaro (2007) A Robust Class of Context-Sensitive Languages. At LICS LICS, Poland. 10 - 12 Jul 2007. pp. 161-170.

Ferrante, Alessandro, Parlato, Gennaro, Sorrentino, Francesco and Ventre, Carmine (2005) Improvements for Truthful Mechanisms with Verifiable One-Parameter Selfish Agents. At WAOA WAOA. pp. 147-160.

Carrabs, Francesco, Cerulli, Raffaele, Gentili, Monica and Parlato, Gennaro (2005) A linear time algorithm for the minimum Weighted Feedback Vertex Set on diamonds. Inf. Process. Lett., 94 (1), 29-35.

Carrabs, Francesco, Cerulli, Raffaele, Gentili, Monica and Parlato, Gennaro (2004) Minimum Weighted Feedback Vertex Set on Diamonds. At CTW CTW. pp. 81-85.

Torre, Salvatore La, Napoli, Margherita, Parente, Mimmo and Parlato, Gennaro (2003) Hierarchical and Recursive State Machines with Context-Dependent Properties. At ICALP ICALP. 30 Jun - 04 Jul 2003. pp. 776-789.

La Torre, Salvatore and Gennaro, Parlato (2012) Scope-bounded multistack pushdown systems: fixed-point, sequentialization, and tree-width. At 32nd Foundations of Software Technology and Theoretical Computer Science Conference (FSTTCS) 32nd Foundations of Software Technology and Theoretical Computer Science Conference (FSTTCS), India. 15 - 17 Dec 2012. 12 pp, pp. 173-184.

Uzun, Emre, Atluri, Vijayalakshmi, Sural, Shamik, Vaidya, Jaideep, Gennaro, Parlato, Ferrara, Anna Lisa and Madhusudan, Parthasarathy (2012) Analyzing temporal role based access control models. In SACMAT '12 Proceedings of the 17th ACM symposium on Access Control Models and Technologies. ACM. 177 -186. (doi:10.1145/2295136.2295169).

Ferrara, Anna Lisa, Madhusudan, P. and Parlato, Gennaro (2013) Policy analysis for self-administrated role-based access control. At TACAS 2013: 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) TACAS 2013: 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Italy. 16 - 24 Mar 2013. 15 pp.

Ferrara, Anna Lisa, Madhusudan, P. and Parlato, Gennaro (2012) Security Analysis of Role-based Access Control through Program Verification. At 25th IEEE Computer Security Foundations Symposium (CSF) 25th IEEE Computer Security Foundations Symposium (CSF). 13 pp, pp. 113-125.

Fischer, Bernd, Inverso, Omar and Parlato, Gennaro (2013) CSeq: A Sequentialization Tool for C - (Competition Contribution). At Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013 Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013. pp. 616-618.

Garg, Pranav, Madhusudan, P. and Parlato, Gennaro (2013) Quantified Data Automata on Skinny Trees: an Abstract Domain for Lists. At 20th Static Analysis Symposium 20th Static Analysis Symposium.

Enea, Constantin, Habermehl, Peter, Inverso, Omar and Parlato, Gennaro (2014) On the Path-Width of Integer Linear Programming. At Fifth International Symposium on Games, Automata, Logics and Formal Verification (GandALF) Fifth International Symposium on Games, Automata, Logics and Formal Verification (GandALF), Italy.

Inverso, Omar, La Torre, Salvatore, Tomasco, Ermenegildo and Parlato, Gennaro (2013) Looking at Computations from a Different Angle University of Southampton ,

La Torre, Salvatore, Napoli, Margherita and Parlato, Gennaro (2013) On Multi-stack Visibly Pushdown Languages. 20 pp.

Tomasco, Ermenegildo, Inverso, Omar, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2014) MU-CSeq: sequentialization of c programs by shared memory unwindings (competition contribution). At TACAS (SV-COMP) TACAS (SV-COMP).

Inverso, Omar, Tomasco, Ermenegildo, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2014) Lazy-CSeq: a lazy sequentialization tool for c (competition contribution). At Tools and Algorithms for the Construction and Analysis of Systems - TACAS (SV-COMP) Tools and Algorithms for the Construction and Analysis of Systems - TACAS (SV-COMP).

La Torre, Salvatore, Napoli, Margherita and Parlato, Gennaro (2014) Scope-bounded pushdown languages. At 18th International Conference on Developments in Language Theory (DLT 2014) 18th International Conference on Developments in Language Theory (DLT 2014), Russian Federation. 26 - 29 Aug 2014. 12 pp.

Atig, Mohamed Faouzi, Bouajjani, Ahmed and Parlato, Gennaro (2014) Context-bounded analysis of tso systems, vol. 8415, Springer (Lecture Notes in Computer Science, 8415) ,

Ferrara, Anna Lisa, Madhusudan, P., Lam Nguyen, Truc and Parlato, Gennaro (2014) VAC - verifier of administrative role-based access control policies. At 26th International Conference on Computer Aided Verification (CAV 2014) 26th International Conference on Computer Aided Verification (CAV 2014), Austria. 18 - 22 Jul 2014. 8 pp.

Inverso, Omar, Tomasco, Ermenegildo, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2014) Bounded model checking of multi-threaded c programs via lazy sequentialization. At 26th International Conference on Computer Aided Verification (CAV 2014) 26th International Conference on Computer Aided Verification (CAV 2014), Austria. 18 - 22 Jul 2014. 18 pp.

Fischer, Bernd, Inverso, Omar and Parlato, Gennaro (2013) CSeq: a concurrency pre-processor for sequential c verification tools (tool demonstration). At 28th IEEE/ACM International Conference on Automated Software Engineering (ASE) 28th IEEE/ACM International Conference on Automated Software Engineering (ASE).

La Torre, Salvatore, Napoli, Margherita and Parlato, Gennaro (2014) A unifying approach for multistack pushdown automata. At 39th International Symposium on Mathematical Foundations of Computer Science (MFCS 2014) 39th International Symposium on Mathematical Foundations of Computer Science (MFCS 2014), Hungary. 25 - 29 Aug 2014. 18 pp.

Inverso, Omar, Tomasco, Ermenegildo, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2014) Lazy-CSeq: a lazy sequentialization tool for C. At 20th International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 20th International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 05 - 13 Apr 2014. pp. 398-401.

Uzun, Emre, Atluri, Vijayalakshmi, Vaidya, Jaideep, Sural, Shamik, Ferrara, Anna Lisa, Parlato, Gennaro and Madhusudan, P. (2014) Security analysis for temporal role based access control. Journal of Computer Security.

Tomasco, Ermenegildo, Inverso, Omar, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2015) Verifying concurrent programs by memory unwinding. 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), United Kingdom. 11 - 15 Apr 2015. 15 pp.

Tomasco, Ermenegildo, Inverso, Omar, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2015) MU-CSeq 0.3: Sequentialization by read-implicit and coarse-grained memory unwindings (competition contribution). At 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), United Kingdom. 11 - 15 Apr 2015. 3 pp.

Lam Nguyen, Truc, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2015) Unbounded Lazy-CSeq: a lazy sequentialization tool for C programs with unbounded context switches (competition contribution). 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), United Kingdom. 11 - 15 Apr 2015. 3 pp.

Inverso, Omar, Tomasco, Ermenegildo, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2014) Lazy-CSeq 0.6c: An improved lazy sequentialization tool for C (competition contribution) Southampton, GB. University of Southampton 3pp. ,

La Torre, Salvatore, Napoli, Margherita, Parente, Mimmo and Parlato, Gennaro (2007) Verification of Succinct Hierarchical State Machines. At Conference on Language and Automata Theory and Applications (LATA) Conference on Language and Automata Theory and Applications (LATA).

Carrabs, Francesco, Cerulli, Raffaele, Gentili, Monica and Parlato, Gennaro (2004) Minimum Weighted Feedback Vertex Set on Diamonds. Electronic Notes in Discrete Mathematics, 17, 87-91. (doi:10.1016/j.endm.2004.09.001).

Inverso, Omar, Nguyen Lam, Truc, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2015) Lazy-CSeq: A Context-Bounded Model Checking Tool for Multi-Threaded C-Programs. At 30th IEEE/ACM International Conference on Automated Software Engineering (ASE 2015) 30th IEEE/ACM International Conference on Automated Software Engineering (ASE 2015).

Parlato, Gennaro (2015) On Sequentializing Concurrent Programs. At UPMARC Summer School on Multicore Computing 2015 UPMARC Summer School on Multicore Computing 2015, Sweden.

Parlato, Gennaro (2015) On Sequentializing Concurrent Programs -- Bounded Model Checking. UPMARC Summer School on Multicore Computing 2015, Sweden.

Tomasco, Ermenegildo, Nguyen, Truc, Inverso, Omar, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2016) MU-CSeq 0.4: individual memory location unwindings: (competition contribution). 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS).

Enea, Constantin, Habermehl, Peter, Inverso, Omar and Parlato, Gennaro (2017) On the path-width of integer linear programming. Information and Computation, 257-271. (doi:10.1016/j.ic.2016.07.010).

La Torre, Salvatore, Napoli, Margherita and Parlato, Gennaro (2016) Scope-Bounded Pushdown Languages. International Journal of Foundations of Computer Science, 27 (2), 215-233.

Inverso, Omar, Nguyen, Truc, Tomasco, Ermenegildo, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2015) Lazy-CSeq 1.0:(Competition Contribution) University of Southampton ,

Nguyen, Truc, Inverso, Omar, Tomasco, Ermenegildo, La Torre, Salvatore, Fischer, Bernd and Parlato, Gennaro (2015) Unbounded Lazy-CSeq: A Lazy Sequentialization Tool for C with unboundedly many Context Switches: (Competition Contribution) University of Southampton ,

Nguyen Lam, Truc, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2016) Lazy sequentialization for the safety verification of unbounded concurrent programs. 14th International Symposium on Automated Technology for Verification and Analysis (ATVA), Japan. 17 - 19 Oct 2016. 16 pp. (In Press)

Tomasco, Ermenegildo, Nguyen Lam, Truc, Inverso, Omar, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2016) Lazy Sequentialization for TSO and PSO via Shared Memory Abstractions. At Formal Methods in Computer-Aided Design (FMCAD) Formal Methods in Computer-Aided Design (FMCAD), United States. 02 - 06 Oct 2016.

Tomasco, Ermenegildo, Nguyen Lam, Truc, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2016) Separating computation from communication: a design approach for concurrent program verification Southampton, GB. University of Southampton 31pp. ,

Tomasco, Ermenegildo, Nguyen Lam, Truc, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2016) Embedding weak memory models within eager sequentialization Southampton, GB. University of Southampton 29pp. ,

NGUYEN, TRUC L, Inverso, Omar, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2017) Lazy-CSeq 2.0: combining lazy sequentialization with abstract interpretation: (Competition contribution). Legay, Axel and Margaria, Tiziana (eds.) In Tools and Algorithms for the Construction and Analysis of Systems. vol. 10206, Springer. 4 pp. (doi:10.1007/978-3-662-54580-5_26).

Nguyen, Truc L., Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2017) Concurrent program verification with Lazy sequentialization and interval analysis. In The 5th Edition of The International Conference on Networked sYStems. Springer. 15 pp, pp. 255-271. (doi:10.1007/978-3-319-59647-1_20).

Tomasco, Ermenegildo, Nguyen, Truc, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2017) Using shared memory abstractions to design eager sequentializations for weak memory models. In SEFM 2017: Software Engineering and Formal Methods. vol. 10469, Springer. pp. 185-202. (doi:10.1007/978-3-319-66197-1_12).

Uzun, Emre, Parlato, Gennaro, Atluri, Vijayalakshmi, Ferrara, Anna Lisa, Vaidya, Jaideep, Sural, Shamik and Lorenzi, David (2017) Preventing unauthorized data flows. Livraga, G. and Zhu, S. (eds.) In Data and Applications Security and Privacy XXXI. DBSec 2017. vol. 10359, Springer. 0 pp, pp. 41-62.

Nguyen Lam, Truc, Schrammel, Peter, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2017) Parallel bug-finding in concurrent programs via reduced interleaving instances. Rosu, Grigore, Di Penta, Massimiliano and Nguyen, Tien N. (eds.) In ASE '17: Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering. IEEE. pp. 753-764.

Contact

Share this profile FacebookGoogle+TwitterWeibo

We use cookies to ensure that we give you the best experience on our website. If you continue without changing your settings, we will assume that you are happy to receive cookies on the University of Southampton website.

×