Travelled to:
1 × China
1 × Estonia
1 × Russia
1 × Switzerland
2 × Italy
7 × USA
Collaborated with:
A.Rybalchenko W.Chin A.Gupta T.A.Beyene S.Grebenshchikov N.P.Lopes H.H.Nguyen S.Qin S.Khoo D.N.Xu S.Chaudhuri F.Craciun
Talks about:
verifi (6) program (5) thread (4) multi (4) base (4) safeti (3) proof (3) constraint (2) contribut (2) threader (2)
Person: Corneliu Popeea
DBLP: Popeea:Corneliu
Contributed to:
Wrote 15 papers:
- POPL-2014-BeyeneCPR #approach #constraints #game studies #graph #infinity
- A constraint-based approach to solving games on infinite graphs (TAB, SC, CP, AR), pp. 221–234.
- CAV-2013-BeyenePR #horn clause #quantifier
- Solving Existentially Quantified Horn Clauses (TAB, CP, AR), pp. 869–882.
- TACAS-2013-PopeeaR #concurrent #contest #multi #named #source code #thread #verification
- Threader: A Verifier for Multi-threaded Programs — (Competition Contribution) (CP, AR), pp. 633–636.
- PLDI-2012-GrebenshchikovLPR #proving #verification
- Synthesizing software verifiers from proof rules (SG, NPL, CP, AR), pp. 405–416.
- TACAS-2012-GrebenshchikovGLPR #contest #horn clause #verification
- HSF(C): A Software Verifier Based on Horn Clauses — (Competition Contribution) (SG, AG, NPL, CP, AR), pp. 549–551.
- TACAS-2012-PopeeaR #composition #concurrent #multi #proving #source code #termination #thread
- Compositional Termination Proofs for Multi-threaded Programs (CP, AR), pp. 237–251.
- CAV-2011-GuptaPR #concurrent #constraints #multi #named #source code #thread #verification
- Threader: A Constraint-Based Verifier for Multi-threaded Programs (AG, CP, AR), pp. 412–417.
- POPL-2011-GuptaPR #abstraction #concurrent #multi #refinement #source code #thread #verification
- Predicate abstraction and refinement for verifying multi-threaded programs (AG, CP, AR), pp. 331–344.
- SAC-2010-PopeeaC #analysis #debugging #proving #safety
- Dual analysis for proving safety and finding bugs (CP, WNC), pp. 2137–2143.
- SAC-PL-J-2010-PopeeaC13 #analysis #debugging #proving #safety
- Dual analysis for proving safety and finding bugs (CP, WNC), pp. 390–411.
- ISMM-2008-ChinNPQ #bound #low level #memory management #source code
- Analysing memory resource bounds for low-level programs (WNC, HHN, CP, SQ), pp. 151–160.
- PEPM-2008-PopeeaXC #array #bound #precise
- A practical and precise inference and specializer for array bound checks elimination (CP, DNX, WNC), pp. 177–187.
- OOPSLA-2006-ChinCKP #approach #parametricity
- A flow-based approach for variant parametric types (WNC, FC, SCK, CP), pp. 273–290.
- ICSE-2005-ChinKQPN #alias #policy #safety #verification
- Verifying safety policies with size properties and alias controls (WNC, SCK, SQ, CP, HHN), pp. 186–195.
- PEPM-2004-PopeeaC #correctness #protocol #proving #type system #verification
- A type system for resource protocol verification and its correctness proof (CP, WNC), pp. 135–146.