Travelled to:1 × Austria
1 × Hungary
1 × Ireland
1 × Russia
1 × The Netherlands
2 × France
2 × Poland
2 × United Kingdom
3 × Italy
4 × USA
Collaborated with:S.L.Torre P.Madhusudan B.Fischer O.Inverso E.Tomasco T.L.Nguyen M.Napoli A.Bouajjani P.Madhusudan A.L.Ferrara M.Parente P.Garg M.F.Atig X.Qiu M.Emmi P.Schrammel B.F.0002
Talks about:program (10) sequenti (9) seq (8) concurr (7) lazi (7) context (6) contribut (5) competit (5) bound (5) tool (5)
Person: Gennaro Parlato
DBLP: Parlato:Gennaro
Contributed to:
2015
2014
20142014
2013
201320132011
2011201120102009
2009
20082008
2007
2007
20072003201520172019Wrote 28 papers:
- TACAS-2015-Nguyen0TP #bound #c #contest #lazy evaluation #source code
- Unbounded Lazy-CSeq: A Lazy Sequentialization Tool for C Programs with Unbounded Context Switches — (Competition Contribution) (TLN, BF, SLT, GP), pp. 461–463.
- TACAS-2015-TomascoI0TP #contest #memory management
- MU-CSeq 0.3: Sequentialization by Read-Implicit and Coarse-Grained Memory Unwindings — (Competition Contribution) (ET, OI, BF, SLT, GP), pp. 436–438.
- TACAS-2015-TomascoI0TP15a #concurrent #memory management #source code #verification
- Verifying Concurrent Programs by Memory Unwinding (ET, OI, BF, SLT, GP), pp. 551–565.
- CAV-2014-FerraraMNP #data access #named #policy #verification
- Vac — Verifier of Administrative Role-Based Access Control Policies (ALF, PM, TLN, GP), pp. 184–191.
- CAV-2014-InversoT0TP #bound #c #concurrent #lazy evaluation #model checking #multi #source code #thread
- Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization (OI, ET, BF, SLT, GP), pp. 585–602.
- DLT-2014-TorreNP #automaton #bound
- Scope-Bounded Pushdown Languages (SLT, MN, GP), pp. 116–128.
- TACAS-2014-InversoT0TP #c #contest #lazy evaluation #named
- Lazy-CSeq: A Lazy Sequentialization Tool for C — (Competition Contribution) (OI, ET, BF, SLT, GP), pp. 398–401.
- TACAS-2014-TomascoI0TP #c #contest #memory management #named #source code
- MU-CSeq: Sequentialization of C Programs by Shared Memory Unwindings — (Competition Contribution) (ET, OI, BF, SLT, GP), pp. 402–404.
- ASE-2013-0002IP #c #concurrent #named #preprocessor #tool support #verification
- CSeq: A concurrency pre-processor for sequential C verification tools (BF, OI, GP), pp. 710–713.
- SAS-2013-0001MP #abstract domain #automaton #quantifier
- Quantified Data Automata on Skinny Trees: An Abstract Domain for Lists (PG, PM, GP), pp. 172–193.
- TACAS-2013-0002IP #c #contest #named
- CSeq: A Sequentialization Tool for C — (Competition Contribution) (BF, OI, GP), pp. 616–618.
- TACAS-2013-FerraraMP #analysis #data access #policy #self
- Policy Analysis for Self-administrated Role-Based Access Control (ALF, PM, GP), pp. 432–447.
- CAV-2011-AtigBP #analysis
- Getting Rid of Store-Buffers in TSO Analysis (MFA, AB, GP), pp. 99–115.
- POPL-2011-MadhusudanP
- The tree width of auxiliary storage (PM, GP), pp. 283–294.
- POPL-2011-MadhusudanPQ #decidability #logic
- Decidable logics combining heap structures and data (PM, GP, XQ), pp. 611–622.
- SAS-2011-BouajjaniEP #concurrent #on the #source code
- On Sequentializing Concurrent Programs (AB, ME, GP), pp. 129–145.
- CAV-2010-TorreMP #concurrent #interface #linear #model checking #source code #using
- Model-Checking Parameterized Concurrent Programs Using Linear Interfaces (SLT, PM, GP), pp. 629–644.
- CAV-2009-TorreMP #bound #concurrent #reachability
- Reducing Context-Bounded Concurrent Reachability to Sequential Reachability (SLT, PM, GP), pp. 477–492.
- PLDI-2009-TorreMP #calculus #fixpoint #recursion #source code #using
- Analyzing recursive programs using a fixed-point calculus (SLT, PM, GP), pp. 211–222.
- CSL-2008-TorreMP #automaton #exponential #infinity
- An Infinite Automaton Characterization of Double Exponential Time (SLT, PM, GP), pp. 33–48.
- TACAS-2008-TorreMP #analysis #bound #concurrent #queue
- Context-Bounded Analysis of Concurrent Queue Systems (SLT, PM, GP), pp. 299–314.
- ICALP-2007-TorreP #complexity #model checking #on the #recursion #state machine
- On the Complexity of LtlModel-Checking of Recursive State Machines (SLT, GP), pp. 937–948.
- LATA-2007-TorreNPP #state machine #verification
- Verification of Succinct Hierarchical State Machines (SLT, MN, MP, GP), pp. 485–496.
- LICS-2007-TorreMP #context-sensitive grammar #robust
- A Robust Class of Context-Sensitive Languages (SLT, PM, GP), pp. 161–170.
- ICALP-2003-TorreNPP #recursion #state machine
- Hierarchical and Recursive State Machines with Context-Dependent Properties (SLT, MN, MP, GP), pp. 776–789.
- ASE-2015-InversoN0TP #bound #concurrent #model checking #multi #named #thread
- Lazy-CSeq: A Context-Bounded Model Checking Tool for Multi-threaded C-Programs (OI, TLN, BF, SLT, GP), pp. 807–812.
- ASE-2017-NguyenS0TP #concurrent #parallel #source code
- Parallel bug-finding in concurrent programs via reduced interleaving instances (TLN, PS, BF0, SLT, GP), pp. 753–764.
- ASE-2019-FischerTP #concurrent #multi #source code #thread
- VeriSmart 2.0: Swarm-Based Bug-Finding for Multi-threaded Programs with Lazy-CSeq (BF, SLT, GP), pp. 1150–1153.