Automated Software Verification
On June 1 we discussed a paper by Dietsch et al that compares two approaches to checking program traces.
On May 25 we discussed the paper Property Checking Array Programs Using Loop Shrinking by Kumar et al from TACAS 2018.
On May 18 we discussed the tutorial paper Automated Software Verification by Farzan et al.
On May 11 we had a shared coding session. I.e., bring along your current coding project and let’s write some code...
Disambiguating Parser Conflicts
On May 4, Luís Eduardo de Souza Amorim from TU Delft gave a talk on his work to disambiguate conflicts in generalised parsers.
Context-free grammars are widely used for language prototyping and implementation. They allow formalizing the syntax of domain-specific or general-purpose programming languages concisely and declaratively. However, the natural and concise way of writing a context-free grammar is often ambiguous. Therefore, grammar formalisms support extensions in the form of declarative disambiguation rules to specify operator precedence and associativity, solving ambiguities that are caused by the subset of the grammar that corresponds to expressions. Ambiguities with respect to operator precedence and associativity arise from combining the various operators of a language. While shallow conflicts can be resolved efficiently by one-level tree patterns, deep conflicts require more elaborate techniques, because they can occur arbitrarily nested in a tree. Current state-of-the-art approaches to solving deep priority conflicts come with a severe performance overhead. In this talk, I will present a novel low-overhead implementation technique for disambiguating deep associativity and priority conflicts in scannerless generalized parsers with lightweight data-dependency. By parsing a corpus of popular open-source repositories written in Java and OCaml, we found that our approach yields speedups of up to 1.73 x over a grammar rewriting technique when parsing programs with deep priority conflicts — with a modest overhead of 1 % to 2 % when parsing programs without deep conflicts.
On April 27 Tony Sloane gave a demo of the JupyterLab in-browser computational environment, including some discussion of support for non-notebook-traditional JVM-based languages such as Scala via the beakerx extension.
Author Obfuscation using Differential Privacy
On April 6 Natasha Fernandes presented her MRes thesis work on A Novel Framework for Author Obfuscation using Generalised Differential Privacy.
- Threshold concepts in computer science: do they exist and are they useful? by Boustedt et al
- Identifying threshold concepts: from dead end to a new direction by Shinners-Kennedy et al
On March 16 we discussed the following paper: Abstraction ability as an indicator of success for learning computing science? by Bennedssen and Caspersen.
On March 9 we discussed two short papers about the applications and use of WebAssembly:
- TaintAssembly: Taint-Based Information Flow Control Tracking for WebAssembly by Fu et al.
On March 2 we discussed the paper Mechanising and Verifying the WebAssembly Specification by Watt. More information on WebAssembly can be found at the project site.
Safety-Critical Use of a Formally-Verified Compiler
On January 19 we discussed the paper CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler by Kästner et al.