BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
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 DBLP: Popeea:Corneliu

Contributed to:

POPL 20142014
CAV 20132013
TACAS 20132013
PLDI 20122012
TACAS 20122012
CAV 20112011
POPL 20112011
SAC 20102010
SAC 20102013
ISMM 20082008
PEPM 20082008
OOPSLA 20062006
ICSE 20052005
PEPM 20042004

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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.