Travelled to:1 × Canada
1 × Denmark
1 × Germany
1 × Hungary
1 × Russia
1 × Slovenia
1 × Spain
1 × United Kingdom
10 × USA
2 × Cyprus
2 × France
2 × Italy
Collaborated with:M.Dodds G.M.Bierman L.Birkedal V.Vafeiadis K.Svendsen R.Bornat C.Calcagno E.Koskinen J.Wickerson M.Botincan D.Distefano P.W.O'Hearn A.F.Donaldson A.J.Summers A.Gotsman T.Dinsdale-Young P.Gardner S.Jagannathan M.Herlihy J.Noble R.Strnisa P.Sewell D.Vytiniotis K.Vaswani M.Costa Aaron Blankstein C.Haase S.Ishtiaq J.Ouaknine X.Feng B.Cook A.Khyzha M.Windsor B.Simner H.Yang C.S.Gordon J.Parsons A.Bromfield J.Duffy D.Naudziuniene R.Grigore Piyus Kedia P.Deligiannis D.McDermott Jonathan Balkind
Talks about:separ (7) logic (7) modular (6) concurr (6) reason (6) memori (4) verif (4) block (4) safe (4) abstract (3)
Person: Matthew J. Parkinson
DBLP: Parkinson:Matthew_J=
Contributed to:
2015
2013
2013
2013
2013
2012
2011
201120112011
20112010201020102009200920082008200820072007
2007
200620052017201720172017Wrote 31 papers:
- PLDI-2015-KoskinenP #transaction
- The Push/Pull model of transactions (EK, MJP), pp. 186–195.
- CAV-2013-HaaseIOP #graph #logic #named #reasoning
- SeLoger: A Tool for Graph-Based Reasoning in Separation Logic (CH, SI, JO, MJP), pp. 790–795.
- ECOOP-2013-SvendsenBP #case study #composition #concurrent #higher-order #library #named #specification
- Joins: A Case Study in Modular Specification of a Concurrent Reentrant Higher-Order Library (KS, LB, MJP), pp. 327–351.
- ESOP-2013-SvendsenBP #composition #concurrent #data type #reasoning
- Modular Reasoning about Separation of Concurrent Data Structures (KS, LB, MJP), pp. 169–188.
- ESOP-2013-WickersonDP #logic #proving
- Ribbon Proofs for Separation Logic (JW, MD, MJP), pp. 189–208.
- POPL-2013-Dinsdale-YoungBGPY #composition #concurrent #named #reasoning #source code
- Views: compositional reasoning for concurrent programs (TDY, LB, PG, MJP, HY), pp. 287–300.
- OOPSLA-2012-GordonPPBD #parallel
- Uniqueness and reference immutability for safe parallelism (CSG, MJP, JP, AB, JD), pp. 21–40.
- ASE-2011-BotincanDDP #manycore #memory management
- Safe asynchronous multicore memory operations (MB, MD, AFD, MJP), pp. 153–162.
- ESEC-FSE-2011-NaudziunieneBDDGP #automation #ide #java #named #source code #verification
- jStar-eclipse: an IDE for automated verification of Java programs (DN, MB, DD, MD, RG, MJP), pp. 428–431.
- ESOP-2011-ParkinsonS #logic
- The Relationship between Separation Logic and Implicit Dynamic Frames (MJP, AJS), pp. 439–458.
- POPL-2011-DoddsJP #composition #parallel #reasoning
- Modular reasoning for deterministic parallelism (MD, SJ, MJP), pp. 259–270.
- PPoPP-2011-BotincanDDP #automation #memory management #proving #safety
- Automatic safety proofs for asynchronous memory operations (MB, MD, AFD, MJP), pp. 313–314.
- ECOOP-2010-Dinsdale-YoungDGPV #concurrent
- Concurrent Abstract Predicates (TDY, MD, PG, MJP, VV), pp. 504–528.
- ECOOP-2010-SvendsenBP #verification
- Verifying Generics and Delegates (KS, LB, MJP), pp. 175–199.
- ESOP-2010-WickersonDP #composition #reasoning
- Explicit Stabilisation for Modular Rely-Guarantee Reasoning (JW, MD, MJP), pp. 610–629.
- POPL-2010-KoskinenPH #transaction
- Coarse-grained transactions (EK, MJP, MH), pp. 19–30.
- ESOP-2009-DoddsFPV #reasoning
- Deny-Guarantee Reasoning (MD, XF, MJP, VV), pp. 363–377.
- POPL-2009-GotsmanCPV #algorithm #proving
- Proving that non-blocking algorithms don’t block (AG, BC, MJP, VV), pp. 16–28.
- ECOOP-2008-BiermanPN #incremental #named
- UpgradeJ: Incremental Typechecking for Class Upgrades (GMB, MJP, JN), pp. 235–259.
- OOPSLA-2008-DistefanoP #java #named #towards #verification
- jStar: towards practical verification for java (DD, MJP), pp. 213–226.
- POPL-2008-ParkinsonB #abstraction #inheritance #logic
- Separation logic, abstraction and inheritance (MJP, GMB), pp. 75–86.
- OOPSLA-2007-StrniaaSP #design #java #semantics
- The java module system: core design and semantic definition (RS, PS, MJP), pp. 499–514.
- POPL-2007-ParkinsonBO #composition #stack #verification
- Modular verification of a non-blocking stack (MJP, RB, PWO), pp. 297–302.
- SAS-2007-CalcagnoPV #composition #concurrent #fine-grained #safety
- Modular Safety Checking for Fine-Grained Concurrency (CC, MJP, VV), pp. 233–248.
- LICS-2006-ParkinsonBC #hoare #logic
- Variables as Resource in Hoare Logics (MJP, RB, CC), pp. 137–146.
- POPL-2005-BornatCOP #logic
- Permission accounting in separation logic (RB, CC, PWO, MJP), pp. 259–270.
- POPL-2005-ParkinsonB #abstraction #logic
- Separation logic and abstraction (MJP, GMB), pp. 247–258.
- ESOP-2017-KhyzhaDGP #partial order #proving #using
- Proving Linearizability Using Partial Orders (AK, MD, AG, MJP), pp. 639–667.
- CAV-2017-WindsorDSP #concurrent #lightweight #named #verification
- Starling: Lightweight Concurrency Verification with Views (MW, MD, BS, MJP), pp. 544–569.
- OOPSLA-2017-ParkinsonVVCDMB #dot-net #memory management
- Project snowflake: non-blocking safe manual memory management in .NET (MJP, DV, KV, MC, PD, DM, AB, JB), p. 25.
- PLDI-2017-KediaCPVVB #memory management #performance
- Simple, fast, and safe manual memory management (PK, MC, MJP, KV, DV, AB), pp. 233–247.