Articles

  • No categories

Publications

  • A Mechanical Soundness Proof for Subtyping over Recursive Types. Timothy Jones and David J. Pearce. In Proceedings of the Workshop on Formal Techniques for Java-like Languages (FTFJP), (to appear), 2016.
  • Designing a Verifying Compiler: Lessons Learned from Developing Whiley. David J. Pearce and Lindsay Groves. In Science of Computer Programming, pages 191–220, 2015. © Elsevier. A preprint version is also available [ PDF / DOI ].
  • The Whiley Rewrite Language (WyRL). David J. Pearce. In Proceedings of the Conference on Software Language Engineering (SLE), pages 161–166, 2015. [ PDF / Conference Website ]
  • Some Usability Hypotheses for Verification. David J. Pearce. In Proceedings of the Workshop on Evaluation and Usability of Programming Languages (PLATEAU), 2015. [ PDF / Workshop Website ].
  • Integer Range Analysis for Whiley on Embedded Systems. David J. Pearce. In Proceedings of the IEEE/IFIP Workshop on Software Technologies for Future Embedded and Ubiquitous Systems, (to appear), 2015. © IEEE Computer Society Press [ PDF / Workshop Website ]
  • Reflections on Verifying Software with Whiley. David J. Pearce and Lindsay Groves. In Proceedings of the Workshop on Formal Techniques for Safety-Critical Software (FTSCS), (to appear), 2013. A preliminarly copy is available [ PDF ]
  • Whiley: a Platform for Research in Software Verification. David J. Pearce and Lindsay Groves. In Proceedings of the Conference on Software Language Engineering (SLE), pages 238–248, 2013. A preliminarly copy is available [ PDF ]
  • A Calculus for Constraint-Based Flow Typing. David J. Pearce. In Proceedings of the Workshop on Formal Techniques for Java-like Languages (FTFJP), Article 7, 2013. [ Postscript / PDF / DOI ] (see also technical report below).
  • Sound and Complete Flow Typing with Unions, Intersections and Negations, David J. Pearce.  In Proceedings of the Conference on Verification, Model Checking and Abstract Interpretation (VMCAI), to appear, 2013. [ Postscript / PDF ] (see also technical report below).
  • Implementing a Language with Flow-Sensitive and Structural Typing on the JVM. David J. Pearce and James Noble. In Proceedings of the Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE), 2011. [ Postscript / PDF ]

Technical Reports

  • Practical Verification Condition Generation for a Bytecode Language. David J. Pearce, Victoria University of Wellington, Technical Report #ECSTR14-07, 2014. [ PDF ]
  • Reflections on Verifying Software with Whiley. David J. Pearce and Lindsay Groves, Victoria University of Wellington, Technical Report #ECSTR13-06, 2013. [ PDF ]
  • Sound and Complete Flow Typing with Unions, Intersections and Negations. David J. Pearce, Victoria University of Wellington, Technical Report #ECSTR12-20, 2012. [ Postscript / PDF ]
  • A Constraint-Based Calculus for Flow Typing. David J. Pearce, Victoria University of Wellington, Technical Report #ECSTR12-10, 2012. [ Postscript / PDF ]
  • An Algorithmic Framework for Recursive Structural Types. David J. Pearce, Victoria University of Wellington, Technical Report #ECSTR11-10, 2011. [ PostscriptPDF ]
  • Flow-Sensitive Types for Whiley. David J. Pearce and James Noble, Victoria University of Wellington, Technical Report #ECSTR10-23, 2011. [ PostscriptPDF ]