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
3 × USA
Collaborated with:
A.Rybalchenko J.Lee C.Hur J.Regehr J.Monteiro S.Grebenshchikov C.Popeea D.Menendez S.Nagarakatte J.A.N.Pérez A.Singh A.Gupta G.D.Plotkin N.Bjørner G.Varghese R.J.0002 Zhengyang Liu R.S.0001 M.Costa A.Lal S.K.Rajamani S.A.Seshia K.Vaswani Yoonseung Kim Youngju Song S.Das David Majnemer
Talks about:
verifi (4) optim (4) softwar (3) llvm (3) distribut (2) peephol (2) verif (2) level (2) aliv (2) methodolog (1)

Person: Nuno P. Lopes

DBLP DBLP: Lopes:Nuno_P=

Contributed to:

PLDI 20152015
VMCAI 20142014
PLDI 20122012
TACAS 20122012
VMCAI 20112011
ICLP 20102010
CAV (2) 20192019
OOPSLA 20182018
PLDI 20162016
POPL 20162016
PLDI 20172017

Wrote 11 papers:

PLDI-2015-LopesMNR #optimisation
Provably correct peephole optimizations with alive (NPL, DM, SN, JR), pp. 22–32.
VMCAI-2014-LopesM #compilation #optimisation #synthesis
Weakest Precondition Synthesis for Compiler Optimizations (NPL, JM), pp. 203–221.
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.
VMCAI-2011-LopesR #distributed #model checking #predict
Distributed and Predictable Software Model Checking (NPL, AR), pp. 340–355.
ICLP-J-2010-LopesNRS #distributed #prolog
Applying Prolog to develop distributed systems (NPL, JANP, AR, AS), pp. 691–707.
CAV-2019-LeeHL #named #optimisation #verification
AliveInLean: A Verified LLVM Peephole Optimization Verifier (JL, CKH, NPL), pp. 445–455.
OOPSLA-2018-LeeHJLRL #low level #optimisation
Reconciling high-level optimizations and low-level code in LLVM (JL, CKH, RJ0, ZL, JR, NPL), p. 28.
PLDI-2016-0001CLLRSV #design #verification
A design and verification methodology for secure isolated regions (RS0, MC, AL, NPL, SKR, SAS, KV), pp. 665–681.
POPL-2016-PlotkinBLRV #network #scalability #symmetry #using #verification
Scaling network verification using symmetry and surgery (GDP, NB, NPL, AR, GV), pp. 69–83.
PLDI-2017-LeeKSHDMRL #behaviour
Taming undefined behavior in LLVM (JL, YK, YS, CKH, SD, DM, JR, NPL), pp. 633–647.
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.